diff --git a/BrauerGroup/AlgClosedUnion.lean b/BrauerGroup/AlgClosedUnion.lean
index e3c5cf8..7f74091 100644
--- a/BrauerGroup/AlgClosedUnion.lean
+++ b/BrauerGroup/AlgClosedUnion.lean
@@ -1,6 +1,7 @@
 module
 
 public import Mathlib.FieldTheory.IsAlgClosed.Basic
+public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
 public import Mathlib.RingTheory.Flat.Basic
 public import Mathlib.RingTheory.TensorProduct.Free
 
diff --git a/BrauerGroup/Azumaya/Basic.lean b/BrauerGroup/Azumaya/Basic.lean
index 0b1703f..fce80eb 100644
--- a/BrauerGroup/Azumaya/Basic.lean
+++ b/BrauerGroup/Azumaya/Basic.lean
@@ -57,15 +57,14 @@ lemma IsCentral.left_of_tensor (B C : Type*)
       map_zero' := by ext; simp
       map_add' := fun _ _ ↦ by ext; simp [add_tmul]
       commutes' := fun _ ↦ rfl}
-  have f_surj : Function.Surjective f := fun ⟨bc, ⟨b, hb⟩, h⟩ ↦ ⟨⟨b, hb⟩, by simpa [f] using h⟩
+  have f_surj : Function.Surjective f := fun ⟨bc, ⟨b, hb⟩, h⟩ ↦ ⟨⟨b, hb⟩, Subtype.ext h⟩
   have e : ((Algebra.TensorProduct.includeLeft (R := K) (B := C)).comp
     (Subalgebra.center K B).val).range ≃ₐ[K] (Subalgebra.center K B) :=
     (AlgEquiv.ofBijective f
     ⟨fun ⟨b1, hb1⟩ ⟨b2, hb2⟩ h12 ↦ by
-      simp only [AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
-        Subtype.mk.injEq, f] at h12
+      have h12' : b1 ⊗ₜ[K] (1 : C) = b2 ⊗ₜ[K] (1 : C) := congrArg Subtype.val h12
       ext
-      exact TensorProduct.flip_mk_injective _ one_ne_zero h12,
+      exact TensorProduct.flip_mk_injective (R := K) (1 : C) one_ne_zero h12',
     f_surj⟩).symm
   have e2 := Subalgebra.equivOfEq _ _ eq |>.trans <| Algebra.botEquiv K _
   have ee: Subalgebra.center K B ≃ₐ[K] K := e.symm.trans e2
@@ -185,6 +184,7 @@ abbrev matrixAlgEquivMatrixMop (n : ℕ) :
 noncomputable abbrev mopAlgEquivEnd : Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=
   AlgEquiv.ofRingEquiv (f := mopEquivEnd R) fun r ↦ by
     ext; simp [mopEquivEnd]
+    erw [RingEquiv.ofBijective_apply]; simp
 
 noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=
   Algebra.TensorProduct.lid R Rᵐᵒᵖ|>.trans <| mopAlgEquivEnd R
@@ -192,6 +192,7 @@ noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R
 lemma equal_mulLeftRight : tensorEquivEnd R = AlgHom.mulLeftRight R R := by
   ext r
   simp [mopEquivEnd, AlgHom.mulLeftRight_apply]
+  erw [RingEquiv.ofBijective_apply]; simp
 
 lemma bij_Rtensor : Function.Bijective (AlgHom.mulLeftRight R R) := by
   rw [← equal_mulLeftRight]
diff --git a/BrauerGroup/Azumaya/Group.lean b/BrauerGroup/Azumaya/Group.lean
index 3f450d0..09acf02 100644
--- a/BrauerGroup/Azumaya/Group.lean
+++ b/BrauerGroup/Azumaya/Group.lean
@@ -28,7 +28,9 @@ abbrev Endmop (A : Type*) [Ring A] [Algebra R A] : Module.End R A →ₐ[R] Modu
 
 abbrev EndmopEquiv (A : Type*) [Ring A] [Algebra R A] : Module.End R A ≃ₐ[R] Module.End R Aᵐᵒᵖ :=
   AlgEquiv.ofBijective (Endmop R A) ⟨
-  fun f1 f2 h ↦ by simpa using h, fun f ↦ ⟨(opLinearEquiv R).symm.toLinearMap ∘ₗ f ∘ₗ
+  fun f1 f2 h ↦ by
+    ext x
+    exact congrArg (fun g ↦ (g (MulOpposite.op x)).unop) h, fun f ↦ ⟨(opLinearEquiv R).symm.toLinearMap ∘ₗ f ∘ₗ
     (opLinearEquiv R).toLinearMap, rfl⟩⟩
 
 
