[Merged by Bors] - style: fix spacing around left arrows

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

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

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

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

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α

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 =>

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.

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

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