diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index e2dd547..f54ad88 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -230,7 +230,7 @@ structure Hom (χ η : ACCSystem) where
 def Hom.comp {χ η ε : ACCSystem} (g : Hom η ε) (f : Hom χ η) : Hom χ ε where
   charges := LinearMap.comp g.charges f.charges
   anomalyFree := g.anomalyFree ∘ f.anomalyFree
-  commute := by rw [LinearMap.coe_comp, Function.comp.assoc, f.commute,
-    ← Function.comp.assoc, g.commute, Function.comp.assoc]
+  commute := by rw [LinearMap.coe_comp, Function.comp_assoc, f.commute,
+    ← Function.comp_assoc, g.commute, Function.comp_assoc]
 
 end ACCSystem
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 5f70a23..f0512ff 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -39,8 +39,7 @@ namespace AnomalyFreePerp
 and for the cube line to sit in the quad. -/
 def LineEqProp (R : MSSMACC.AnomalyFreePerp) : Prop := α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0
 
-instance (R : MSSMACC.AnomalyFreePerp) : Decidable (LineEqProp R) := by
-  apply And.decidable
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (LineEqProp R) := instDecidableAnd
 
 /-- A condition on `Sols` which we will show in `linEqPropSol_iff_proj_linEqProp` that is equivalent
   to the condition that the `proj` of the solution satisfies `lineEqProp`. -/
@@ -80,8 +79,7 @@ entirely in the quadratic surface. -/
 def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
     quadBiLin R.val R.val = 0 ∧ quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
 
-instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InQuadProp R) := by
-  apply And.decidable
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InQuadProp R) := instDecidableAnd
 
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
 lies entirely in the quadratic surface. -/
@@ -126,8 +124,7 @@ def InCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
     cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
     cubeTriLin R.val R.val Y₃.val = 0
 
-instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := by
-  apply And.decidable
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := instDecidableAnd
 
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
 lies entirely in the cubic surface. -/
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 35cc97b..fca1016 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -85,7 +85,11 @@ def preimageType' {𝓥 : Type} (v : 𝓥) : Over 𝓥 ⥤ Type where
       have h := congrFun F.w x
       simp only [Functor.const_obj_obj, Functor.id_obj, Functor.id_map, types_comp_apply,
         CostructuredArrow.right_eq_id, Functor.const_obj_map, types_id_apply] at h
-      simpa [h] using x.2⟩
+      simp only [Functor.id_obj, Functor.const_obj_obj, Set.mem_preimage, Set.mem_singleton_iff]
+      obtain ⟨val, property⟩ := x
+      simp_all only
+      simp_all only [Functor.id_obj, Functor.const_obj_obj, Set.mem_preimage,
+        Set.mem_singleton_iff]⟩
 
 /-- The functor from `Over (P.HalfEdgeLabel × P.EdgeLabel × P.VertexLabel)` to
   `Over P.HalfEdgeLabel` induced by pull-back along insertion of `v : P.VertexLabel`. -/