@@ -57,7 +59,13 @@ lemma Mopcomm_square (A : Type*) [Ring A] [Algebra R A] :
     (Algebra.TensorProduct.congr (AlgEquiv.refl) (AlgEquiv.opOp R A).symm).toAlgHom) := by
   ext a a'
   · simp [-Algebra.lsmul_coe, AlgHom.mulLeftRight_apply]
+    erw [AlgEquiv.ofBijective_apply]
+    change a * a' = MulOpposite.op ((AlgHom.mulLeftRight R A (1 ⊗ₜ[R] a)) a'.unop)
+    simp [AlgHom.mulLeftRight_apply]
   · simp [-Algebra.lsmul_coe, AlgHom.mulLeftRight_apply]
+    erw [AlgEquiv.ofBijective_apply]
+    change a' * a.unop = MulOpposite.op ((AlgHom.mulLeftRight R A (a.unop.unop ⊗ₜ[R] 1)) a'.unop)
+    simp [AlgHom.mulLeftRight_apply]
 
 lemma mop_bij (A : Azumaya R) : Function.Bijective (AlgHom.mulLeftRight R Aᵐᵒᵖ) := by
   rw [Mopcomm_square R A]
diff --git a/BrauerGroup/BrauerGroup.lean b/BrauerGroup/BrauerGroup.lean
index 804f9de..fb9a57a 100644
--- a/BrauerGroup/BrauerGroup.lean
+++ b/BrauerGroup/BrauerGroup.lean
@@ -323,11 +323,8 @@ lemma matrixEquivForward_surjective
   simp only [matrixEquivForward, Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply,
     TensorProduct.lift.tmul]
   ext a b
-  erw [Matrix.kroneckerMapBilinear_apply_apply]
-  erw [Matrix.kroneckerMap_apply]
-  erw [Algebra.coe_lmul_eq_mul]
-  rw [LinearMap.mul]
-  simp only [LinearMap.mk₂_apply]
+  change Matrix.kroneckerMap (· * ·) (Matrix.single i.1 j.1 (1 : K)) (Matrix.single i.2 j.2 (1 : K)) a b = _
+  rw [Matrix.kroneckerMap_apply]
   simp only [Matrix.single, Matrix.of_apply, mul_ite, mul_one, mul_zero]
   split_ifs with h1 h2 h3 h4 h5
   · rfl
