bump to nightly-2023-05-28-04

mathlib commit leanprover-community/mathlib@917c3c0

Mathbin/Algebra/Algebra/Basic.lean

@@ -398,8 +398,7 @@ theorem algebra_ext {R : Type _} [CommSemiring R] {A : Type _} [Semiring A] (P Q
           haveI := Q
           algebraMap R A r) :
     P = Q := by
-  rcases P with @⟨⟨P⟩⟩
-  rcases Q with @⟨⟨Q⟩⟩
+  rcases P with @⟨⟨P⟩⟩; rcases Q with @⟨⟨Q⟩⟩
   congr
   · funext r a
     replace w := congr_arg (fun s => s * a) (w r)
@@ -633,10 +632,8 @@ but is expected to have type
   forall {R : Type.{u1}} {A : Type.{u2}}, (Nat -> R -> A) -> Nat -> (List.{u1} R) -> (List.{u2} A)
 Case conversion may be inaccurate. Consider using '#align algebra.bit1_smul_bit1 [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit1 r • bit1 a = r • bit0 (bit1 a) + bit1 a :=
-  by
-  simp only [bit0, bit1, add_smul, smul_add, one_smul]
-  abel
+theorem [anonymous] : bit1 r • bit1 a = r • bit0 (bit1 a) + bit1 a := by
+  simp only [bit0, bit1, add_smul, smul_add, one_smul]; abel
 #align algebra.bit1_smul_bit1 [anonymous]
 
 end
@@ -936,9 +933,7 @@ instance : Algebra R Aᵐᵒᵖ :=
       R with
     toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _
     smul_def' := fun c x =>
-      unop_injective <| by
-        dsimp
-        simp only [op_mul, Algebra.smul_def, Algebra.commutes, op_unop]
+      unop_injective <| by dsimp; simp only [op_mul, Algebra.smul_def, Algebra.commutes, op_unop]
     commutes' := fun r =>
       MulOpposite.rec' fun x => by dsimp <;> simp only [← op_mul, Algebra.commutes] }
 
@@ -1108,9 +1103,7 @@ instance (priority := 99) algebraNat : Algebra ℕ R
 
 #print nat_algebra_subsingleton /-
 instance nat_algebra_subsingleton : Subsingleton (Algebra ℕ R) :=
-  ⟨fun P Q => by
-    ext
-    simp⟩
+  ⟨fun P Q => by ext; simp⟩
 #align nat_algebra_subsingleton nat_algebra_subsingleton
 -/
 
@@ -1213,9 +1206,7 @@ but is expected to have type
   forall {R : Type.{u1}} [_inst_1 : Ring.{u1} R], Subsingleton.{succ u1} (Algebra.{0, u1} Int R Int.instCommSemiringInt (Ring.toSemiring.{u1} R _inst_1))
 Case conversion may be inaccurate. Consider using '#align int_algebra_subsingleton int_algebra_subsingletonₓ'. -/
 instance int_algebra_subsingleton : Subsingleton (Algebra ℤ R) :=
-  ⟨fun P Q => by
-    ext
-    simp⟩
+  ⟨fun P Q => by ext; simp⟩
 #align int_algebra_subsingleton int_algebra_subsingleton
 
 end Int
@@ -1254,10 +1245,7 @@ but is expected to have type
 Case conversion may be inaccurate. Consider using '#align no_zero_smul_divisors.algebra_map_injective NoZeroSMulDivisors.algebraMap_injectiveₓ'. -/
 theorem algebraMap_injective [CommRing R] [Ring A] [Nontrivial A] [Algebra R A]
     [NoZeroSMulDivisors R A] : Function.Injective (algebraMap R A) :=
-  suffices Function.Injective fun c : R => c • (1 : A)
-    by
-    convert this
-    ext
+  suffices Function.Injective fun c : R => c • (1 : A) by convert this; ext;
     rw [Algebra.smul_def, mul_one]
   smul_left_injective R one_ne_zero
 #align no_zero_smul_divisors.algebra_map_injective NoZeroSMulDivisors.algebraMap_injective

Mathbin/Algebra/Algebra/Bilinear.lean