@@ -288,7 +292,7 @@ instance diagramVertexPropDecidable
     (f : 𝓥 ⟶ P.VertexLabel) : Decidable (P.DiagramVertexProp F f) :=
   @decidable_of_decidable_of_iff _ _
     (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
-    (fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ => @instDecidableAnd _ _ _ (@Fintype.decidablePiFintype _ _
     (fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _) _)
     (P.diagramVertexProp_iff F f).symm
 
@@ -298,7 +302,7 @@ instance diagramEdgePropDecidable
     (f : 𝓔 ⟶ P.EdgeLabel) : Decidable (P.DiagramEdgeProp F f) :=
   @decidable_of_decidable_of_iff _ _
     (@Fintype.decidableForallFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _
-    (fun _ => @And.decidable _ _ _ (@Fintype.decidablePiFintype _ _
+    (fun _ => @instDecidableAnd _ _ _ (@Fintype.decidablePiFintype _ _
     (fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _) _)
     (P.diagramEdgeProp_iff F f).symm
 
@@ -371,7 +375,7 @@ instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (
     (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
     [Fintype 𝓥] [DecidableEq 𝓥] [Fintype 𝓔] [DecidableEq 𝓔] [h : Fintype 𝓱𝓔] [DecidableEq 𝓱𝓔] :
     Decidable (Cond 𝓔𝓞 𝓥𝓞 𝓱𝓔To𝓔𝓥) :=
-  @And.decidable _ _
+  @instDecidableAnd _ _
     (@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
     (@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
 
@@ -569,7 +573,7 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFin
 
 instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFinitePreFeynmanRule P]
     (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
-  And.decidable
+  instDecidableAnd
 
 /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
 @[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
@@ -712,10 +716,10 @@ def AdjRelation : F.𝓥 → F.𝓥 → Prop := fun x y =>
   ∧ (F.𝓱𝓔To𝓔𝓥.hom a).2.2 = x ∧ (F.𝓱𝓔To𝓔𝓥.hom b).2.2 = y)
 
 instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
-  @And.decidable _ _ _ $
+  @instDecidableAnd _ _ _ $
   @Fintype.decidableExistsFintype _ _ (fun _ => @Fintype.decidableExistsFintype _ _ (
-  fun _ => @And.decidable _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
-    @And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
+  fun _ => @instDecidableAnd _ _ (instDecidableEq𝓔OfIsFiniteDiagram _ _) $
+    @instDecidableAnd _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
     (instDecidableEq𝓥OfIsFiniteDiagram _ _)) _) _
 
 /-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
@@ -736,7 +740,7 @@ instance [IsFiniteDiagram F] : DecidableRel F.toSimpleGraph.Adj :=
 
 instance [IsFiniteDiagram F] :
   Decidable (F.toSimpleGraph.Preconnected ∧ Nonempty F.𝓥) :=
-  @And.decidable _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
+  @instDecidableAnd _ _ _ $ decidable_of_iff _ Finset.univ_nonempty_iff
 
 instance [IsFiniteDiagram F] : Decidable F.toSimpleGraph.Connected :=
   decidable_of_iff _ (SimpleGraph.connected_iff F.toSimpleGraph).symm
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index d63eb22..28e9d34 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -303,7 +303,8 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
     rw [cb_eq_zero_of_ud_us_zero ha] at h1
     simp at h1
     simp only [VcdAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, VcsAbs]
-    linear_combination ← h1
+    rw [← h1]
+    ring
   · simp only [VcdAbs, Fin.isValue, sub_nonneg, sq_le_one_iff_abs_le_one]
     rw [@abs_le]
     have h1 := VAbs_leq_one 1 0 ⟦V⟧
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
index f473b52..eab86d4 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@@ -31,7 +31,8 @@ open minkowskiMatrix
 lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := by
   have h1 := A.2
   erw [mem_skewAdjointMatricesLieSubalgebra] at h1
-  simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1
+  simpa only [neg_mul, mem_skewAdjointMatricesSubmodule, IsSkewAdjoint, IsAdjointPair,
+    mul_neg] using h1
 
 lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ}
     (h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by
@@ -96,8 +97,7 @@ instance lorentzVectorAsLieRingModule : LieRingModule lorentzAlgebra (LorentzVec
 
 @[simps!]
 instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) where
-  smul_lie r Λ x := by
-    simp [Bracket.bracket, smul_mulVec_assoc]
+  smul_lie r Λ x := smul_mulVec_assoc r Λ.1 x
   lie_smul r Λ x := by
     simp only [Bracket.bracket]
     rw [mulVec_smul]
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index d3bbf34..1b30006 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -98,7 +98,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
     LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, basis_left, map_smul, smul_eq_mul, map_neg,
     mul_eq_mul_left_iff]
   ring_nf
-  exact (true_or_iff (η μ μ = 0)).mpr trivial
+  exact (true_or (η μ μ = 0)).mpr trivial
 
 open minkowskiMatrix LorentzVector in
 lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
index 261f9ab..ff4655c 100644
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
@@ -98,20 +98,36 @@ noncomputable def toSelfAdjointMatrix :
     · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl]
       rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl]
       simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero]
+      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
+        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
+        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_zero, empty_val',
+        cons_val_fin_one]
       ring
     · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl]
       rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl]
       simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta,
         cons_val_zero]
+      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
+        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
+        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_one, empty_val',
+        cons_val_fin_one, cons_val_zero]
       ring
     · rw [show (x + y) (Sum.inr 0) = x (Sum.inr 0) + y (Sum.inr 0) from rfl]
       rw [show (x + y) (Sum.inr 1) = x (Sum.inr 1) + y (Sum.inr 1) from rfl]
       simp only [Fin.isValue, ofReal_add, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one,
         head_fin_const]
+      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
+        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
+        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_zero, empty_val',
+        cons_val_fin_one, cons_val_one, head_fin_const]
       ring
     · rw [show (x + y) (Sum.inl 0) = x (Sum.inl 0) + y (Sum.inl 0) from rfl]
       rw [show (x + y) (Sum.inr 2) = x (Sum.inr 2) + y (Sum.inr 2) from rfl]
       simp only [Fin.isValue, ofReal_add, Fin.mk_one, cons_val_one, head_cons, head_fin_const]
