style: add missing spaces between a tactic name and its arguments (#1…

…1714)

After the `(d)simp` and `rw` tactics - hints to find further occurrences welcome.

[zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Style.3A.20spacing.20between.20tactic.20name.20and.20arguments)

Co-authored-by: @sven-manthe

Mathlib/Algebra/Associated.lean

@@ -1191,7 +1191,7 @@ theorem le_of_mul_le_mul_left (a b c : Associates α) (ha : a ≠ 0) : a * b ≤
 
 theorem one_or_eq_of_le_of_prime : ∀ p m : Associates α, Prime p → m ≤ p → m = 1 ∨ m = p
   | p, m, ⟨hp0, _, h⟩, ⟨d, r⟩ => by
-    have dvd_rfl' : p ∣ m * d := by rw[r]
+    have dvd_rfl' : p ∣ m * d := by rw [r]
     rw [r]
     match h m d dvd_rfl' with
     | Or.inl h' =>

Mathlib/Algebra/GradedMonoid.lean

@@ -448,7 +448,7 @@ theorem GradedMonoid.mk_list_dProd (l : List α) (fι : α → ι) (fA : ∀ a,
   match l with
   | [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
   | head::tail =>
-    simp[← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
+    simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
 #align graded_monoid.mk_list_dprod GradedMonoid.mk_list_dProd
 
 /-- A variant of `GradedMonoid.mk_list_dProd` for rewriting in the other direction. -/

Mathlib/Algebra/Parity.lean

@@ -306,7 +306,7 @@ set_option linter.deprecated false in
 
 @[simp]
 theorem even_two : Even (2 : α) :=
-  ⟨1, by rw[one_add_one_eq_two]⟩
+  ⟨1, by rw [one_add_one_eq_two]⟩
 #align even_two even_two
 
 @[simp]

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -222,7 +222,7 @@ noncomputable abbrev Scheme.restrictMapIso {X Y : Scheme} (f : X ⟶ Y) [IsIso f
   apply IsOpenImmersion.isoOfRangeEq (f := X.ofRestrict _ ≫ f)
     (H := PresheafedSpace.IsOpenImmersion.comp (hf := inferInstance) (hg := inferInstance))
     (Y.ofRestrict _) _
-  dsimp[restrict]
+  dsimp [restrict]
   rw [coe_comp, Set.range_comp, Opens.coe_inclusion, Subtype.range_val, Subtype.range_coe]
   refine' @Set.image_preimage_eq _ _ f.1.base U.1 _
   rw [← TopCat.epi_iff_surjective]

Mathlib/Analysis/Calculus/FDeriv/Prod.lean

@@ -414,7 +414,7 @@ theorem hasStrictFDerivAt_apply (i : ι) (f : ∀ i, F' i) :
   have h := ((hasStrictFDerivAt_pi'
              (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ':=id') (x:=f))).1
   have h' : comp (proj i) id' = proj i := by rfl
-  rw[← h']; apply h; apply hasStrictFDerivAt_id
+  rw [← h']; apply h; apply hasStrictFDerivAt_id
 
 @[simp 1100] -- Porting note: increased priority to make lint happy
 theorem hasStrictFDerivAt_pi :
@@ -477,7 +477,7 @@ theorem hasFDerivWithinAt_apply (i : ι) (f : ∀ i, F' i) (s' : Set (∀ i, F'
   have h := ((hasFDerivWithinAt_pi'
              (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ':=id') (x:=f) (s:=s'))).1
   have h' : comp (proj i) id' = proj i := by rfl
-  rw[← h']; apply h; apply hasFDerivWithinAt_id
+  rw [← h']; apply h; apply hasFDerivWithinAt_id
 
 theorem hasFDerivWithinAt_pi :
     HasFDerivWithinAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') s x ↔

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

@@ -1115,7 +1115,7 @@ This is an isomorphism iff `G` preserves the equalizer of `f,g`; see
 noncomputable def equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] :
     G.obj (equalizer f g) ⟶ equalizer (G.map f) (G.map g) :=
   equalizer.lift (G.map (equalizer.ι _ _))
-    (by simp only [← G.map_comp]; rw[equalizer.condition])
+    (by simp only [← G.map_comp]; rw [equalizer.condition])
 #align category_theory.limits.equalizer_comparison CategoryTheory.Limits.equalizerComparison
 
 @[reassoc (attr := simp)]

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -493,7 +493,7 @@ def image.eqToHom (h : f = f') : image f ⟶ image f' :=
 instance (h : f = f') : IsIso (image.eqToHom h) :=
   ⟨⟨image.eqToHom h.symm,
       ⟨(cancel_mono (image.ι f)).1 (by
-          -- Porting note: added let's for used to be a simp[image.eqToHom]
+          -- Porting note: added let's for used to be a simp [image.eqToHom]
           let F : MonoFactorisation f' :=
             ⟨image f, image.ι f, factorThruImage f, (by aesop_cat)⟩
           dsimp [image.eqToHom]
@@ -502,7 +502,7 @@ instance (h : f = f') : IsIso (image.eqToHom h) :=
             ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
           rw [image.lift_fac F'] ),
         (cancel_mono (image.ι f')).1 (by
-          -- Porting note: added let's for used to be a simp[image.eqToHom]
+          -- Porting note: added let's for used to be a simp [image.eqToHom]
           let F' : MonoFactorisation f :=
             ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
           dsimp [image.eqToHom]

Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

@@ -538,7 +538,7 @@ def IsKernel.isoKernel {Z : C} (l : Z ⟶ X) {s : KernelFork f} (hs : IsLimit s)
     Cones.ext i.symm fun j => by
       cases j
       · exact (Iso.eq_inv_comp i).2 h
-      · dsimp; rw[← h]; simp
+      · dsimp; rw [← h]; simp
 #align category_theory.limits.is_kernel.iso_kernel CategoryTheory.Limits.IsKernel.isoKernel
 
 /-- If `i` is an isomorphism such that `i.hom ≫ kernel.ι f = l`, then `l` is a kernel of `f`. -/

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -110,7 +110,7 @@ theorem ext (I J : HasZeroMorphisms C) : I = J := by
     apply I.zero_comp X (J.zero Y Y).zero
   have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
     apply J.comp_zero (I.zero X Y).zero Y
-  rw[← this, ← that]
+  rw [← this, ← that]
 #align category_theory.limits.has_zero_morphisms.ext CategoryTheory.Limits.HasZeroMorphisms.ext
 
 instance : Subsingleton (HasZeroMorphisms C) :=

Mathlib/Control/Functor/Multivariate.lean

@@ -193,7 +193,7 @@ theorem LiftP_PredLast_iff {β} (P : β → Prop) (x : F (α ::: β)) :
     rw [MvFunctor.map_map]
     dsimp (config := { unfoldPartialApp := true }) [(· ⊚ ·)]
     suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val)
-      by rw[this];
+      by rw [this];
     ext i ⟨x, _⟩
     cases i <;> rfl
 #align mvfunctor.liftp_last_pred_iff MvFunctor.LiftP_PredLast_iff
@@ -234,7 +234,7 @@ theorem LiftR_RelLast_iff (x y : F (α ::: β)) :
     suffices  (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst))
             ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd))
     by  rcases this with ⟨left, right⟩
-        rw[left, right];
+        rw [left, right];
     constructor <;> ext i ⟨x, _⟩ <;> cases i <;> rfl
 #align mvfunctor.liftr_last_rel_iff MvFunctor.LiftR_RelLast_iff
 

Mathlib/Data/List/Infix.lean

@@ -377,7 +377,7 @@ theorem tails_cons (a : α) (l : List α) : tails (a :: l) = (a :: l) :: l.tails
 @[simp]
 theorem inits_append : ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l
   | [], [] => by simp
-  | [], a :: t => by simp[· ∘ ·]
+  | [], a :: t => by simp [· ∘ ·]
   | a :: s, t => by simp [inits_append s t, · ∘ ·]
 #align list.inits_append List.inits_append
 
@@ -440,7 +440,7 @@ theorem nth_le_tails (l : List α) (n : ℕ) (hn : n < length (tails l)) :
   induction' l with x l IH generalizing n
   · simp
   · cases n
-    · simp[nthLe_cons]
+    · simp [nthLe_cons]
     · simpa[nthLe_cons] using IH _ _
 #align list.nth_le_tails List.nth_le_tails
 
@@ -450,7 +450,7 @@ theorem nth_le_inits (l : List α) (n : ℕ) (hn : n < length (inits l)) :
   induction' l with x l IH generalizing n
   · simp
   · cases n
-    · simp[nthLe_cons]
+    · simp [nthLe_cons]
     · simpa[nthLe_cons] using IH _ _
 #align list.nth_le_inits List.nth_le_inits
 end deprecated

Mathlib/Data/Nat/Digits.lean

@@ -270,7 +270,7 @@ theorem ofDigits_digits (b n : ℕ) : ofDigits b (digits b n) = n := by
   · cases' b with b
     · induction' n with n ih
       · rfl
-      · rw[show succ zero = 1 by rfl] at ih ⊢
+      · rw [show succ zero = 1 by rfl] at ih ⊢
         simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
     · apply Nat.strongInductionOn n _
       clear n

Mathlib/Data/Vector/MapLemmas.lean

@@ -235,7 +235,7 @@ theorem mapAccumr_eq_map {f : α → σ → σ × β} {s₀ : σ} (S : Set σ) (
     (closure : ∀ a s, s ∈ S → (f a s).1 ∈ S)
     (out : ∀ a s s', s ∈ S → s' ∈ S → (f a s).2 = (f a s').2) :
     (mapAccumr f xs s₀).snd = map (f · s₀ |>.snd) xs := by
-  rw[Vector.map_eq_mapAccumr]
+  rw [Vector.map_eq_mapAccumr]
   apply mapAccumr_bisim_tail
   use fun s _ => s ∈ S, h₀
   exact @fun s _q a h => ⟨closure a s h, out a s s₀ h h₀⟩
@@ -253,7 +253,7 @@ theorem mapAccumr₂_eq_map₂ {f : α → β → σ → σ × γ} {s₀ : σ} (
     (closure : ∀ a b s, s ∈ S → (f a b s).1 ∈ S)
     (out : ∀ a b s s', s ∈ S → s' ∈ S → (f a b s).2 = (f a b s').2) :
     (mapAccumr₂ f xs ys s₀).snd = map₂ (f · · s₀ |>.snd) xs ys := by
-  rw[Vector.map₂_eq_mapAccumr₂]
+  rw [Vector.map₂_eq_mapAccumr₂]
   apply mapAccumr₂_bisim_tail
   use fun s _ => s ∈ S, h₀
   exact @fun s _q a b h => ⟨closure a b s h, out a b s s₀ h h₀⟩

Mathlib/Data/Vector/Snoc.lean

@@ -138,7 +138,7 @@ theorem mapAccumr_snoc :
       (r.1, r.2.snoc q.2) := by
   induction xs using Vector.inductionOn
   · rfl
-  · simp[*]
+  · simp [*]
 
 variable (ys : Vector β n)
 

Mathlib/GroupTheory/MonoidLocalization.lean

@@ -1979,8 +1979,8 @@ theorem leftCancelMulZero_of_le_isLeftRegular
     exact ha hb
   have main : g (b.1 * (x.2 * y.1)) = g (b.1 * (y.2 * x.1)) :=
     calc
-      g (b.1 * (x.2 * y.1)) = g b.1 * (g x.2 * g y.1) := by rw[map_mul g,map_mul g]
-      _ = a * g b.2 * (g x.2 * (w * g y.2)) := by rw[hb, hy]
+      g (b.1 * (x.2 * y.1)) = g b.1 * (g x.2 * g y.1) := by rw [map_mul g,map_mul g]
+      _ = a * g b.2 * (g x.2 * (w * g y.2)) := by rw [hb, hy]
       _ = a * w * g b.2 * (g x.2 * g y.2) := by
         rw [← mul_assoc, ← mul_assoc _ w, mul_comm _ w, mul_assoc w, mul_assoc,
           ← mul_assoc w, ← mul_assoc w, mul_comm w]

Mathlib/Logic/Embedding/Basic.lean

@@ -206,9 +206,9 @@ def setValue {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' =
     split_ifs at h with h₁ h₂ _ _ h₅ h₆ <;>
         (try subst b) <;>
         (try simp only [f.injective.eq_iff, not_true_eq_false] at *)
-    · rw[h₁,h₂]
-    · rw[h₁,h]
-    · rw[h₅, ← h]
+    · rw [h₁,h₂]
+    · rw [h₁,h]
+    · rw [h₅, ← h]
     · exact h₆.symm
     · exfalso; exact h₅ h.symm
     · exfalso; exact h₁ h

Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

@@ -226,7 +226,7 @@ theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α]
   rw [← Equiv.image_eq_preimage _ _]
   refine ⟨{y | y n}, by measurability, ?_⟩
   rw [← Equiv.preimage_eq_iff_eq_image]
-  simp[mapNatBool]
+  simp [mapNatBool]
 
 /-- If a measurable space admits a countable sequence of measurable sets separating points,
 it admits a measurable injection into the Cantor space `ℕ → Bool`

test/fun_prop_dev.lean

@@ -354,7 +354,7 @@ def iterate (n : Nat) (f : α → α) (x : α) : α :=
   | n+1 => iterate n f (f x)
 
 theorem iterate_con (n : Nat) (f : α → α) (hf : Con f) : Con (iterate n f) := by
-  induction n <;> (simp[iterate]; fun_prop)
+  induction n <;> (simp [iterate]; fun_prop)
 
 
 example : let f := fun x : α => x; Con f := by fun_prop