@@ -189,15 +189,9 @@ Case conversion may be inaccurate. Consider using '#align non_unital_alg_hom.lmu
 
 A weaker version of this for non-unital non-associative algebras exists as `linear_map.mul`. -/
 def NonUnitalAlgHom.lmul : A →ₙₐ[R] End R A :=
-  {
-    mul R A with
-    map_mul' := by
-      intro a b
-      ext c
-      exact mul_assoc a b c
-    map_zero' := by
-      ext a
-      exact MulZeroClass.zero_mul a }
+  { mul R A with
+    map_mul' := by intro a b; ext c; exact mul_assoc a b c
+    map_zero' := by ext a; exact MulZeroClass.zero_mul a }
 #align non_unital_alg_hom.lmul NonUnitalAlgHom.lmul
 
 variable {R A}
@@ -213,29 +207,23 @@ theorem NonUnitalAlgHom.coe_lmul_eq_mul : ⇑(NonUnitalAlgHom.lmul R A) = mul R
 /- warning: linear_map.commute_mul_left_right -> LinearMap.commute_mulLeft_right is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align linear_map.commute_mul_left_right LinearMap.commute_mulLeft_rightₓ'. -/
-theorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b) :=
-  by
-  ext c
+theorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b) := by ext c;
   exact (mul_assoc a c b).symm
 #align linear_map.commute_mul_left_right LinearMap.commute_mulLeft_right
 
 /- warning: linear_map.mul_left_mul -> LinearMap.mulLeft_mul is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align linear_map.mul_left_mul LinearMap.mulLeft_mulₓ'. -/
 @[simp]
-theorem mulLeft_mul (a b : A) : mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b) :=
-  by
-  ext
+theorem mulLeft_mul (a b : A) : mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b) := by ext;
   simp only [mul_left_apply, comp_apply, mul_assoc]
 #align linear_map.mul_left_mul LinearMap.mulLeft_mul
 
 /- warning: linear_map.mul_right_mul -> LinearMap.mulRight_mul is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align linear_map.mul_right_mul LinearMap.mulRight_mulₓ'. -/
 @[simp]
-theorem mulRight_mul (a b : A) : mulRight R (a * b) = (mulRight R b).comp (mulRight R a) :=
-  by
-  ext
+theorem mulRight_mul (a b : A) : mulRight R (a * b) = (mulRight R b).comp (mulRight R a) := by ext;
   simp only [mul_right_apply, comp_apply, mul_assoc]
 #align linear_map.mul_right_mul LinearMap.mulRight_mul
 
@@ -256,23 +244,11 @@ the algebra.
 
 A weaker version of this for non-unital algebras exists as `non_unital_alg_hom.mul`. -/
 def Algebra.lmul : A →ₐ[R] End R A :=