+      simp only [Fin.isValue, toSelfAdjointMatrix', toMatrix, LorentzVector.time,
+        LorentzVector.space, Function.comp_apply, AddMemClass.mk_add_mk, of_add_of, add_cons,
+        head_cons, tail_cons, empty_add_empty, of_apply, cons_val', cons_val_one, empty_val',
+        cons_val_fin_one, head_fin_const]
       ring
   map_smul' r x := by
     ext i j : 2
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
index f1d2922..0795769 100644
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@@ -97,7 +97,8 @@ noncomputable abbrev timeVec : (LorentzVector d) := e (Sum.inl 0)
 
 lemma timeVec_space : (@timeVec d).space = 0 := by
   funext i
-  simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, ↓reduceIte, PiLp.zero_apply]
+  simp only [space, Function.comp_apply, stdBasis_apply, Fin.isValue, reduceCtorEq, ↓reduceIte,
+    PiLp.zero_apply]
 
 lemma timeVec_time: (@timeVec d).time = 1 := by
   simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean
index 9d18391..0719bc0 100644
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@@ -156,6 +156,7 @@ lemma one_add_metric_non_zero : 1 + ⟪f, f'.1.1⟫ₘ ≠ 0 := by
 
 section
 variable {v w : NormOneLorentzVector d}
+open InnerProductSpace
 
 lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
     0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index b56a04a..1461767 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -17,7 +17,7 @@ of Lorentz vectors in d dimensions.
 -/
 
 open Matrix
-
+open InnerProductSpace
 /-!
 
 # The definition of the Minkowski Matrix
diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean
index 3abd848..bcbc1ab 100644
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@@ -63,6 +63,7 @@ def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
         conjTranspose_mul, conjTranspose_conjTranspose,
         (star_eq_conjTranspose A.1).symm.trans $ selfAdjoint.mem_iff.mp A.2]⟩
   map_add' A B := by
+    simp only [AddSubgroup.coe_add, AddMemClass.mk_add_mk, Subtype.mk.injEq]
     noncomm_ring [AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, AddSubmonoid.mk_add_mk,
       Subtype.mk.injEq]
   map_smul' r A := by
diff --git a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
index 66033ab..6f125bd 100644
--- a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
+++ b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
@@ -26,6 +26,7 @@ open Matrix
 open Complex
 open ComplexConjugate
 open SpaceTime
+open InnerProductSpace
 
 /-!
 