@@ -767,14 +764,16 @@ def e6Aux0 : (E ⊗[K] A) ⊗[E] (E ⊗[K] B) →ₐ[E] E ⊗[K] (A ⊗[K] B) :=
         | zero => simp only [map_zero, zero_mul, mul_zero]
         | add x x' hx hx' => simp only [map_add, mul_add, hx, hx', add_mul]
         | tmul e a =>
-        simp only [Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk]
+        erw [Algebra.TensorProduct.lift_tmul]
         induction y using TensorProduct.induction_on with
         | zero => simp only [map_zero, mul_zero, zero_mul]
         | add y y' hy hy' => simp only [map_add, mul_add, hy, hy', add_mul]
         | tmul e' b =>
-        simp only [Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk]
-        change (_ ⊗ₜ _) * (_ ⊗ₜ _) * ((_ ⊗ₜ _) * (_ ⊗ₜ _))
-          = (_ ⊗ₜ _) * (_ ⊗ₜ _) * ((_ ⊗ₜ _) * (_ ⊗ₜ _))
+        erw [Algebra.TensorProduct.lift_tmul]
+        change (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B))) *
+            (e' ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) =
+          (e' ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) *
+            (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B)))
         simp only [Algebra.TensorProduct.tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
         rw [mul_comm]
 
@@ -807,7 +806,8 @@ def e6 [Algebra.IsCentral K A] [csa_A : IsSimpleRing A]
     refine ⟨(e ⊗ₜ a) ⊗ₜ[E] (1 ⊗ₜ b), ?_⟩
     simp only [e6Aux0, Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk,
       _root_.one_mul, map_one];
-    change e ⊗ₜ[K] (1 ⊗ₜ[K] 1) * 1 ⊗ₜ[K] (a ⊗ₜ[K] 1) * 1 ⊗ₜ[K] (1 ⊗ₜ[K] b) = _
+    change (e ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] (a ⊗ₜ[K] (1 : B))) *
+      ((1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] (1 : B)) * (1 : E) ⊗ₜ[K] ((1 : A) ⊗ₜ[K] b)) = _
     simp only [Algebra.TensorProduct.tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
 
 def e7 : E ≃ₐ[E] (E ⊗[K] K) := .symm <| Algebra.TensorProduct.rid _ _ _
diff --git a/BrauerGroup/BrauerOverR.lean b/BrauerGroup/BrauerOverR.lean
index 31ecd0a..b411cb1 100644
--- a/BrauerGroup/BrauerOverR.lean
+++ b/BrauerGroup/BrauerOverR.lean
@@ -233,12 +233,19 @@ abbrev C2toBrauerOverR : ZMod 2 →+ Additive (BrauerGroup ℝ) where
 
 lemma toC2.left_inv : Function.LeftInverse C2toBrauerOverR toC2 := fun A ↦ by
   induction A using Quotient.inductionOn' with | h A
+  classical
+  simp only [AddMonoidHom.coe_mk, dite_eq_ite, ZeroHom.coe_mk]
   obtain h1 | h2 := BrauerOverR A
   · change IsBrauerEquivalent A one_in' at h1
-    simp only [AddMonoidHom.coe_mk, dite_eq_ite, ZeroHom.coe_mk, Quotient.lift_mk, h1, ↓reduceIte]
-    rw [Quotient.sound']; exact h1.symm
+    refine (dif_pos ?_).trans ?_
+    · change (if IsBrauerEquivalent A one_in' then (0 : ZMod 2) else 1) = 0
+      simp [h1]
+    · exact Quotient.sound' h1.symm
   · have : ¬ (IsBrauerEquivalent A one_in') := fun h ↦ QuaternionNotEquivR <| h2.symm.trans h
-    simpa [this] using! Quotient.sound' h2.symm
+    refine (dif_neg ?_).trans ?_
+    · change ¬ ((if IsBrauerEquivalent A one_in' then (0 : ZMod 2) else 1) = 0)
+      simp [this]
+    · exact Quotient.sound' h2.symm
 
 set_option backward.isDefEq.respectTransparency false in
 lemma toC2.right_inv : Function.RightInverse C2toBrauerOverR toC2 := fun x ↦ by
diff --git a/BrauerGroup/CSA/ReducedCharPoly.lean b/BrauerGroup/CSA/ReducedCharPoly.lean
index 1a449bc..f16d52a 100644
--- a/BrauerGroup/CSA/ReducedCharPoly.lean
+++ b/BrauerGroup/CSA/ReducedCharPoly.lean
@@ -45,9 +45,9 @@ variable {K F E} in
 def φ_m (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) F →ₐ[K] Matrix (Fin n) (Fin n) E where
   toFun M := fun i j ↦ φ (M i j)
   map_one' := by ext i j; simp [Matrix.one_apply]
-  map_mul' M1 M2 := by ext i j; simp [Matrix.mul_apply]
+  map_mul' M1 M2 := by ext i j; simp [Matrix.mul_apply]; try rfl
   map_zero' := by ext; simp
-  map_add' M1 M2 := by ext; simp
+  map_add' M1 M2 := by ext; simp; try rfl
   commutes' k := by
     ext i j
     simp [Matrix.algebraMap_matrix_apply]
@@ -62,9 +62,9 @@ variable {K F E} in
 abbrev e1Aux (φ : F →ₐ[K] E) : Matrix (Fin n) (Fin n) φ.range ≃ₐ[K] (φ_m n φ).range where
   toFun M := ⟨(M · · |>.1), fun i j ↦ M i j |>.2.choose, by ext i j; exact M i j|>.2.choose_spec⟩
   invFun := fun ⟨M, h⟩ i j ↦ ⟨M i j, h.choose i j, Matrix.ext_iff.2 h.choose_spec i j⟩
-  left_inv _ := by simp
+  left_inv _ := by simp; try rfl
   right_inv _ := by simp
-  map_mul' _ _ := by ext; simp [Matrix.mul_apply]
+  map_mul' _ _ := by ext; simp [Matrix.mul_apply]; try rfl
   map_add' _ _ := rfl
   commutes' k := by
     ext
@@ -122,6 +122,7 @@ lemma mat_over_extension (φ : F →ₐ[K] E) (a : A) :
     AlgHom.mapMatrix_apply]
   ext i j
   simp [Matrix.map_apply]
+  try rfl
 
 variable {K F n A} in
 def ReducedCharPoly (a : A) : Polynomial F := Matrix.charpoly (e (1 ⊗ₜ a)) -- elements in F[X]
diff --git a/BrauerGroup/DoubleCentralizer.lean b/BrauerGroup/DoubleCentralizer.lean
index 602f8ff..451bf51 100644
--- a/BrauerGroup/DoubleCentralizer.lean
+++ b/BrauerGroup/DoubleCentralizer.lean
@@ -209,9 +209,9 @@ lemma centralizer_mulLeft_le_of_isCentralSimple :
       ext x
       simp only [LinearMap.mulLeft_apply]
       simp only [tensor_self_op.equivEnd, tensor_self_op.toEnd, AlgEquiv.coe_ofBijective,
-        Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk,
-        OneHom.coe_mk, MulOpposite.unop_one, mul_one, Module.End.mul_apply, LinearMap.coe_mk,
-        AddHom.coe_mk, eqv] ]
+        eqv]
+      erw [Algebra.TensorProduct.lift_tmul]
+      simp ]
     ext b
     simp only [Module.End.mul_apply, LinearMap.mulLeft_apply]
     -- change y * (eqv (eqv.symm x)) b = (eqv (eqv.symm x)) (y * b)
@@ -258,9 +258,9 @@ lemma centralizer_mulLeft_le_of_isCentralSimple :
   refine ⟨y.unop, ?_⟩
   ext c
   simp only [LinearMap.mulRight_apply, tensor_self_op.equivEnd, tensor_self_op.toEnd,
-    AlgEquiv.coe_ofBijective, Algebra.TensorProduct.lift_tmul, AlgHom.coe_mk, RingHom.coe_mk,
-    MonoidHom.coe_mk, OneHom.coe_mk, one_mul, Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk,
-    eqv]
+    AlgEquiv.coe_ofBijective, eqv]
+  erw [Algebra.TensorProduct.lift_tmul]
+  simp
 
 end central_simple_case
 
@@ -522,8 +522,11 @@ lemma Subalgebra.conj_simple_iff {B : Subalgebra F A} {x : Aˣ} :
         rw [← mul_assoc x⁻¹.1, Units.inv_mul, one_mul])
       (by
         rintro ⟨_, ⟨a, ha, rfl⟩⟩ ⟨_, ⟨b, hb, rfl⟩⟩ ⟨c, hc1, hc2⟩
-        simp only [toConj, AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
-          Subtype.mk.injEq, Units.mul_left_inj, Units.mul_right_inj] at hc2
+        have h1 : (x : A) * c.1 * ((x⁻¹ : Aˣ) : A) = x * a * ((x⁻¹ : Aˣ) : A) := congrArg Subtype.val hc2
+        have h2 : c.1 = a := by
+          have := congrArg (fun z => ((x⁻¹ : Aˣ) : A) * z * (x : A)) h1
+          simpa [mul_assoc] using this
+        replace hc2 : c = ⟨a, ha⟩ := Subtype.ext h2
         refine ⟨⟨a, ha⟩ * ⟨b, hb⟩, J.mul_mem_right _ _ <| by
           simp_rw [← hc2]; exact hc1, ?_⟩
         ext
@@ -773,7 +776,7 @@ lemma finrank_mop (B : Type*) [Ring B] [Algebra F B] : Module.finrank F Bᵐᵒ
 
 end centralizer_isSimple.aux
 
-set_option maxHeartbeats 400000 in
+set_option maxHeartbeats 1600000 in
 -- Unclear
 open centralizer_isSimple.aux in
 lemma centralizer_isSimple {ι : Type*} (ℬ : Basis ι F <| Module.End F B) :
diff --git a/BrauerGroup/MatrixEquivTensor.lean b/BrauerGroup/MatrixEquivTensor.lean
index 60923a8..9309049 100644
--- a/BrauerGroup/MatrixEquivTensor.lean
+++ b/BrauerGroup/MatrixEquivTensor.lean
@@ -33,19 +33,16 @@ abbrev toTensorMatrix_toFun_Klinear : K ⊗[F] Matrix n n A →ₗ[K] Matrix n n
   {__ := toTensorMatrix_toFun_Flinear K F A n,
    map_smul' k tensor := by
     induction tensor with
-    | zero => simp
     | tmul k0 M => simp [TensorProduct.smul_tmul', SemigroupAction.mul_smul]
     | add _ _ h1 h2 => simp_all}
 
 abbrev toTensorMatrix : K ⊗[F] Matrix n n A →ₐ[K] Matrix n n (K ⊗[F] A) := by
   refine .ofLinearMap (toTensorMatrix_toFun_Klinear K F A n)
-    (by simp [Algebra.TensorProduct.one_def]) fun t1 t2 ↦ ?_
+    (by simp [Algebra.TensorProduct.one_def, Matrix.map_one _ (map_zero _) (map_one _)]) fun t1 t2 ↦ ?_
   induction t1 with
-  | zero => simp
   | add _ _ h1 h2 => simp_all [add_mul]
   | tmul x y =>
   induction t2 with
-  | zero => simp
   | add _ _ h1 h2 => simp_all [mul_add]
   | tmul x0 y0 =>
   simp [Algebra.TensorProduct.tmul_mul_tmul, mul_comm x x0, SemigroupAction.mul_smul]
@@ -73,7 +70,6 @@ abbrev invFun_Klinear (i j : n) : K ⊗[F] A →ₗ[K] K ⊗[F] Matrix n n A :=
   {__ := invFun_toFun K F A n i j,
    map_smul' k tensor := by
     induction tensor with
-    | zero => simp
     | tmul k0 a => simp [smul_tmul']
     | add _ _ h1 h2 => simp_all}
 
@@ -85,7 +81,6 @@ abbrev invFun_linearMap : Matrix n n (K ⊗[F] A) →ₗ[K] K ⊗[F] Matrix n n
 lemma left_inv (M : K ⊗[F] Matrix n n A) :
     invFun_linearMap K F A n (toTensorMatrix K F A n M) = M := by
   induction M with
-  | zero => simp
   | tmul k M =>
     simp [← tmul_sum, smul_tmul', Fintype.sum_prod_type, ← matrix_eq_sum_single]
   | add koxa1 koxa2 h1 h2 => rw [map_add, map_add, h1, h2]
@@ -97,7 +92,6 @@ lemma right_inv (M : Matrix n n (K ⊗[F] A)) :
   conv_rhs => rw [matrix_eq_sum_single M]
   refine Finset.sum_congr rfl fun p _ => Finset.sum_congr rfl fun q _ => ?_
   induction M p q with
-  | zero => simp
   | tmul x y => simp [smul_tmul']
   | add _ _ h1 h2 => simp [single_add, h1, h2]
 
diff --git a/BrauerGroup/Morita/ChangeOfRings.lean b/BrauerGroup/Morita/ChangeOfRings.lean
index 0b0c715..4166072 100644
--- a/BrauerGroup/Morita/ChangeOfRings.lean
+++ b/BrauerGroup/Morita/ChangeOfRings.lean
@@ -165,13 +165,20 @@ end  MoritaEquivalence
 
 namespace MoritaEquivalence
 
+section EndHelpers
+variable {C : Type*} [Category C] [Preadditive C] {X : C}
+
+@[simp] lemma end_add_asHom (x y : End X) : (x + y).asHom = x.asHom + y.asHom := rfl
+
+end EndHelpers
+
 variable (A B : Type u) [DivisionRing A] [DivisionRing B] [Algebra R A] [Algebra R B]
 
 instance : Algebra R (End (ModuleCat.of A A)) := inferInstance
 
 @[simps]
 def mopToEnd : Aᵐᵒᵖ →ₐ[R] End (ModuleCat.of A A) where
-  toFun a := ModuleCat.ofHom <|
+  toFun a := End.of <| ModuleCat.ofHom <|
     { toFun := fun (x : A) ↦ x * a.unop
       map_add' := by simp [add_mul]
       map_smul' := by simp [mul_assoc] }
@@ -179,10 +186,12 @@ def mopToEnd : Aᵐᵒᵖ →ₐ[R] End (ModuleCat.of A A) where
   map_one' := by aesop
   map_add' := fun x y => by simp [mul_add]; rfl
   map_mul' := fun (x y) => by
-    simp only [MulOpposite.unop_mul, End.mul_def]
+    simp only [MulOpposite.unop_mul, End.mul_asHom]
+    apply End.ext
     apply ModuleCat.hom_ext
     simp only [ModuleCat.hom_comp]; ext; simp
   commutes' r := by
+    apply End.ext
     apply hom_ext
     ext
     change _ = algebraMap R A r * 1
@@ -217,15 +226,15 @@ set_option backward.isDefEq.respectTransparency false in
 lemma moptoend_bij : Function.Bijective (mopToEnd R A) :=
   ⟨RingHom.injective_iff_ker_eq_bot _ |>.mpr <|
     SetLike.ext fun (α : Aᵐᵒᵖ) => ⟨fun (h : _ = _) => by
-      rw [ModuleCat.hom_ext_iff] at h
+      have h := congrArg (fun φ => φ.asHom.hom) h
       simp only [mopToEnd, hom_zero, LinearMap.ext_iff, LinearMap.zero_apply] at h
       specialize h (1 : A)
       simp_all,
-      by rintro rfl; simp⟩, fun φ => ⟨MulOpposite.op (φ.hom.toFun (1 : A)), ModuleCat.hom_ext <|
+      by rintro rfl; simp⟩, fun φ => ⟨MulOpposite.op (φ.asHom.hom.toFun (1 : A)), End.ext <| ModuleCat.hom_ext <|
       LinearMap.ext fun r ↦ by
-      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, mopToEnd_apply, MulOpposite.unop_op,
+      simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, mopToEnd_apply_asHom, MulOpposite.unop_op,
         hom_ofHom, LinearMap.coe_mk, AddHom.coe_mk]
-      rw [← smul_eq_mul, ← φ.hom.map_smul, smul_eq_mul, mul_one]⟩⟩
+      rw [← smul_eq_mul, ← φ.asHom.hom.map_smul, smul_eq_mul, mul_one]⟩⟩
 
 -- noncomputable def mopEquivEnd : Rᵐᵒᵖ ≃+* End (ModuleCat.of R R) :=
 --   RingEquiv.ofBijective (mopToEnd R) ⟨RingHom.injective_iff_ker_eq_bot _ |>.mpr $
@@ -254,24 +263,26 @@ variable (e : MoritaEquivalence R A B)
 set_option backward.isDefEq.respectTransparency false in
 variable {R S} in
 def aux1 : End (ModuleCat.of A A) ≃ₐ[R] End (e.eqv.functor.obj <| .of A A) where
-  toFun (f : _ ⟶ _) := e.eqv.functor.map f
-  invFun g := e.eqv.unit.app _ ≫ e.eqv.inverse.map g ≫ e.eqv.unitInv.app _
+  toFun f := End.of (e.eqv.functor.map f.asHom)
+  invFun g := End.of (e.eqv.unit.app _ ≫ e.eqv.inverse.map g.asHom ≫ e.eqv.unitInv.app _)
   left_inv := by
     intro f
     simp only [Equivalence.inv_fun_map, Functor.id_obj, Category.assoc]
     rw [← Category.assoc]
+    apply End.ext
     change (e.eqv.unit ≫ e.eqv.unitInv).app _ ≫ _ = _
     simp
   right_inv := by
     intro g
     simp only [Functor.map_comp, Equivalence.fun_inv_map, Functor.id_obj,
       Category.assoc, Equivalence.counitInv_functor_comp, Category.comp_id]
-    exact e.eqv.functor_unit_comp_assoc (ModuleCat.of A A) g
-  map_mul' x y := by simp
-  map_add' x y := by rw [e.eqv.functor.map_add]
+    exact congrArg End.of (e.eqv.functor_unit_comp_assoc (ModuleCat.of A A) g.asHom)
+  map_mul' x y := by apply End.ext; simp
+  map_add' x y := by apply End.ext; simp [e.eqv.functor.map_add]
   commutes' r := by
-    rw [Algebra.algebraMap_eq_smul_one, e.linear.map_smul, Algebra.algebraMap_eq_smul_one]
-    simp only [End.one_def, CategoryTheory.Functor.map_id]
+    rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one]
+    apply End.ext
+    simp [e.linear.map_smul]
 
 -- instance (M : Type*) [AddCommGroup M] [Module B M] : Algebra R (Module.End B M) :=
 -- {
@@ -311,13 +322,14 @@ noncomputable def aux20 : (e.eqv.functor.obj (ModuleCat.of A A)) ≅ ModuleCat.o
 
 set_option backward.isDefEq.respectTransparency false in
 def aux2 (M N : ModuleCat B) (f : M ≅ N) : End M ≃ₐ[R] End N where
-  toFun x := f.inv ≫ x ≫ f.hom
-  invFun x := f.hom ≫ x ≫ f.inv
+  toFun x := End.of (f.inv ≫ x.asHom ≫ f.hom)
+  invFun x := End.of (f.hom ≫ x.asHom ≫ f.inv)
   left_inv x := by simp
   right_inv x := by simp
-  map_mul' x y := by simp
-  map_add' x y := by rw [Preadditive.add_comp, Preadditive.comp_add]
+  map_mul' x y := by apply End.ext; simp
+  map_add' x y := by apply End.ext; simp [Preadditive.add_comp, Preadditive.comp_add]
   commutes' r := by
+    apply End.ext
     apply hom_ext
     ext n
     change f.hom.hom ((ModuleCat.ofHom _).hom (f.inv.hom n)) = (ModuleCat.ofHom _).hom n
diff --git a/BrauerGroup/Morita/TensorProduct.lean b/BrauerGroup/Morita/TensorProduct.lean
index 57e57f0..6440661 100644
--- a/BrauerGroup/Morita/TensorProduct.lean
+++ b/BrauerGroup/Morita/TensorProduct.lean
@@ -237,7 +237,9 @@ abbrev fromModuleOverTensor : ModuleCat (A ⊗[R] C) ⥤ TensorModule R A C wher
   }
   map f := {
     hom := (ModuleCat.restrictScalars (Algebra.TensorProduct.includeLeftRingHom)).map f
-    commutes c := by ext; simp
+    commutes c := by
+      ext x
+      exact (map_smul f.hom ((1 : A) ⊗ₜ[R] c) x).symm
   }
   map_id M := by ext; simp
   map_comp _ _ := by ext; simp
@@ -291,10 +293,12 @@ abbrev e02 (M : ModuleCat (A ⊗[R] C)) :
       conv_rhs => erw [AddHom.id_apply]
       rw [smul_tensormod]
       simp [smul_smul]
+      change (a ⊗ₜ[R] (1 : C)) • (((1 : A) ⊗ₜ[R] c) • m) = (a ⊗ₜ[R] c) • m
+      rw [smul_smul, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
       | add x y h1 h2 =>
       rw [RingHom.id_apply, AddHom.toFun_eq_coe]
       erw [AddHom.id_apply, AddHom.id_apply]
-      conv_rhs => rw [add_smul]
+      conv_rhs => erw [add_smul]
       erw [AddHom.toFun_eq_coe, AddHom.id_apply] at h1 h2
       simp only [RingHom.id_apply] at h1 h2
       erw [AddHom.id_apply] at h1 h2
diff --git a/BrauerGroup/MoritaEquivalence.lean b/BrauerGroup/MoritaEquivalence.lean
index 4c698d0..0ae7fd6 100644
--- a/BrauerGroup/MoritaEquivalence.lean
+++ b/BrauerGroup/MoritaEquivalence.lean
@@ -167,17 +167,18 @@ def matrix.unitIsoHom :
     { toFun x := ∑ i : ι, x.1 i
       map_add' := by
         rintro ⟨_, x, rfl⟩ ⟨_, y, rfl⟩
-        simp only [← Finset.sum_add_distrib]
-        rfl
+        exact Finset.sum_add_distrib
       map_smul' := by
         rintro r ⟨_, x, rfl⟩
-        simp only [RingHom.id_apply, Finset.smul_sum]
+        rw [RingHom.id_apply]
+        change ∑ i, ((single default default r : M[ι, R]) • (single default default 1 • x)) i =
+          r • ∑ i, (single default default 1 • x) i
+        refine Eq.trans ?_ (Finset.smul_sum (r := r) (f := fun i => (single default default 1 • x) i)
+          (s := Finset.univ)).symm
         refine Finset.sum_congr rfl fun i _ => ?_
-        rw [fromModuleCatOverMatrix.smul_α_coe, Subtype.coe_mk, ← SemigroupAction.mul_smul]
-        change ∑ _, _ = r • ∑ _, _
-        simp only [single_mul_single_same, mul_one]
-        simp only [single, of_apply, ite_smul, zero_smul, one_smul, Finset.smul_sum,
-          smul_ite, smul_zero]}
+        change ∑ j : ι, single default default r i j • (∑ k : ι, single default default 1 j k • x k) =
+          r • ∑ k : ι, single default default 1 i k • x k
+        simp [single_apply, ite_and, Finset.smul_sum, ite_smul, Finset.sum_ite_eq]}
   naturality {X Y} f := by
     simp only [Functor.id_obj, Functor.comp_map, Functor.id_map]
     ext ⟨_, x, rfl⟩
@@ -207,7 +208,7 @@ def matrix.unitIsoInv :
           eq_rec_constant, Pi.zero_apply, dite_eq_ite]
         split_ifs with h
         · subst h
-          simp only [true_and, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
+          simp
         · apply Finset.sum_eq_zero
           intro j _
           rw [if_neg]
@@ -260,7 +261,9 @@ def matrix.unitIso :
       simp only [single, of_apply, ite_smul, one_smul, zero_smul, true_and]
       split_ifs with h
       · subst h
-        simp only [true_and, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
+        simp only [true_and]
+        exact (Finset.sum_ite_eq Finset.univ default (fun j => (x : ι → X) j)).trans
+          (if_pos (Finset.mem_univ _))
       · apply Finset.sum_eq_zero
         intro j _
         rw [if_neg]
@@ -419,7 +422,10 @@ noncomputable def moritaEquivalentToMatrix : ModuleCat R ≌ ModuleCat M[ι, R]
       (∑ k : ι, single default i (1 : R) j k • v k)
     by_cases h : j = default
     · subst h
-      simp [Function.update, single]
+      simp only [Function.update, single, eq_rec_constant, Pi.zero_apply, dite_eq_ite]
+      simp only [of_apply, ite_smul, one_smul, zero_smul, true_and]
+      exact ((Finset.sum_ite_eq Finset.univ i (fun j => (v : ι → X) j)).trans
+        (if_pos (Finset.mem_univ _))).symm
     · simp [Function.update, single, h, Ne.symm h]
 
 namespace IsMoritaEquivalent
@@ -468,8 +474,12 @@ lemma division_ring_exists_unique_isSimpleModule
     refine ⟨b.repr ≪≫ₗ LinearEquiv.ofBijective ⟨⟨fun x => x ⟨i, by simp⟩, ?_⟩, ?_⟩ ⟨?_, ?_⟩⟩
     · intro x y; simp
     · intro x y; simp
-    · intro x y hxy; ext; simpa using hxy
-    · intro x; exact ⟨Finsupp.single ⟨i, by simp⟩ x, by simp⟩
+    · intro x y hxy
+      refine Finsupp.ext fun ⟨j, hj⟩ => ?_
+      have hji : j = i := by simpa using hj
+      subst hji
+      exact hxy
+    · intro x; exact ⟨Finsupp.single ⟨i, by simp⟩ x, Finsupp.single_eq_same⟩
 
 instance : e.functor.Additive :=
   Functor.additive_of_preserves_binary_products _
diff --git a/BrauerGroup/SkolemNoether.lean b/BrauerGroup/SkolemNoether.lean
index 9ff4bb4..0d4e46c 100644
--- a/BrauerGroup/SkolemNoether.lean
+++ b/BrauerGroup/SkolemNoether.lean
@@ -65,8 +65,10 @@ def smul1AddHom (K A B M : Type u)
   TensorProduct.liftAddHom (smul1AddHom' K A B M f m) fun k b l ↦ by
     simp only [smul1AddHom', AddMonoidHom.coe_mk, ZeroHom.coe_mk, LinearMapClass.map_smul,
       smul_assoc, LinearMap.smul_apply]
-    rw [smul_comm]
+    change k • f b • l m = f b • (k • l) m
+    exact smul_comm k (f b) (l m)
 
+set_option backward.isDefEq.respectTransparency false in
 def smul1 (K A B M : Type u)
     [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] [Ring B] [Algebra K B]
     [AddCommGroup M] [Module K M] [Module A M] [IsScalarTower K A M] (f : B →ₐ[K] A) :
@@ -81,10 +83,8 @@ def smul1 (K A B M : Type u)
       · rename_i b l
         simp only [TensorProduct.smul_tmul', TensorProduct.liftAddHom_tmul, AddMonoidHom.coe_mk,
           ZeroHom.coe_mk, LinearMapClass.map_smul, smul_assoc]
-        congr
-        ext k m
-        change k • m = algebraMap _ _ k • m
-        simp only [algebraMap_smul]
+        change k • f b • l m = algebraMap K A k • f b • l m
+        rw [algebraMap_smul]
       · rename_i bl1 bl2 hbl1 hbl2
         simp only [smul_add, map_add, hbl1, hbl2]
   }
@@ -94,6 +94,7 @@ lemma one_smul1 (K A B M : Type u)
     [Module K M] [Module A M] [IsScalarTower K A M] (f : B →ₐ[K] A) :
     ∀ (m : module_inst K A B M f), smul1 K A B M f m 1 = m := fun m ↦ by
   simp [smul1, smul1AddHom, smul1AddHom', Algebra.TensorProduct.one_def]
+  rfl
 
 set_option backward.isDefEq.respectTransparency false in
 lemma mul_smul1 (K A B M : Type u)
@@ -172,10 +173,6 @@ instance (K A B M : Type u)
     IsScalarTower K (B ⊗[K] Module.End A M) (module_inst K A B M f) where
   smul_assoc a x y := by
     induction x with
-    | zero =>
-      -- simp
-      change smul1 K A B M f _ _ = _ • smul1 K A B M f _ _
-      rw [map_zero, smul_zero, smul_zero, map_zero]
     | tmul b z =>
       change (smul1 K A B M f _ _) = _ • smul1 K A B M f _ _
       simp
@@ -206,7 +203,8 @@ instance module_inst_findim (K A B M : Type u)
       change _ = smul1 K A B M f k _
       simp only [smul1, smul1AddHom, smul1AddHom', ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe,
         LinearMap.coe_mk, AddHom.coe_mk, TensorProduct.liftAddHom_tmul, AddMonoidHom.coe_mk,
-        ZeroHom.coe_mk, AlgHom.commutes, algebraMap_smul, Module.End.one_apply]]
+        ZeroHom.coe_mk, AlgHom.commutes, algebraMap_smul, Module.End.one_apply]
+      rfl]
   refine Submodule.smul_mem _ _ ?_
   simp only
   refine Submodule.subset_span ?_
diff --git a/BrauerGroup/Subfield/Separable.lean b/BrauerGroup/Subfield/Separable.lean
index cb27ffc..c4a7452 100644
--- a/BrauerGroup/Subfield/Separable.lean
+++ b/BrauerGroup/Subfield/Separable.lean
@@ -242,13 +242,14 @@ noncomputable abbrev ZCL_equiv_ZCL_map (L : SubField K D) :
       (Subalgebra.centralizer K (A := D) L).val
       (Subalgebra.center K (Subalgebra.centralizer K (A := D) L)) :=
   AlgEquiv.ofBijective {
-    toFun x := ⟨x.1, ⟨⟨x.1, by simp⟩, by simp⟩⟩
+    toFun x := ⟨x.1.1, x.1, x.2, rfl⟩
     map_one' := by ext; rfl
     map_mul' _ _ := by ext; simp
     map_zero' := by ext; rfl
     map_add' _ _ := by ext; simp
     commutes' _ := by ext; simp }
-  ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp_all, fun ⟨y, ⟨y', hy1, hy2⟩⟩ ↦ ⟨⟨y', hy1⟩, by simpa using hy2⟩⟩
+  ⟨fun x y h ↦ Subtype.ext (Subtype.ext (congrArg Subtype.val h)),
+    fun ⟨y, ⟨y', hy1, hy2⟩⟩ ↦ ⟨⟨y', hy1⟩, Subtype.ext hy2⟩⟩
 
 abbrev SubField.bot_adjoin (a : D) : SubField K D :=
   SubField.adjoin K D ⊥ a (by