-  {
-    LinearMap.mul R
-      A with
-    map_one' := by
-      ext a
-      exact one_mul a
-    map_mul' := by
-      intro a b
-      ext c
-      exact mul_assoc a b c
-    map_zero' := by
-      ext a
-      exact MulZeroClass.zero_mul a
-    commutes' := by
-      intro r
-      ext a
-      exact (Algebra.smul_def r a).symm }
+  { LinearMap.mul R A with
+    map_one' := by ext a; exact one_mul a
+    map_mul' := by intro a b; ext c; exact mul_assoc a b c
+    map_zero' := by ext a; exact MulZeroClass.zero_mul a
+    commutes' := by intro r; ext a; exact (Algebra.smul_def r a).symm }
 #align algebra.lmul Algebra.lmul
 
 variable {R A}
@@ -295,8 +271,7 @@ theorem mulLeft_eq_zero_iff (a : A) : mulLeft R a = 0 ↔ a = 0 :=
   by
   constructor <;> intro h
   · rw [← mul_one a, ← mul_left_apply a 1, h, LinearMap.zero_apply]
-  · rw [h]
-    exact mul_left_zero_eq_zero
+  · rw [h]; exact mul_left_zero_eq_zero
 #align linear_map.mul_left_eq_zero_iff LinearMap.mulLeft_eq_zero_iff
 
 /- warning: linear_map.mul_right_eq_zero_iff -> LinearMap.mulRight_eq_zero_iff is a dubious translation:
@@ -310,24 +285,19 @@ theorem mulRight_eq_zero_iff (a : A) : mulRight R a = 0 ↔ a = 0 :=
   by
   constructor <;> intro h
   · rw [← one_mul a, ← mul_right_apply a 1, h, LinearMap.zero_apply]
-  · rw [h]
-    exact mul_right_zero_eq_zero
+  · rw [h]; exact mul_right_zero_eq_zero
 #align linear_map.mul_right_eq_zero_iff LinearMap.mulRight_eq_zero_iff
 
 #print LinearMap.mulLeft_one /-
 @[simp]
-theorem mulLeft_one : mulLeft R (1 : A) = LinearMap.id :=
-  by
-  ext
+theorem mulLeft_one : mulLeft R (1 : A) = LinearMap.id := by ext;
   simp only [LinearMap.id_coe, one_mul, id.def, mul_left_apply]
 #align linear_map.mul_left_one LinearMap.mulLeft_one
 -/
 
 #print LinearMap.mulRight_one /-
 @[simp]
-theorem mulRight_one : mulRight R (1 : A) = LinearMap.id :=
-  by
-  ext
+theorem mulRight_one : mulRight R (1 : A) = LinearMap.id := by ext;
   simp only [LinearMap.id_coe, mul_one, id.def, mul_right_apply]
 #align linear_map.mul_right_one LinearMap.mulRight_one
 -/

Mathbin/Algebra/Algebra/Equiv.lean

@@ -111,10 +111,7 @@ instance : AlgEquivClass (A₁ ≃ₐ[R] A₂) R A₁ A₂
     where
   coe := toFun
   inv := invFun
-  coe_injective' f g h₁ h₂ := by
-    cases f
-    cases g
-    congr
+  coe_injective' f g h₁ h₂ := by cases f; cases g; congr
   map_add := map_add'
   map_mul := map_mul'
   commutes := commutes'
@@ -410,10 +407,8 @@ def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
   { e.toRingEquiv.symm with
     commutes' := fun r =>
       by
-      rw [← e.to_ring_equiv.symm_apply_apply (algebraMap R A₁ r)]
-      congr
-      change _ = e _
-      rw [e.commutes] }
+      rw [← e.to_ring_equiv.symm_apply_apply (algebraMap R A₁ r)]; congr
+      change _ = e _; rw [e.commutes] }
 #align alg_equiv.symm AlgEquiv.symm
 -/
 
@@ -454,10 +449,7 @@ theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
 
 #print AlgEquiv.symm_symm /-
 @[simp]
-theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e :=
-  by
-  ext
-  rfl
+theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e := by ext; rfl
 #align alg_equiv.symm_symm AlgEquiv.symm_symm
 -/
 
@@ -567,20 +559,16 @@ theorem trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x
 <too large>
 Case conversion may be inaccurate. Consider using '#align alg_equiv.comp_symm AlgEquiv.comp_symmₓ'. -/
 @[simp]