diff --git a/HepLean/Tensors/Basic.lean b/HepLean/Tensors/Basic.lean
index 3eb49c6..4ebeb2f 100644
--- a/HepLean/Tensors/Basic.lean
+++ b/HepLean/Tensors/Basic.lean
@@ -51,8 +51,8 @@ variable {d : ℕ} {X X' Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y
 /-- A relation on colors which is true if the two colors are equal or are duals. -/
 def colorRel (μ ν : 𝓒.Color) : Prop := μ = ν ∨ μ = 𝓒.τ ν
 
-instance : Decidable (colorRel 𝓒 μ ν) :=
-  Or.decidable
+instance : Decidable (colorRel 𝓒 μ ν) := instDecidableOr
+
 omit [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
 /-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
 lemma colorRel_equivalence : Equivalence 𝓒.colorRel where
@@ -90,8 +90,7 @@ instance colorSetoid : Setoid 𝓒.Color := ⟨𝓒.colorRel, 𝓒.colorRel_equi
 def colorQuot (μ : 𝓒.Color) : Quotient 𝓒.colorSetoid :=
   Quotient.mk 𝓒.colorSetoid μ
 
-instance (μ ν : 𝓒.Color) : Decidable (μ ≈ ν) :=
-  Or.decidable
+instance (μ ν : 𝓒.Color) : Decidable (μ ≈ ν) := instDecidableOr
 
 instance : DecidableEq (Quotient 𝓒.colorSetoid) :=
   instDecidableEqQuotientOfDecidableEquiv
diff --git a/HepLean/Tensors/IndexNotation/ColorIndexList/Basic.lean b/HepLean/Tensors/IndexNotation/ColorIndexList/Basic.lean
index a5ddb45..62fc7f4 100644
--- a/HepLean/Tensors/IndexNotation/ColorIndexList/Basic.lean
+++ b/HepLean/Tensors/IndexNotation/ColorIndexList/Basic.lean
@@ -75,7 +75,7 @@ lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) :
     intro x
     exact Finset.mem_univ ((Fin.castOrderIso (Eq.symm h)).toFun x)
     exact fun ⦃a b⦄ a => a
-  exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1))))
+  exact Eq.symm (OrderEmbedding.range_inj.mp (congrArg Set.range (id (Eq.symm h1))))
 
 /-!
 
diff --git a/HepLean/Tensors/IndexNotation/ColorIndexList/ContrPerm.lean b/HepLean/Tensors/IndexNotation/ColorIndexList/ContrPerm.lean
index aad5c71..5b25f5c 100644
--- a/HepLean/Tensors/IndexNotation/ColorIndexList/ContrPerm.lean
+++ b/HepLean/Tensors/IndexNotation/ColorIndexList/ContrPerm.lean
@@ -170,7 +170,7 @@ lemma symm (h : ContrPerm l l') : ContrPerm l' l := by
   rw [ContrPerm] at h ⊢
   apply And.intro h.1.symm
   apply And.intro (Subperm.symm h.2.1 h.1)
-  rw [← Function.comp.assoc, ← h.2.2, Function.comp.assoc, Function.comp.assoc]
+  rw [← Function.comp_assoc, ← h.2.2, Function.comp_assoc, Function.comp_assoc]
   rw [show (l.contr.getDualInOtherEquiv l'.contr) =
     (l'.contr.getDualInOtherEquiv l.contr).symm from rfl]
   simp only [Equiv.symm_comp_self, CompTriple.comp_eq]
diff --git a/HepLean/Tensors/IndexNotation/IndexList/Basic.lean b/HepLean/Tensors/IndexNotation/IndexList/Basic.lean
index 2a87597..ec6bdc5 100644
--- a/HepLean/Tensors/IndexNotation/IndexList/Basic.lean
+++ b/HepLean/Tensors/IndexNotation/IndexList/Basic.lean
@@ -309,27 +309,27 @@ lemma filter_sort_comm {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [Deci
     intro m
     simp only [Multiset.quot_mk_to_coe'', Multiset.coe_sort, Multiset.filter_coe]
     have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
-        (List.mergeSort (fun i j => i ≤ j) m)) := by
+        (List.mergeSort' (fun i j => i ≤ j) m)) := by
       simp only [List.Sorted]
       rw [List.pairwise_filter, List.pairwise_iff_get]
       intro i j h1 _ _
-      have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
-        exact List.sorted_mergeSort (fun i j => i ≤ j) m
+      have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort' (fun i j => i ≤ j) m) := by
+        exact List.sorted_mergeSort' (fun i j => i ≤ j) m
       simp only [List.Sorted] at hs
       rw [List.pairwise_iff_get] at hs
       exact hs i j h1
-    have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
-      exact List.perm_mergeSort (fun i j => i ≤ j) m
-    have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
+    have hp1 : (List.mergeSort' (fun i j => i ≤ j) m).Perm m := by
+      exact List.perm_mergeSort' (fun i j => i ≤ j) m
+    have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort' (fun i j => i ≤ j) m))).Perm
         (List.filter (fun b => decide (p b)) m) := by
       exact List.Perm.filter (fun b => decide (p b)) hp1
     have hp3 : (List.filter (fun b => decide (p b)) m).Perm
-      (List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
-      exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
+      (List.mergeSort' (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
+      exact List.Perm.symm (List.perm_mergeSort' (fun i j => i ≤ j)
       (List.filter (fun b => decide (p b)) m))
     have hp4 := hp2.trans hp3
     refine List.eq_of_perm_of_sorted hp4 h1 ?_
-    exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
+    exact List.sorted_mergeSort' (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
   exact this s.val
 
 omit [IndexNotation X] [Fintype X] [DecidableEq X] in
diff --git a/HepLean/Tensors/IndexNotation/IndexList/Color.lean b/HepLean/Tensors/IndexNotation/IndexList/Color.lean
index db2322f..a518c1c 100644
--- a/HepLean/Tensors/IndexNotation/IndexList/Color.lean
+++ b/HepLean/Tensors/IndexNotation/IndexList/Color.lean
@@ -331,7 +331,8 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
             exact hn hn''
           erw [hm'']
           rfl
-        · exact true_iff_iff.mpr hm
+        · rw [true_iff]
+          exact hm
       · simp only [hm, iff_false, ne_eq]
         simp only [colorMap, List.get_eq_getElem] at hm
         have hm' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑i].toColor) = false := by simpa using hm
diff --git a/HepLean/Tensors/IndexNotation/IndexList/Duals.lean b/HepLean/Tensors/IndexNotation/IndexList/Duals.lean
index 9ab8ab3..0580036 100644
--- a/HepLean/Tensors/IndexNotation/IndexList/Duals.lean
+++ b/HepLean/Tensors/IndexNotation/IndexList/Duals.lean
@@ -129,7 +129,9 @@ lemma mem_withDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther
 
 @[simp]
 lemma withDual_isSome (i : l.withDual) : (l.getDual? i).isSome := by
-  simpa [withDual] using i.2
+  have hx := i.2
+  simp only [Finset.mem_filter, withDual] at hx
+  exact hx.2
 
 @[simp]
 lemma mem_withDual_iff_isSome (i : Fin l.length) : i ∈ l.withDual ↔ (l.getDual? i).isSome := by
diff --git a/HepLean/Tensors/IndexNotation/TensorIndex.lean b/HepLean/Tensors/IndexNotation/TensorIndex.lean
index cdcec6f..b5c1db5 100644
--- a/HepLean/Tensors/IndexNotation/TensorIndex.lean
+++ b/HepLean/Tensors/IndexNotation/TensorIndex.lean
@@ -172,7 +172,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
       Function.comp_apply, LinearEquiv.coe_mk, Equiv.cast_apply, LinearEquiv.coe_symm_mk, cast_cast]
     apply cast_eq_iff_heq.mpr
     let hl := i.contrEquiv_on_withDual_empty l h
-    exact let_value_heq f hl
+    exact congr_arg_heq f hl
 
 omit [DecidableEq 𝓣.Color] in
 lemma contr_tensor_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
diff --git a/README.md b/README.md
index 81a3a61..62df503 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
 [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
 [![](https://img.shields.io/badge/Informal_dependencies-Graph-green)](https://heplean.github.io/HepLean/InformalGraph)
-[![](https://img.shields.io/badge/Lean-v4.11.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.11.0)
+[![](https://img.shields.io/badge/Lean-v4.12.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.12.0)
 
 A project to digitalize high energy physics.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 7001a99..6d8ab7e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,20 +55,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308",
+   "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",
@@ -85,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,10 +115,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.11.0-rc1",
+   "inputRev": "v4.12.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "hep_lean",
diff --git a/lakefile.toml b/lakefile.toml
index 164507d..bd32b42 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,12 +6,12 @@ defaultTargets = ["HepLean"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.11.0"
+rev = "v4.12.0"
 
 [[require]]
 name = "«doc-gen4»"
 git = "https://github.com/leanprover/doc-gen4"
-rev = "v4.11.0-rc1"
+rev = "v4.12.0"
 
 [[lean_lib]]
 name = "HepLean"
diff --git a/lean-toolchain b/lean-toolchain
index 5a9c76d..8998520 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0