chore: simplify by rfl (#7039)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib/Algebra/Free.lean

@@ -115,7 +115,7 @@ def lift : (α → β) ≃ (FreeMagma α →ₙ* β) where
   { toFun := liftAux f
     map_mul' := fun x y ↦ rfl }
   invFun F := F ∘ of
-  left_inv f := by rfl
+  left_inv f := rfl
   right_inv F := by ext; rfl
 #align free_magma.lift FreeMagma.lift
 

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -194,11 +194,11 @@ def ofHomotopy {φ₁ φ₂ : F ⟶ G} (ho : Homotopy φ₁ φ₂) : Cochain F G
 
 @[simp]
 lemma ofHomotopy_ofEq {φ₁ φ₂ : F ⟶ G} (h : φ₁ = φ₂) :
-    ofHomotopy (Homotopy.ofEq h) = 0 := by rfl
+    ofHomotopy (Homotopy.ofEq h) = 0 := rfl
 
 @[simp]
 lemma ofHomotopy_refl (φ : F ⟶ G) :
-    ofHomotopy (Homotopy.refl φ) = 0 := by rfl
+    ofHomotopy (Homotopy.refl φ) = 0 := rfl
 
 @[reassoc]
 lemma v_comp_XIsoOfEq_hom

Mathlib/Algebra/Lie/CartanMatrix.lean

@@ -153,11 +153,11 @@ def adF : B × B → FreeLieAlgebra R (Generators B) :=
 #align cartan_matrix.relations.ad_F CartanMatrix.Relations.adF
 
 private theorem adE_of_eq_eq_zero (i : B) (h : A i i = 2) : adE R A ⟨i, i⟩ = 0 := by
-  have h' : (-2 : ℤ).toNat = 0 := by rfl
+  have h' : (-2 : ℤ).toNat = 0 := rfl
   simp [adE, h, h']
 
 private theorem adF_of_eq_eq_zero (i : B) (h : A i i = 2) : adF R A ⟨i, i⟩ = 0 := by
-  have h' : (-2 : ℤ).toNat = 0 := by rfl
+  have h' : (-2 : ℤ).toNat = 0 := rfl
   simp [adF, h, h']
 
 /-- The union of all the relations as a subset of the free Lie algebra. -/

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -56,7 +56,7 @@ abbrev grade (m : M) : Submodule R (AddMonoidAlgebra R M) :=
   gradeBy R id m
 #align add_monoid_algebra.grade AddMonoidAlgebra.grade
 
-theorem gradeBy_id : gradeBy R (id : M → M) = grade R := by rfl
+theorem gradeBy_id : gradeBy R (id : M → M) = grade R := rfl
 #align add_monoid_algebra.grade_by_id AddMonoidAlgebra.gradeBy_id
 
 theorem mem_gradeBy_iff (f : M → ι) (i : ι) (a : AddMonoidAlgebra R M) :

Mathlib/Algebra/Symmetrized.lean

@@ -198,11 +198,11 @@ theorem unsym_neg [Neg α] (a : αˢʸᵐ) : unsym (-a) = -unsym a :=
 #align sym_alg.unsym_neg SymAlg.unsym_neg
 
 theorem mul_def [Add α] [Mul α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : αˢʸᵐ) :
-    a * b = sym (⅟ 2 * (unsym a * unsym b + unsym b * unsym a)) := by rfl
+    a * b = sym (⅟ 2 * (unsym a * unsym b + unsym b * unsym a)) := rfl
 #align sym_alg.mul_def SymAlg.mul_def
 
 theorem unsym_mul [Mul α] [Add α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : αˢʸᵐ) :
-    unsym (a * b) = ⅟ 2 * (unsym a * unsym b + unsym b * unsym a) := by rfl
+    unsym (a * b) = ⅟ 2 * (unsym a * unsym b + unsym b * unsym a) := rfl
 #align sym_alg.unsym_mul SymAlg.unsym_mul
 
 theorem sym_mul_sym [Mul α] [Add α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : α) :

Mathlib/Analysis/SpecialFunctions/Integrals.lean

@@ -357,7 +357,7 @@ theorem integral_rpow {r : ℝ} (h : -1 < r ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a,
   apply_fun Complex.re at this; convert this
   · simp_rw [intervalIntegral_eq_integral_uIoc, Complex.real_smul, Complex.ofReal_mul_re]
     · -- Porting note: was `change ... with ...`
-      have : Complex.re = IsROrC.re := by rfl
+      have : Complex.re = IsROrC.re := rfl
       rw [this, ← integral_re]; rfl
       refine' intervalIntegrable_iff.mp _
       cases' h' with h' h'

Mathlib/CategoryTheory/Category/Grpd.lean

@@ -70,8 +70,8 @@ instance category : LargeCategory.{max v u} Grpd.{v, u} where
   Hom C D := C ⥤ D
   id C := 𝟭 C
   comp F G := F ⋙ G
-  id_comp _ := by rfl
-  comp_id _ := by rfl
+  id_comp _ := rfl
+  comp_id _ := rfl
   assoc := by intros; rfl
 set_option linter.uppercaseLean3 false in
 #align category_theory.Groupoid.category CategoryTheory.Grpd.category

Mathlib/CategoryTheory/Idempotents/Karoubi.lean

@@ -118,11 +118,11 @@ theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g := by
   simpa [hom_ext_iff] using h
 
 @[simp]
-theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := by rfl
+theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := rfl
 #align category_theory.idempotents.karoubi.comp_f CategoryTheory.Idempotents.Karoubi.comp_f
 
 @[simp]
-theorem id_eq {P : Karoubi C} : 𝟙 P = ⟨P.p, by repeat' rw [P.idem]⟩ := by rfl
+theorem id_eq {P : Karoubi C} : 𝟙 P = ⟨P.p, by repeat' rw [P.idem]⟩ := rfl
 #align category_theory.idempotents.karoubi.id_eq CategoryTheory.Idempotents.Karoubi.id_eq
 
 /-- It is possible to coerce an object of `C` into an object of `Karoubi C`.
@@ -132,12 +132,12 @@ instance coe : CoeTC C (Karoubi C) :=
 #align category_theory.idempotents.karoubi.coe CategoryTheory.Idempotents.Karoubi.coe
 
 -- porting note: removed @[simp] as the linter complains
-theorem coe_X (X : C) : (X : Karoubi C).X = X := by rfl
+theorem coe_X (X : C) : (X : Karoubi C).X = X := rfl
 set_option linter.uppercaseLean3 false in
 #align category_theory.idempotents.karoubi.coe_X CategoryTheory.Idempotents.Karoubi.coe_X
 
 @[simp]
-theorem coe_p (X : C) : (X : Karoubi C).p = 𝟙 X := by rfl
+theorem coe_p (X : C) : (X : Karoubi C).p = 𝟙 X := rfl
 #align category_theory.idempotents.karoubi.coe_p CategoryTheory.Idempotents.Karoubi.coe_p
 
 @[simp]

Mathlib/CategoryTheory/Limits/Presheaf.lean

@@ -85,7 +85,7 @@ def restrictedYonedaYoneda : restrictedYoneda (yoneda : C ⥤ Cᵒᵖ ⥤ Type u
         dsimp
         have : x.app X (CategoryStruct.id (Opposite.unop X)) =
             (x.app X (𝟙 (Opposite.unop X)))
-              := by rfl
+              := rfl
         rw [this]
         rw [← FunctorToTypes.naturality _ _ x f (𝟙 _)]
         simp only [id_comp, Functor.op_obj, Opposite.unop_op, yoneda_obj_map, comp_id]

Mathlib/CategoryTheory/PathCategory.lean

@@ -62,7 +62,7 @@ def lift {C} [Category C] (φ : V ⥤q C) : Paths V ⥤ C where
   map {X} {Y} f :=
     @Quiver.Path.rec V _ X (fun Y _ => φ.obj X ⟶ φ.obj Y) (𝟙 <| φ.obj X)
       (fun _ f ihp => ihp ≫ φ.map f) Y f
-  map_id X := by rfl
+  map_id X := rfl
   map_comp f g := by
     induction' g with _ _ g' p ih _ _ _
     · rw [Category.comp_id]

Mathlib/Data/Complex/Basic.lean

@@ -916,14 +916,14 @@ example : (Complex.instSMulRealComplex : SMul ℚ ℂ) = (Algebra.toSMul : SMul
 
 /-- A complex number `z` plus its conjugate `conj z` is `2` times its real part. -/
 theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 := by
-  have : (↑(↑2 : ℝ) : ℂ) = (2 : ℂ) := by rfl
+  have : (↑(↑2 : ℝ) : ℂ) = (2 : ℂ) := rfl
   simp only [add_conj, ofReal_mul, ofReal_one, ofReal_bit0, this,
     mul_div_cancel_left (z.re : ℂ) two_ne_zero]
 #align complex.re_eq_add_conj Complex.re_eq_add_conj
 
 /-- A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part. -/
 theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj z) / (2 * I) := by
-  have : (↑2 : ℝ ) * I = 2 * I := by rfl
+  have : (↑2 : ℝ ) * I = 2 * I := rfl
   simp only [sub_conj, ofReal_mul, ofReal_one, ofReal_bit0, mul_right_comm, this,
     mul_div_cancel_left _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
 #align complex.im_eq_sub_conj Complex.im_eq_sub_conj
@@ -1024,7 +1024,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem abs_two : Complex.abs 2 = 2 :=
   calc
-    Complex.abs 2 = Complex.abs (2 : ℝ) := by rfl
+    Complex.abs 2 = Complex.abs (2 : ℝ) := rfl
     _ = (2 : ℝ) := Complex.abs_of_nonneg (by norm_num)
 #align complex.abs_two Complex.abs_two
 

Mathlib/Data/MvPolynomial/Equiv.lean

@@ -268,8 +268,8 @@ def sumAlgEquiv : MvPolynomial (Sum S₁ S₂) R ≃ₐ[R] MvPolynomial S₁ (Mv
   { sumRingEquiv R S₁ S₂ with
     commutes' := by
       intro r
-      have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) : _) := by rfl
-      have B : algebraMap R (MvPolynomial (Sum S₁ S₂) R) r = C r := by rfl
+      have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) : _) := rfl
+      have B : algebraMap R (MvPolynomial (Sum S₁ S₂) R) r = C r := rfl
       simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe_apply,
         Equiv.coe_fn_mk, B, sumToIter_C, A] }
 #align mv_polynomial.sum_alg_equiv MvPolynomial.sumAlgEquiv

Mathlib/Data/Nat/PartENat.lean

@@ -637,11 +637,11 @@ example (n : ℕ) : ((n : ℕ∞) : PartENat) = ↑n := rfl
 
 -- Porting note : new
 @[simp]
-lemma ofENat_none : ofENat Option.none = ⊤ := by rfl
+lemma ofENat_none : ofENat Option.none = ⊤ := rfl
 
 -- Porting note : new
 @[simp]
-lemma ofENat_some (n : ℕ) : ofENat (Option.some n) = ↑n := by rfl
+lemma ofENat_some (n : ℕ) : ofENat (Option.some n) = ↑n := rfl
 
 -- Porting note : new
 @[simp, norm_cast]

Mathlib/Data/PFunctor/Multivariate/Basic.lean

@@ -104,7 +104,7 @@ theorem const.get_map (f : α ⟹ β) (x : (const n A).Obj α) : const.get (f <$
 #align mvpfunctor.const.get_map MvPFunctor.const.get_map
 
 @[simp]
-theorem const.get_mk (x : A) : const.get (const.mk n x : (const n A).Obj α) = x := by rfl
+theorem const.get_mk (x : A) : const.get (const.mk n x : (const n A).Obj α) = x := rfl
 #align mvpfunctor.const.get_mk MvPFunctor.const.get_mk
 
 @[simp]

Mathlib/Data/PFunctor/Univariate/M.lean

@@ -330,7 +330,7 @@ set_option linter.uppercaseLean3 false in
 #align pfunctor.M.agree' PFunctor.M.Agree'
 
 @[simp]
-theorem dest_mk (x : F.Obj <| M F) : dest (M.mk x) = x := by rfl
+theorem dest_mk (x : F.Obj <| M F) : dest (M.mk x) = x := rfl
 set_option linter.uppercaseLean3 false in
 #align pfunctor.M.dest_mk PFunctor.M.dest_mk
 
@@ -535,7 +535,7 @@ theorem head_mk (x : F.Obj (M F)) : head (M.mk x) = x.1 :=
   Eq.symm <|
     calc
       x.1 = (dest (M.mk x)).1 := by rw [dest_mk]
-      _ = head (M.mk x) := by rfl
+      _ = head (M.mk x) := rfl
 
 set_option linter.uppercaseLean3 false in
 #align pfunctor.M.head_mk PFunctor.M.head_mk
@@ -562,7 +562,7 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem iselect_nil [DecidableEq F.A] [Inhabited (M F)] {a} (f : F.B a → M F) :
-    iselect nil (M.mk ⟨a, f⟩) = a := by rfl
+    iselect nil (M.mk ⟨a, f⟩) = a := rfl
 set_option linter.uppercaseLean3 false in
 #align pfunctor.M.iselect_nil PFunctor.M.iselect_nil
 

Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean

@@ -222,7 +222,7 @@ private theorem Cofix.bisim_aux {α : TypeVec n} (r : Cofix F α → Cofix F α
   intro rxy
   apply Quot.sound
   let r' := fun x y => r (Quot.mk _ x) (Quot.mk _ y)
-  have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := by rfl
+  have hr' : r' = fun x y => r (Quot.mk _ x) (Quot.mk _ y) := rfl
   have : IsPrecongr r' := by
     intro a b r'ab
     have h₀ :

Mathlib/Data/Seq/Computation.lean

@@ -711,7 +711,7 @@ theorem map_id : ∀ s : Computation α, map id s = s
   | ⟨f, al⟩ => by
     apply Subtype.eq; simp [map, Function.comp]
     have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl
-    have h : ((fun x: Option α => x) = id) := by rfl
+    have h : ((fun x: Option α => x) = id) := rfl
     simp [e, h, Stream'.map_id]
 #align computation.map_id Computation.map_id
 

Mathlib/LinearAlgebra/BilinearForm.lean

@@ -1106,7 +1106,7 @@ def isPairSelfAdjointSubmodule : Submodule R₂ (Module.End R₂ M₂) where
 
 @[simp]
 theorem mem_isPairSelfAdjointSubmodule (f : Module.End R₂ M₂) :
-    f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f := by rfl
+    f ∈ isPairSelfAdjointSubmodule B₂ F₂ ↔ IsPairSelfAdjoint B₂ F₂ f :=  by rfl
 #align bilin_form.mem_is_pair_self_adjoint_submodule BilinForm.mem_isPairSelfAdjointSubmodule
 
 theorem isPairSelfAdjoint_equiv (e : M₂' ≃ₗ[R₂] M₂) (f : Module.End R₂ M₂) :

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -474,7 +474,7 @@ theorem aestronglyMeasurable'_condexpL1Clm (f : α →₁[μ] F') :
     refine' AEStronglyMeasurable'.congr _ (coeFn_add _ _).symm
     exact AEStronglyMeasurable'.add hfm hgm
   · have : {f : Lp F' 1 μ | AEStronglyMeasurable' m (condexpL1Clm F' hm μ f) μ} =
-        condexpL1Clm F' hm μ ⁻¹' {f | AEStronglyMeasurable' m f μ} := by rfl
+        condexpL1Clm F' hm μ ⁻¹' {f | AEStronglyMeasurable' m f μ} := rfl
     rw [this]
     refine' IsClosed.preimage (condexpL1Clm F' hm μ).continuous _
     exact isClosed_aeStronglyMeasurable' hm

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

@@ -131,7 +131,7 @@ theorem condexpL2_indicator_of_measurable (hm : m ≤ m0) (hs : MeasurableSet[m]
   have h_mem : indicatorConstLp 2 (hm s hs) hμs c ∈ lpMeas E 𝕜 m 2 μ :=
     mem_lpMeas_indicatorConstLp hm hs hμs
   let ind := (⟨indicatorConstLp 2 (hm s hs) hμs c, h_mem⟩ : lpMeas E 𝕜 m 2 μ)
-  have h_coe_ind : (ind : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c := by rfl
+  have h_coe_ind : (ind : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c := rfl
   have h_orth_mem := orthogonalProjection_mem_subspace_eq_self ind
   rw [← h_coe_ind, h_orth_mem]
 #align measure_theory.condexp_L2_indicator_of_measurable MeasureTheory.condexpL2_indicator_of_measurable

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

@@ -718,7 +718,7 @@ theorem tendsto_of_forall_integral_tendsto {γ : Type*} {F : Filter γ} {μs : 
   apply key.mp
   have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := isometry_subtype_coe.lipschitz
   set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀
-  have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := by rfl
+  have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := rfl
   have f₀_nn : 0 ≤ ⇑f₀ := fun _ => by
     simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
   have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := eventually_of_forall f₀_nn

Mathlib/MeasureTheory/Measure/Portmanteau.lean

@@ -120,7 +120,7 @@ theorem le_measure_compl_liminf_of_limsup_measure_le {ι : Type*} {L : Filter ι
     simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
   simp_rw [meas_Ec, meas_i_Ec]
   have obs :
-    (L.liminf fun i : ι => 1 - μs i E) = L.liminf ((fun x => 1 - x) ∘ fun i : ι => μs i E) := by rfl
+    (L.liminf fun i : ι => 1 - μs i E) = L.liminf ((fun x => 1 - x) ∘ fun i : ι => μs i E) := rfl
   rw [obs]
   have := antitone_const_tsub.map_limsup_of_continuousAt (F := L)
     (fun i => μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
@@ -148,7 +148,7 @@ theorem limsup_measure_compl_le_of_le_liminf_measure {ι : Type*} {L : Filter ι
     simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
   simp_rw [meas_Ec, meas_i_Ec]
   have obs :
-    (L.limsup fun i : ι => 1 - μs i E) = L.limsup ((fun x => 1 - x) ∘ fun i : ι => μs i E) := by rfl
+    (L.limsup fun i : ι => 1 - μs i E) = L.limsup ((fun x => 1 - x) ∘ fun i : ι => μs i E) := rfl
   rw [obs]
   have := antitone_const_tsub.map_liminf_of_continuousAt (F := L)
     (fun i => μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt

Mathlib/NumberTheory/ModularForms/JacobiTheta/Basic.lean

@@ -79,7 +79,7 @@ theorem jacobiTheta_two_add (z : ℂ) : jacobiTheta (2 + z) = jacobiTheta z := b
 
 theorem jacobiTheta_T_sq_smul (τ : ℍ) : jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta τ := by
   suffices ↑(ModularGroup.T ^ 2 • τ) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
-  have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := by rfl
+  have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl
   simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
   norm_cast
 set_option linter.uppercaseLean3 false in

Mathlib/RingTheory/Polynomial/Basic.lean

@@ -898,7 +898,7 @@ protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNo
       ⟨s, le_antisymm (Ideal.span_le.2 fun x hx =>
           have : x ∈ I.degreeLE N := hs ▸ Submodule.subset_span hx
           this.2) <| by
-        have : Submodule.span R[X] ↑s = Ideal.span ↑s := by rfl
+        have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl
         rw [this]
         intro p hp
         generalize hn : p.natDegree = k

Mathlib/RingTheory/Valuation/Basic.lean

@@ -132,12 +132,12 @@ directly. -/
 -- instance : CoeFun (Valuation R Γ₀) fun _ => R → Γ₀ :=
   -- FunLike.hasCoeToFun
 
-theorem toFun_eq_coe (v : Valuation R Γ₀) : v.toFun = v := by rfl
+theorem toFun_eq_coe (v : Valuation R Γ₀) : v.toFun = v := rfl
 #align valuation.to_fun_eq_coe Valuation.toFun_eq_coe
 
 @[simp] --Porting note: requested by simpNF as toFun_eq_coe LHS simplifies
 theorem toMonoidWithZeroHom_coe_eq_coe (v : Valuation R Γ₀) : (v.toMonoidWithZeroHom : R → Γ₀) = v
-    := by rfl
+    := rfl
 
 @[ext]
 theorem ext {v₁ v₂ : Valuation R Γ₀} (h : ∀ r, v₁ r = v₂ r) : v₁ = v₂ :=

Mathlib/RingTheory/Valuation/ValuationSubring.lean

@@ -709,7 +709,7 @@ def principalUnitGroupEquiv :
       rw [A.coe_mem_principalUnitGroup_iff]; simpa using SetLike.coe_mem x⟩
   left_inv x := by simp
   right_inv x := by simp
-  map_mul' x y := by rfl
+  map_mul' x y := rfl
 #align valuation_subring.principal_unit_group_equiv ValuationSubring.principalUnitGroupEquiv
 
 @[simp]

Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

@@ -192,7 +192,7 @@ private theorem candidates_lipschitz_aux (fA : f ∈ candidates X Y) :
     _ = 2 * maxVar X Y * max (dist x z) (dist y t) := by
       rw [dist_comm t y]
       ring
-    _ = 2 * maxVar X Y * dist (x, y) (z, t) := by rfl
+    _ = 2 * maxVar X Y * dist (x, y) (z, t) := rfl
 
 /-- Candidates are Lipschitz -/
 private theorem candidates_lipschitz (fA : f ∈ candidates X Y) :

test/toAdditive.lean

@@ -90,12 +90,12 @@ theorem bar9_works : bar9 = 1 := by decide
 @[to_additive bar10]
 def foo10 (n m : ℕ) := HPow.hPow n m + n * m * 2 + 1 * 0 + 37 * 1 + 2
 
-theorem bar10_works : bar10 = foo10 := by rfl
+theorem bar10_works : bar10 = foo10 := rfl
 
 @[to_additive bar11]
 def foo11 (n : ℕ) (m : ℤ) := n * m * 2 + 1 * 0 + 37 * 1 + 2
 
-theorem bar11_works : bar11 = foo11 := by rfl
+theorem bar11_works : bar11 = foo11 := rfl
 
 @[to_additive bar12]
 def foo12 (_ : Nat) (_ : Int) : Fin 37 := ⟨2, by decide⟩