-theorem comp_symm (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂ :=
-  by
-  ext
-  simp
+theorem comp_symm (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂ := by
+  ext; simp
 #align alg_equiv.comp_symm AlgEquiv.comp_symm
 
 /- warning: alg_equiv.symm_comp -> AlgEquiv.symm_comp is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align alg_equiv.symm_comp AlgEquiv.symm_compₓ'. -/
 @[simp]
-theorem symm_comp (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁ :=
-  by
-  ext
-  simp
+theorem symm_comp (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = AlgHom.id R A₁ := by
+  ext; simp
 #align alg_equiv.symm_comp AlgEquiv.symm_comp
 
 /- warning: alg_equiv.left_inverse_symm -> AlgEquiv.leftInverse_symm is a dubious translation:
@@ -622,18 +610,14 @@ theorem arrowCongr_comp {A₁' A₂' A₃' : Type _} [Semiring A₁'] [Semiring
     (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃) :
     arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) :=
   by
-  ext
-  simp only [arrow_congr, Equiv.coe_fn_mk, AlgHom.comp_apply]
-  congr
-  exact (e₂.symm_apply_apply _).symm
+  ext; simp only [arrow_congr, Equiv.coe_fn_mk, AlgHom.comp_apply]
+  congr ; exact (e₂.symm_apply_apply _).symm
 #align alg_equiv.arrow_congr_comp AlgEquiv.arrowCongr_comp
 
 #print AlgEquiv.arrowCongr_refl /-
 @[simp]
-theorem arrowCongr_refl : arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂) :=
-  by
-  ext
-  rfl
+theorem arrowCongr_refl : arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ →ₐ[R] A₂) := by
+  ext; rfl
 #align alg_equiv.arrow_congr_refl AlgEquiv.arrowCongr_refl
 -/
 
@@ -644,10 +628,8 @@ Case conversion may be inaccurate. Consider using '#align alg_equiv.arrow_congr_
 theorem arrowCongr_trans {A₁' A₂' A₃' : Type _} [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
     [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂')
     (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃') :
-    arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') :=
-  by
-  ext
-  rfl
+    arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') := by
+  ext; rfl
 #align alg_equiv.arrow_congr_trans AlgEquiv.arrowCongr_trans
 
 /- warning: alg_equiv.arrow_congr_symm -> AlgEquiv.arrowCongr_symm is a dubious translation:
@@ -656,10 +638,7 @@ Case conversion may be inaccurate. Consider using '#align alg_equiv.arrow_congr_
 @[simp]
 theorem arrowCongr_symm {A₁' A₂' : Type _} [Semiring A₁'] [Semiring A₂'] [Algebra R A₁']
     [Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
-    (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm :=
-  by
-  ext
-  rfl
+    (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm := by ext; rfl
 #align alg_equiv.arrow_congr_symm AlgEquiv.arrowCongr_symm
 
 #print AlgEquiv.ofAlgHom /-
@@ -839,20 +818,15 @@ theorem ofLinearEquiv_symm :
 Case conversion may be inaccurate. Consider using '#align alg_equiv.of_linear_equiv_to_linear_equiv AlgEquiv.ofLinearEquiv_toLinearEquivₓ'. -/
 @[simp]
 theorem ofLinearEquiv_toLinearEquiv (map_mul) (commutes) :
-    ofLinearEquiv e.toLinearEquiv map_mul commutes = e :=
-  by
-  ext
-  rfl
+    ofLinearEquiv e.toLinearEquiv map_mul commutes = e := by ext; rfl
 #align alg_equiv.of_linear_equiv_to_linear_equiv AlgEquiv.ofLinearEquiv_toLinearEquiv
 
 /- warning: alg_equiv.to_linear_equiv_of_linear_equiv -> AlgEquiv.toLinearEquiv_ofLinearEquiv is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align alg_equiv.to_linear_equiv_of_linear_equiv AlgEquiv.toLinearEquiv_ofLinearEquivₓ'. -/
 @[simp]
-theorem toLinearEquiv_ofLinearEquiv : toLinearEquiv (ofLinearEquiv l map_mul commutes) = l :=
-  by
-  ext
-  rfl
+theorem toLinearEquiv_ofLinearEquiv : toLinearEquiv (ofLinearEquiv l map_mul commutes) = l := by
+  ext; rfl
 #align alg_equiv.to_linear_equiv_of_linear_equiv AlgEquiv.toLinearEquiv_ofLinearEquiv
 
 end OfLinearEquiv
@@ -915,15 +889,9 @@ def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ
     where
   toFun ψ := ϕ.symm.trans (ψ.trans ϕ)
   invFun ψ := ϕ.trans (ψ.trans ϕ.symm)
-  left_inv ψ := by
-    ext
-    simp_rw [trans_apply, symm_apply_apply]
-  right_inv ψ := by
-    ext
-    simp_rw [trans_apply, apply_symm_apply]
-  map_mul' ψ χ := by
-    ext
-    simp only [mul_apply, trans_apply, symm_apply_apply]
+  left_inv ψ := by ext; simp_rw [trans_apply, symm_apply_apply]
+  right_inv ψ := by ext; simp_rw [trans_apply, apply_symm_apply]
+  map_mul' ψ χ := by ext; simp only [mul_apply, trans_apply, symm_apply_apply]
 #align alg_equiv.aut_congr AlgEquiv.autCongr
 
 /- warning: alg_equiv.aut_congr_refl -> AlgEquiv.autCongr_refl is a dubious translation:
@@ -933,10 +901,7 @@ but is expected to have type
   forall {R : Type.{u1}} {A₁ : Type.{u2}} [_inst_1 : CommSemiring.{u1} R] [_inst_2 : Semiring.{u2} A₁] [_inst_5 : Algebra.{u1, u2} R A₁ _inst_1 _inst_2], Eq.{succ u2} (MulEquiv.{u2, u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (MulOneClass.toMul.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Monoid.toMulOneClass.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (DivInvMonoid.toMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Group.toDivInvMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (AlgEquiv.aut.{u1, u2} R A₁ _inst_1 _inst_2 _inst_5))))) (MulOneClass.toMul.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Monoid.toMulOneClass.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (DivInvMonoid.toMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Group.toDivInvMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (AlgEquiv.aut.{u1, u2} R A₁ _inst_1 _inst_2 _inst_5)))))) (AlgEquiv.autCongr.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5 (AlgEquiv.refl.{u1, u2} R A₁ _inst_1 _inst_2 _inst_5)) (MulEquiv.refl.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (MulOneClass.toMul.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Monoid.toMulOneClass.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (DivInvMonoid.toMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (Group.toDivInvMonoid.{u2} (AlgEquiv.{u1, u2, u2} R A₁ A₁ _inst_1 _inst_2 _inst_2 _inst_5 _inst_5) (AlgEquiv.aut.{u1, u2} R A₁ _inst_1 _inst_2 _inst_5))))))
 Case conversion may be inaccurate. Consider using '#align alg_equiv.aut_congr_refl AlgEquiv.autCongr_reflₓ'. -/
 @[simp]
-theorem autCongr_refl : autCongr AlgEquiv.refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁) :=
-  by
-  ext
-  rfl
+theorem autCongr_refl : autCongr AlgEquiv.refl = MulEquiv.refl (A₁ ≃ₐ[R] A₁) := by ext; rfl
 #align alg_equiv.aut_congr_refl AlgEquiv.autCongr_refl
 
 /- warning: alg_equiv.aut_congr_symm -> AlgEquiv.autCongr_symm is a dubious translation:

Mathbin/Algebra/Algebra/Hom.lean

@@ -119,10 +119,7 @@ theorem toFun_eq_coe (f : A →ₐ[R] B) : f.toFun = f :=
 instance : AlgHomClass (A →ₐ[R] B) R A B
     where
   coe := toFun
-  coe_injective' f g h := by
-    cases f
-    cases g
-    congr
+  coe_injective' f g h := by cases f; cases g; congr
   map_add := map_add'
   map_zero := map_zero'
   map_mul := map_mul'
@@ -514,21 +511,15 @@ def ofLinearMap (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ x y, f (x
 Case conversion may be inaccurate. Consider using '#align alg_hom.of_linear_map_to_linear_map AlgHom.ofLinearMap_toLinearMapₓ'. -/
 @[simp]
 theorem ofLinearMap_toLinearMap (map_one) (map_mul) :
-    ofLinearMap φ.toLinearMap map_one map_mul = φ :=
-  by
-  ext
-  rfl
+    ofLinearMap φ.toLinearMap map_one map_mul = φ := by ext; rfl
 #align alg_hom.of_linear_map_to_linear_map AlgHom.ofLinearMap_toLinearMap
 
 /- warning: alg_hom.to_linear_map_of_linear_map -> AlgHom.toLinearMap_ofLinearMap is a dubious translation:
 <too large>
 Case conversion may be inaccurate. Consider using '#align alg_hom.to_linear_map_of_linear_map AlgHom.toLinearMap_ofLinearMapₓ'. -/
 @[simp]
 theorem toLinearMap_ofLinearMap (f : A →ₗ[R] B) (map_one) (map_mul) :
-    toLinearMap (ofLinearMap f map_one map_mul) = f :=
-  by
-  ext
-  rfl
+    toLinearMap (ofLinearMap f map_one map_mul) = f := by ext; rfl
 #align alg_hom.to_linear_map_of_linear_map AlgHom.toLinearMap_ofLinearMap
 
 /- warning: alg_hom.of_linear_map_id -> AlgHom.ofLinearMap_id is a dubious translation: