From 1ab6b6eff13473e27184092af74fce0ac8ea9fa7 Mon Sep 17 00:00:00 2001 From: Batixx Date: Mon, 20 Jul 2026 01:01:06 +0200 Subject: [PATCH] style: fix spacing around left arrow --- Cache/Main.lean | 2 +- Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean | 2 +- Mathlib/NumberTheory/SelbergSieve.lean | 4 ++-- Mathlib/Tactic/CategoryTheory/Slice.lean | 2 +- Mathlib/Tactic/NormNum/Basic.lean | 2 +- Mathlib/Tactic/NormNum/Eq.lean | 2 +- Mathlib/Tactic/Ring/Common.lean | 2 +- Mathlib/Topology/Sets/Opens.lean | 4 ++-- MathlibTest/Algebra/Polynomial.lean | 2 +- 9 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Cache/Main.lean b/Cache/Main.lean index dcce94de04f8fd..8a721d6c500554 100644 --- a/Cache/Main.lean +++ b/Cache/Main.lean @@ -256,7 +256,7 @@ def main (args : List String) : IO Unit := do unstageFiles stagingDir?.get! overwrite let putStaged (stagingDir : FilePath) := do let repo := repo?.getD MATHLIBREPO - if !(←stagingDir.isDir) then IO.println "--staging-dir must be a directory" return + if !(← stagingDir.isDir) then IO.println "--staging-dir must be a directory" return else let fileSet ← getFilesWithExtension stagingDir "ltar" let auth ← getUploadAuth diff --git a/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean b/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean index 7a830cde3f2de0..506bc6c0e52653 100644 --- a/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean +++ b/Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean @@ -343,7 +343,7 @@ theorem MeromorphicAt.meromorphicTrailingCoeffAt_sub_eq_sub {f₁ f₂ : 𝕜 rw [sub_eq_add_neg, hf₁.meromorphicTrailingCoeffAt_add_eq_add (by fun_prop)] · rw [meromorphicTrailingCoeffAt_neg, sub_eq_add_neg] · rwa [← meromorphicOrderAt_neg] - · rwa [meromorphicTrailingCoeffAt_neg, ←sub_eq_add_neg] + · rwa [meromorphicTrailingCoeffAt_neg, ← sub_eq_add_neg] /-- If `f₁` and `f₂` have equal order at `x` and if their trailing coefficients do not cancel, then the diff --git a/Mathlib/NumberTheory/SelbergSieve.lean b/Mathlib/NumberTheory/SelbergSieve.lean index af6311cc74e0c1..7a855ecf194573 100644 --- a/Mathlib/NumberTheory/SelbergSieve.lean +++ b/Mathlib/NumberTheory/SelbergSieve.lean @@ -244,7 +244,7 @@ private theorem sum_divisors_lambda_sq_larger_sum (f : ℕ → ℕ → ℕ → congr! 1 with d hd rw [mem_divisors] at hd suffices ∀ d1 d2, (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2) by - simp_rw [←Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ite_sum_zero, ← ite_and, this] + simp_rw [← Nat.divisors_filter_dvd_of_dvd hd.2 hd.1, sum_filter, ite_sum_zero, ← ite_and, this] simp +contextual [← and_assoc, Nat.dvd_lcm_left, Nat.dvd_lcm_right] theorem upperMoebius_lambdaSquared (weights : ℕ → ℝ) (hw : weights 1 = 1) : @@ -312,7 +312,7 @@ theorem inv_selbergTerms_eq_sum_divisors_moebius_nu {l : ℕ} (hl : Squarefree l theorem nu_inv_eq_sum_divisors_inv_selbergTerms {d : ℕ} (hdP : d ∣ s.prodPrimes) : (s.nu d)⁻¹ = ∑ l ∈ divisors s.prodPrimes, if l ∣ d then (s.selbergTerms l)⁻¹ else 0 := by - rw [eq_comm, ←sum_filter, Nat.divisors_filter_dvd_of_dvd prodPrimes_ne_zero hdP] + rw [eq_comm, ← sum_filter, Nat.divisors_filter_dvd_of_dvd prodPrimes_ne_zero hdP] have hd_pos : 0 < d := Nat.pos_of_ne_zero <| ne_zero_of_dvd_ne_zero prodPrimes_ne_zero hdP revert hdP; revert d apply (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on _ (fun _ _ ↦ Nat.dvd_trans)).mpr diff --git a/Mathlib/Tactic/CategoryTheory/Slice.lean b/Mathlib/Tactic/CategoryTheory/Slice.lean index aa7a254d6e05b1..44e7887810f226 100644 --- a/Mathlib/Tactic/CategoryTheory/Slice.lean +++ b/Mathlib/Tactic/CategoryTheory/Slice.lean @@ -36,7 +36,7 @@ syntax (name := slice) "slice " num ppSpace num : conv `evalSlice` - rewrites the target expression using `Category.assoc`. - uses `congr` to split off the first `a-1` terms and rotates to `a`-th (last) term -- counts the number `k` of rewrites as it uses `←Category.assoc` to bring the target to +- counts the number `k` of rewrites as it uses `← Category.assoc` to bring the target to left associated form; from the first step this is the total number of remaining terms from `C` - it now splits off `b-a` terms from target using `congr` leaving the desired subterm - finally, it rewrites it once more using `Category.assoc` to bring it to right-associated diff --git a/Mathlib/Tactic/NormNum/Basic.lean b/Mathlib/Tactic/NormNum/Basic.lean index 75d94adc7e7ec4..93a7212043770f 100644 --- a/Mathlib/Tactic/NormNum/Basic.lean +++ b/Mathlib/Tactic/NormNum/Basic.lean @@ -529,7 +529,7 @@ def Result.mul {u : Level} {α : Q(Type u)} {a b : Q($α)} (ra : Result q($a)) ( | .isNNRat dsα .., .isNegNat rα .. | .isNegNat rα .., .isNNRat dsα .. => -- could alternatively try to combine `rα` and `dsα` here, but we'd have to do a defeq check -- so would still need to be in `MetaM`. - ratArm (←synthInstanceQ q(DivisionRing $α)) + ratArm (← synthInstanceQ q(DivisionRing $α)) | .isNNRat dsα .., _ | _, .isNNRat dsα .. => nnratArm dsα | .isNegNat rα .., _ | _, .isNegNat rα .. => intArm rα diff --git a/Mathlib/Tactic/NormNum/Eq.lean b/Mathlib/Tactic/NormNum/Eq.lean index 1e97bb3291dc1e..f4b96a1d825e3a 100644 --- a/Mathlib/Tactic/NormNum/Eq.lean +++ b/Mathlib/Tactic/NormNum/Eq.lean @@ -112,7 +112,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/ | .isNNRat dsα .., .isNegNat rα .. | .isNegNat rα .., .isNNRat dsα .. => -- could alternatively try to combine `rα` and `dsα` here, but we'd have to do a defeq check -- so would still need to be in `MetaM`. - ratArm (←synthInstanceQ q(DivisionRing $α)) + ratArm (← synthInstanceQ q(DivisionRing $α)) | .isNNRat dsα .., _ | _, .isNNRat dsα .. => nnratArm dsα | .isNegNat rα .., _ | _, .isNegNat rα .. => intArm rα | .isNat _ na pa, .isNat mα nb pb => diff --git a/Mathlib/Tactic/Ring/Common.lean b/Mathlib/Tactic/Ring/Common.lean index 996a6a91af732a..d5b432a833389a 100644 --- a/Mathlib/Tactic/Ring/Common.lean +++ b/Mathlib/Tactic/Ring/Common.lean @@ -1081,7 +1081,7 @@ theorem atom_pf (a : R) {e : ℕ} (hone : (nat_lit 1).rawCast = e) theorem atom_pf' (p : (a : R) = a') {e : ℕ} (hone : (nat_lit 1).rawCast = e) (hb : a' ^ e * (nat_lit 1).rawCast = b) : - a = b + 0 := by simp [← hone, ←hb, *] + a = b + 0 := by simp [← hone, ← hb, *] /-- Evaluates an atom, an expression where `ring` can find no additional structure. diff --git a/Mathlib/Topology/Sets/Opens.lean b/Mathlib/Topology/Sets/Opens.lean index cc3280cda6292b..7e789d277caf22 100644 --- a/Mathlib/Topology/Sets/Opens.lean +++ b/Mathlib/Topology/Sets/Opens.lean @@ -282,10 +282,10 @@ theorem mem_compl {U : Opens α} {x : α} : x ∈ Uᶜ ↔ ∃ V : Opens α, Dis simp [compl_eq_sSup_disjoint] theorem interior_compl {U : Opens α} : Opens.interior (U : Set α)ᶜ = Uᶜ := by - simp [←himp_bot, himp_def] + simp [← himp_bot, himp_def] theorem coe_compl_eq_interior_compl {U : Opens α} : ↑(Uᶜ) = interior (U : Set α)ᶜ := by - rw [←interior_compl, coe_interior] + rw [← interior_compl, coe_interior] /-- The coercion from open sets to sets as a `FrameHom`. -/ @[simps] protected def frameHom : FrameHom (Opens α) (Set α) where diff --git a/MathlibTest/Algebra/Polynomial.lean b/MathlibTest/Algebra/Polynomial.lean index e56b3b9a2c5b53..9680c297df39cd 100644 --- a/MathlibTest/Algebra/Polynomial.lean +++ b/MathlibTest/Algebra/Polynomial.lean @@ -38,5 +38,5 @@ example : (reprPrec p2 65).pretty = "(C 57 + C 22 * X ^ 2)" := by native_decide -- test that parens are added inside `C` def pu1 : (ULift.{1} ℕ)[X] := ⟨⟨{1}, Pi.single 1 (ULift.up 37), - by intro; simp [Pi.single, Function.update_apply, ←ULift.down_inj]⟩⟩ + by intro; simp [Pi.single, Function.update_apply, ← ULift.down_inj]⟩⟩ example : reprStr pu1 = "C (ULift.up 37) * X" := by native_decide