From d448c78045d218be0d635661ce1c59f6941ed691 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 29 Apr 2024 10:42:44 -0400
Subject: [PATCH] refactor: lint

---
 HepLean.lean                                  |   7 +
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean    | 141 ++++++++++++++----
 .../FlavorPhysics/CKMMatrix/Invariants.lean   |  18 +++
 .../FlavorPhysics/CKMMatrix/PhaseFreedom.lean |  55 ++++---
 .../FlavorPhysics/CKMMatrix/Relations.lean    |  53 ++++---
 HepLean/FlavorPhysics/CKMMatrix/Rows.lean     |  91 +++++------
 .../StandardParameterization/Basic.lean       |  24 ++-
 .../StandardParameters.lean                   | 117 ++++++++++-----
 8 files changed, 343 insertions(+), 163 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 590c56f..b5d6922 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -47,3 +47,10 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
 import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
+import HepLean.FlavorPhysics.CKMMatrix.Basic
+import HepLean.FlavorPhysics.CKMMatrix.Invariants
+import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
+import HepLean.FlavorPhysics.CKMMatrix.Relations
+import HepLean.FlavorPhysics.CKMMatrix.Rows
+import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
+import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index b68eb9d..7cadf48 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -6,12 +6,27 @@ Authors: Joseph Tooby-Smith
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Tactic.Polyrith
+/-!
+# The CKM Matrix
+
+The definition of the type of CKM matries as unitary $3×3$-matries.
+
+An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are
+related by phase shifts.
+
+The notation `[V]ud` etc can be used for the elements of a CKM matrix, and
+`[V]ud|us` etc for the ratios of elements.
+
+
+-/
 
 open Matrix Complex
 
 
 noncomputable section
 
+/-- Given three real numbers `a b c` the complex matrix with `exp (I * a)` etc on the
+leading diagonal. -/
 @[simp]
 def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
   ![![cexp (I * a), 0, 0], ![0,  cexp (I * b), 0], ![0, 0, cexp (I * c)]]
@@ -39,6 +54,8 @@ lemma phaseShiftMatrix_mul (a b c d e f : ℝ) :
   change cexp (I * ↑c)  * 0 = 0
   simp
 
+/-- Given three real numbers `a b c` the unitary matrix with `exp (I * a)` etc on the
+leading diagonal. -/
 @[simps!]
 def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
   ⟨phaseShiftMatrix a b c,
@@ -50,6 +67,7 @@ def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
 
 lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c := rfl
 
+/-- The equivalence relation between CKM matrices. -/
 def phaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
   ∃ a b c e f g , U = phaseShift a b c * V * phaseShift e f g
 
@@ -90,11 +108,12 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
   rw [add_comm k e, add_comm l f, add_comm m g]
 
 
-def phaseShiftEquivRelation : Equivalence phaseShiftRelation where
+lemma phaseShiftEquivRelation : Equivalence phaseShiftRelation where
   refl := phaseShiftRelation_refl
   symm := phaseShiftRelation_symm
   trans := phaseShiftRelation_trans
 
+/-- The type of CKM matrices. -/
 def CKMMatrix : Type := unitaryGroup (Fin 3) ℂ
 
 lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := by
@@ -102,18 +121,37 @@ lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := by
   simp at h
   subst h
   rfl
+
+/-- The `ud`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := ud_element) "[" V "]ud" => V.1 0 0
+
+/-- The `us`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := us_element) "[" V "]us" => V.1 0 1
+
+/-- The `ub`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := ub_element) "[" V "]ub" => V.1 0 2
+
+/-- The `cd`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := cd_element) "[" V "]cd" => V.1 1 0
+
+/-- The `cs`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := cs_element) "[" V "]cs" => V.1 1 1
+
+/-- The `cb`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := cb_element) "[" V "]cb" => V.1 1 2
+
+/-- The `td`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := td_element) "[" V "]td" => V.1 2 0
+
+/-- The `ts`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1
+
+/-- The `tb`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2
 
 instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨phaseShiftRelation, phaseShiftEquivRelation⟩
 
+/-- The matrix obtained from `V` by shifting the phases of the fermions. -/
 @[simps!]
 def phaseShiftApply (V : CKMMatrix) (a b c d e f : ℝ) : CKMMatrix :=
     phaseShift a b c * ↑V * phaseShift d e f
@@ -127,87 +165,105 @@ lemma equiv (V : CKMMatrix) (a b c d e f : ℝ) :
 
 lemma ud (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 0 0 = cexp (a * I + d * I) * V.1 0 0  := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const, mul_zero,
+    tail_val', head_val']
   change _ + _ * _ * 0 = _
   rw [exp_add]
   ring_nf
 
 lemma us (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 0 1 = cexp (a * I + e * I) * V.1 0 1  := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, mul_zero, zero_add,
+    head_fin_const]
   rw [exp_add]
   ring_nf
 
 lemma ub (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 0 2 = cexp (a * I + f * I) * V.1 0 2  := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, mul_zero, head_fin_const,
+    zero_add]
   rw [exp_add]
   ring_nf
 
 lemma cd (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 1 0= cexp (b * I + d * I) * V.1 1 0 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
+    mul_zero, tail_val', head_val']
   change _ + _ * _ * 0 = _
   rw [exp_add]
   ring_nf
 
 lemma cs (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 1 1 = cexp (b * I + e * I) * V.1 1 1 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
+    mul_zero]
   rw [exp_add]
   ring_nf
 
 lemma cb (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 1 2 = cexp (b * I + f * I) * V.1 1 2 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
+    mul_zero]
   rw [exp_add]
   ring_nf
 
 lemma td (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 2 0= cexp (c * I + d * I) * V.1 2 0 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
+    zero_mul, add_zero, mul_zero]
   change (0 * _  + _ ) * _ + (0 * _  + _ ) * 0 = _
-  simp
+  simp only [Fin.isValue, zero_mul, zero_add, mul_zero, add_zero]
   rw [exp_add]
   ring_nf
 
 lemma ts (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 2 1 = cexp (c * I + e * I) * V.1 2 1 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
+    zero_mul, add_zero, mul_zero, zero_add]
   change (0 * _ + _) * _ = _
   rw [exp_add]
   ring_nf
 
 lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
     (phaseShiftApply V a b c d e f).1 2 2 = cexp (c * I + f * I) * V.1 2 2 := by
-  simp
+  simp only [Fin.isValue, phaseShiftApply_coe]
   rw [mul_apply, Fin.sum_univ_three]
   rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
-  simp
+  simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
+    zero_mul, add_zero, mul_zero, zero_add]
   change (0 * _ + _) * _ = _
   rw [exp_add]
   ring_nf
@@ -215,13 +271,13 @@ lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
 end phaseShiftApply
 
 
-
+/-- The aboslute value of the `(i,j)`th element of `V`. -/
 @[simp]
 def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
 
 lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
     VAbs' V i j = VAbs' U i j  := by
-  simp
+  simp only [VAbs']
   obtain ⟨a, b, c, e, f, g, h⟩ := h
   rw [h]
   simp only [Submonoid.coe_mul, phaseShift_coe_matrix]
@@ -236,33 +292,52 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
   all_goals change Complex.abs (0 * _ + _) = _
   all_goals simp [Complex.abs_exp]
 
+/-- The absolute value of the `(i,j)`th any representative of `⟦V⟧`.  -/
 def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ :=
   Quotient.lift (fun V => VAbs' V i j) (VAbs'_equiv i j)
 
+/-- The absolute value of the `ud`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VudAbs := VAbs 0 0
 
+/-- The absolute value of the `us`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VusAbs := VAbs 0 1
 
+/-- The absolute value of the `ub`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VubAbs := VAbs 0 2
 
+/-- The absolute value of the `cd`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VcdAbs := VAbs 1 0
 
+/-- The absolute value of the `cs`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VcsAbs := VAbs 1 1
 
+/-- The absolute value of the `cb`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VcbAbs := VAbs 1 2
 
+/-- The absolute value of the `td`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VtdAbs := VAbs 2 0
 
+/-- The absolute value of the `ts`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VtsAbs := VAbs 2 1
 
+/-- The absolute value of the `tb`th element of a representative of an equivalence class of
+ CKM matrices. -/
 @[simp]
 abbrev VtbAbs := VAbs 2 2
 
@@ -273,48 +348,50 @@ open ComplexConjugate
 
 section ratios
 
+/-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
 def Rubud (V : CKMMatrix) : ℂ := [V]ub / [V]ud
 
+/-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := ub_ud_ratio) "[" V "]ub|ud" => Rubud V
 
+/-- The ratio of the `us` and `ud` elements of a CKM matrix. -/
 def Rusud (V : CKMMatrix) : ℂ := [V]us / [V]ud
 
+/-- The ratio of the `us` and `ud` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := us_ud_ratio) "[" V "]us|ud" => Rusud V
 
+/-- The ratio of the `ud` and `us` elements of a CKM matrix. -/
 def Rudus (V : CKMMatrix) : ℂ := [V]ud / [V]us
 
+/-- The ratio of the `ud` and `us` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := ud_us_ratio) "[" V "]ud|us" => Rudus V
 
+/-- The ratio of the `ub` and `us` elements of a CKM matrix. -/
 def Rubus (V : CKMMatrix) : ℂ := [V]ub / [V]us
 
+/-- The ratio of the `ub` and `us` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := ub_us_ratio) "[" V "]ub|us" => Rubus V
 
+/-- The ratio of the `cd` and `cb` elements of a CKM matrix. -/
 def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb
 
+/-- The ratio of the `cd` and `cb` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V
 
 lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := by
   rw [Rcdcb]
   exact (div_mul_cancel₀ (V.1 1 0) h).symm
 
+/-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
 def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb
 
+/-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
 scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V
 
 lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb := by
   rw [Rcscb]
   exact (div_mul_cancel₀ [V]cs h).symm
 
-
-def Rtb!cbud (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]ud)
-
-scoped[CKMMatrix] notation (name := tb_cb_ud_ratio) "[" V "]tb*|cb|ud" => Rtb!cbud V
-
-def Rtb!cbus (V : CKMMatrix) : ℂ := conj [V]tb / ([V]cb * [V]us)
-
-scoped[CKMMatrix] notation (name := tb_cb_us_ratio) "[" V "]tb*|cb|us" => Rtb!cbus V
-
-
 end ratios
 
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index 5ce5d0c..d5001e7 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -7,7 +7,18 @@ import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+/-!
+# Invariants of the CKM Matrix
 
+The CKM matrix is only defined up to an equivalence.
+
+This file defines some invariants of the CKM matrix, which are well-defined with respect to
+this equivalence.
+
+Of note, this file defines the complex jarlskog invariant.
+
+
+-/
 open Matrix Complex
 open ComplexConjugate
 open CKMMatrix
@@ -17,6 +28,7 @@ noncomputable section
 namespace Invariant
 
 
+/-- The complex jarlskog invariant for a CKM matrix. -/
 @[simps!]
 def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
   [V]us * [V]cb * conj [V]ub * conj [V]cs
@@ -36,13 +48,19 @@ lemma jarlskogℂCKM_equiv  (V U : CKMMatrix) (h : V ≈ U) :
   field_simp
   ring
 
+/-- The complex jarlskog invariant for an equivalence class of CKM matrices. -/
 @[simp]
 def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
   Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv
 
+/-- An invariant for CKM mtrices corresponding to the square of the absolute values
+ of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` .
+ -/
 def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ  :=
     VusAbs V ^ 2 * VubAbs V ^ 2  * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)
 
+/-- An invariant for CKM matrices. The argument of this invariant is `δ₁₃` in the
+standard parameterization. -/
 def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
   jarlskogℂ V + VusVubVcdSq V
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index d29ef77..30bd98b 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -8,7 +8,19 @@ import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.Relations
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+/-!
+# Phase freedom of the CKM Matrix
 
+The CKM matrix is only defined up to an equivalence. This leads to a freedom
+to shift the phases of the matrices elements of the CKM matrix.
+
+In this file we define two sets of conditions on the CKM matrices
+`fstRowThdColRealCond` which we show can be satisfied by any CKM matrix up to equivalence
+and `ubOnePhaseCond` which we show can be satisfied by any CKM matrix up to equivalence as long as
+the ub element as absolute value 1.
+
+
+-/
 open Matrix Complex
 
 
@@ -104,7 +116,7 @@ lemma shift_cd_phase_pi {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) :
   rfl
 
 lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
-  (hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) (h1 : τ = - u - c - t - d - s - b) :
+    (hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) (h1 : τ = - u - c - t - d - s - b) :
     [phaseShiftApply V u c t d s b]t =
     conj [phaseShiftApply V u c t d s b]u ×₃ conj [phaseShiftApply V u c t d s b]c := by
   change _ = phaseShiftApply.ucCross _ _ _ _ _ _ _
@@ -118,7 +130,7 @@ lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
     rw [← hτ0]
     rw [← mul_assoc,  ← exp_add, h1]
     congr 2
-    simp
+    simp only [ofReal_sub, ofReal_neg]
     ring
   · simp
     rw [phaseShiftApply.ucCross_snd]
@@ -128,7 +140,7 @@ lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
     rw [← hτ0]
     rw [← mul_assoc, ← exp_add, h1]
     congr 2
-    simp
+    simp only [ofReal_sub, ofReal_neg]
     ring
   · simp
     rw [phaseShiftApply.ucCross_thd]
@@ -138,23 +150,28 @@ lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
     rw [← hτ0]
     rw [← mul_assoc, ← exp_add, h1]
     congr 2
-    simp
+    simp only [ofReal_sub, ofReal_neg]
     ring
 
 end phaseShiftApply
 
 variable (a b c d e f : ℝ)
 
--- rename
+/-- A proposition which is satisfied by a CKM matrix if its `ud`, `us`, `cb` and `tb` elements
+are positive and real, and there is no phase difference between the `t`th-row and
+the cross product of the conjugates of the `u`th and `c`th rows. -/
 def fstRowThdColRealCond (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧
     ∧ [U]cb = VcbAbs ⟦U⟧ ∧ [U]tb = VtbAbs ⟦U⟧ ∧ [U]t = conj [U]u ×₃ conj [U]c
 
--- rename
+/-- A proposition which is satisfied by a CKM matrix `ub` is one, `ud`, `us` and `cb` are zero,
+  there is no phase difference between the `t`th-row and
+the cross product of the conjugates of the `u`th and `c`th rows, and the `cd`th and `cs`th
+elements are real and related in a set way.
+ -/
 def ubOnePhaseCond (U : CKMMatrix) :  Prop :=
     [U]ud = 0 ∧ [U]us = 0 ∧ [U]cb = 0 ∧ [U]ub = 1 ∧ [U]t = conj [U]u ×₃ conj [U]c
     ∧ [U]cd = - VcdAbs ⟦U⟧ ∧ [U]cs = √(1 - VcdAbs ⟦U⟧ ^ 2)
 
--- bad name for this lemma
 lemma fstRowThdColRealCond_shift_solution {V : CKMMatrix} (h1 : a + d = - arg [V]ud)
     (h2 :  a + e = - arg [V]us) (h3 : b + f = - arg [V]cb)
     (h4 : c + f = - arg [V]tb) (h5 : τ = - a - b - c - d - e - f) :
@@ -219,7 +236,7 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
     (- arg [V]us)
     (τ - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb)
   have hUV : ⟦U⟧ = ⟦V⟧ := by
-    simp
+    simp only [Quotient.eq]
     symm
     exact phaseShiftApply.equiv  _ _ _ _ _ _ _
   use U
@@ -252,7 +269,7 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
     (Real.pi - arg [V]cd ) (- arg [V]cs)  (- arg [V]ub )
   use U
   have hUV : ⟦U⟧ = ⟦V⟧ := by
-    simp
+    simp only [Quotient.eq]
     symm
     exact phaseShiftApply.equiv  _ _ _ _ _ _ _
   apply And.intro
@@ -288,7 +305,7 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
     simpa using h1
   apply And.intro
   · have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
-      simp
+      simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
       exact hV.2.2.2.2
     apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
     ring
@@ -304,11 +321,12 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
 
 
 lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
-    (hV : fstRowThdColRealCond V) : [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +
-    (- VubAbs ⟦V⟧ * VudAbs ⟦V⟧ * VcbAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2 )) * cexp (- arg [V]ub * I)
-      := by
+    (hV : fstRowThdColRealCond V) :
+    [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +
+    (- VubAbs ⟦V⟧ * VudAbs ⟦V⟧ * VcbAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2 ))
+    * cexp (- arg [V]ub * I) := by
   have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
-    simp
+    simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
     exact hV.2.2.2.2
   rw [cd_of_ud_us_ub_cb_tb hb hτ]
   rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
@@ -323,11 +341,12 @@ lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠
   ring_nf
 
 lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
-    (hV : fstRowThdColRealCond V) : [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
-      + (- VubAbs ⟦V⟧ *  VusAbs ⟦V⟧ * VcbAbs ⟦V⟧/ (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) * cexp (- arg [V]ub * I)
-      := by
+    (hV : fstRowThdColRealCond V) :
+    [V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
+    + (- VubAbs ⟦V⟧ *  VusAbs ⟦V⟧ * VcbAbs ⟦V⟧/ (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
+    * cexp (- arg [V]ub * I) := by
   have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
-    simp
+    simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
     exact hV.2.2.2.2
   rw [cs_of_ud_us_ub_cb_tb hb hτ]
   rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 5fc5c75..8461f1c 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -6,7 +6,13 @@ Authors: Joseph Tooby-Smith
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Rows
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+/-!
+# Relations for the CKM Matrix
 
+This file contains a collection of relations and properties between the elements of the CKM
+matrix.
+
+-/
 
 open Matrix Complex
 
@@ -55,7 +61,6 @@ lemma thd_row_normalized_normSq (V : CKMMatrix) :
   repeat rw [← Complex.sq_abs]
   exact V.thd_row_normalized_abs
 
--- rename
 lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) :
     normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := by
   linear_combination (fst_row_normalized_normSq V)
@@ -99,6 +104,26 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : [V]ud ≠ 0
   have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp
   exact h2 h3
 
+lemma VAbsub_neq_zero_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
+    (hV : VAbs 0 2 V ≠ 1) :(VudAbs V ^ 2 + VusAbs  V ^ 2) ≠ 0 := by
+  obtain ⟨V⟩ := V
+  change VubAbs ⟦V⟧ ≠ 1 at hV
+  simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV
+  rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
+  simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
+
+lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
+    (hV : VAbs 0 2 V ≠ 1) : √(VudAbs V ^ 2 + VusAbs  V ^ 2) ≠ 0 := by
+  obtain ⟨V⟩ := V
+  rw [Real.sqrt_ne_zero (Left.add_nonneg (sq_nonneg _) (sq_nonneg _))]
+  change VubAbs ⟦V⟧ ≠ 1 at hV
+  simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV
+  rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
+  simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
+
+
+
+
 lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ  {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
     (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by
   have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb
@@ -186,7 +211,7 @@ lemma conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ}
     ring
   rw [h2, V.Vcd_mul_conj_Vud]
   rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]
-  simp
+  simp only [Fin.isValue, neg_mul]
   ring
 
 lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
@@ -202,7 +227,7 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
     ring
   rw [h2, V.Vcs_mul_conj_Vus]
   rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]
-  simp
+  simp only [Fin.isValue, neg_mul]
   ring
 
 
@@ -224,6 +249,7 @@ lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix}  (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
   field_simp
   ring
 
+
 end rows
 
 
@@ -247,25 +273,6 @@ lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤
 
 end individual
 
-lemma VAbs_thd_neq_one_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3}
-    (hV : VAbs i 2 V ≠ 1) : (VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by
-  have h1 : 1 - VAbs i 2 V ^ 2 = VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2 := by
-    linear_combination - (VAbs_sum_sq_row_eq_one V i)
-  rw [← h1]
-  by_contra h
-  have h2 : VAbs i 2 V ^2 = 1 := by
-    nlinarith
-  simp only [Fin.isValue, sq_eq_one_iff] at h2
-  have h3 : 0 ≤  VAbs i 2 V := VAbs_ge_zero i 2 V
-  have h4 : VAbs i 2 V = 1 := by
-    nlinarith
-  exact hV h4
-
-lemma VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3}
-    (hV : VAbs i 2 V ≠ 1) : √(VAbs i 0 V ^ 2 + VAbs i 1 V ^ 2) ≠ 0 := by
-  rw [Real.sqrt_ne_zero (Left.add_nonneg (sq_nonneg (VAbs i 0 V)) (sq_nonneg (VAbs i 1 V)))]
-  exact VAbs_thd_neq_one_fst_snd_sq_neq_zero hV
-
 section columns
 
 
@@ -316,7 +323,7 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
   simp at h1
   simp [VAbs]
   linear_combination h1
-  simp
+  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⟧
   have h0 := VAbs_ge_zero 1 0 ⟦V⟧
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index 550fc19..cc1d70b 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -6,7 +6,16 @@ Authors: Joseph Tooby-Smith
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
 import Mathlib.LinearAlgebra.CrossProduct
+/-!
+# Rows for the CKM Matrix
 
+This file contains the definition extracting the rows of the CKM matrix and
+proves some properties between them.
+
+The first row can be extracted as `[V]u` for a CKM matrix `V`.
+
+
+-/
 
 open Matrix Complex
 
@@ -16,17 +25,26 @@ noncomputable section
 namespace CKMMatrix
 
 
+/-- The `u`th row of the CKM matrix. -/
 def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub]
+
+/-- The `u`th row of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := u_row) "[" V "]u" => uRow V
 
+/-- The `c`th row of the CKM matrix. -/
 def cRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]cd, [V]cs, [V]cb]
+
+/-- The `c`th row of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := c_row) "[" V "]c" => cRow V
 
+/-- The `t`th row of the CKM matrix. -/
 def tRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]td, [V]ts, [V]tb]
+
+/-- The `t`th row of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := t_row) "[" V "]t" => tRow V
 
 lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 0) 0
@@ -35,7 +53,7 @@ lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
   exact ht
 
 lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 1) 1
@@ -44,7 +62,7 @@ lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
   exact ht
 
 lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 1) 0
@@ -53,7 +71,7 @@ lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
   exact ht
 
 lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 0
@@ -62,7 +80,7 @@ lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
   exact ht
 
 lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 0) 1
@@ -71,7 +89,7 @@ lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
   exact ht
 
 lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 1
@@ -80,7 +98,7 @@ lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
   exact ht
 
 lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 2
@@ -89,7 +107,7 @@ lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
   exact ht
 
 lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 0) 2
@@ -98,7 +116,7 @@ lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
   exact ht
 
 lemma tRow_cRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]c = 0 := by
-  simp
+  simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 1) 2
@@ -117,19 +135,20 @@ lemma cRow_cross_tRow_conj (V : CKMMatrix) : conj (conj [V]c ×₃ conj [V]t) =
   fin_cases i <;> simp
 
 lemma uRow_cross_cRow_normalized (V : CKMMatrix) :
-     conj (conj [V]u ×₃ conj [V]c) ⬝ᵥ (conj [V]u ×₃ conj [V]c) = 1 := by
+    conj (conj [V]u ×₃ conj [V]c) ⬝ᵥ (conj [V]u ×₃ conj [V]c) = 1 := by
   rw [uRow_cross_cRow_conj, cross_dot_cross]
   rw [dotProduct_comm, uRow_normalized, dotProduct_comm, cRow_normalized]
   rw [dotProduct_comm, cRow_uRow_orthog, dotProduct_comm, uRow_cRow_orthog]
   simp
 
 lemma cRow_cross_tRow_normalized (V : CKMMatrix) :
-     conj (conj [V]c ×₃ conj [V]t) ⬝ᵥ (conj [V]c ×₃ conj [V]t) = 1 := by
+    conj (conj [V]c ×₃ conj [V]t) ⬝ᵥ (conj [V]c ×₃ conj [V]t) = 1 := by
   rw [cRow_cross_tRow_conj, cross_dot_cross]
   rw [dotProduct_comm, cRow_normalized, dotProduct_comm, tRow_normalized]
   rw [dotProduct_comm, tRow_cRow_orthog, dotProduct_comm, cRow_tRow_orthog]
   simp
 
+/-- A map from `Fin 3` to each row of a CKM matrix. -/
 @[simp]
 def rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ := fun i =>
   match i with
@@ -137,7 +156,7 @@ def rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ := fun i =>
   | 1 => cRow V
   | 2 => tRow V
 
-def rowsLinearlyIndependent (V : CKMMatrix) : LinearIndependent ℂ (rows V) := by
+lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V) := by
   apply Fintype.linearIndependent_iff.mpr
   intro g hg
   rw [Fin.sum_univ_three] at hg
@@ -160,9 +179,10 @@ def rowsLinearlyIndependent (V : CKMMatrix) : LinearIndependent ℂ (rows V) :=
 lemma rows_card :  Fintype.card (Fin 3) = FiniteDimensional.finrank ℂ (Fin 3 → ℂ) := by
   simp only [Fintype.card_fin, FiniteDimensional.finrank_fintype_fun_eq_card]
 
+/-- The rows of a CKM matrix as a basis of `ℂ³`. -/
 @[simps!]
 noncomputable def rowBasis (V : CKMMatrix) : Basis (Fin 3) ℂ (Fin 3 → ℂ) :=
-  basisOfLinearIndependentOfCardEqFinrank (rowsLinearlyIndependent V) rows_card
+  basisOfLinearIndependentOfCardEqFinrank (rows_linearly_independent V) rows_card
 
 lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
     ∃ (κ : ℝ), [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t) := by
@@ -197,7 +217,7 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
   swap
   have hx : Complex.abs (g 0) = -1 := by
     rw [← ofReal_inj]
-    simp
+    simp only [Fin.isValue, ofReal_neg, ofReal_one]
     exact h2
   have h3 := Complex.abs.nonneg (g 0)
   simp_all
@@ -207,7 +227,7 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
     rw [← hg]
     rw [@smul_smul]
     rw [inv_mul_cancel]
-    simp
+    simp only [one_smul]
     by_contra hn
     rw [hn] at h2
     simp at h2
@@ -256,7 +276,7 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
   swap
   have hx : Complex.abs (g 2) = -1 := by
     rw [← ofReal_inj]
-    simp
+    simp only [Fin.isValue, ofReal_neg, ofReal_one]
     exact h2
   have h3 := Complex.abs.nonneg (g 2)
   simp_all
@@ -266,7 +286,7 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
     rw [← hg]
     rw [@smul_smul]
     rw [inv_mul_cancel]
-    simp
+    simp only [one_smul]
     by_contra hn
     rw [hn] at h2
     simp at h2
@@ -283,23 +303,6 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
   rw [hx, hτ]
 
 
-def uRow₁₂ (V : CKMMatrix) : Fin 2 → ℂ := ![[V]ud, [V]us]
-
-def cRow₁₂ (V : CKMMatrix) : Fin 2 → ℂ := ![[V]cd, [V]cs]
-scoped[CKMMatrix] notation (name := c₁₂_row) "[" V "]c₁₂" => cRow₁₂ V
-
-lemma cRow₁₂_normalized_of_cb_zero {V : CKMMatrix} (hcb : [V]cb = 0) :
-    conj [V]c₁₂ ⬝ᵥ [V]c₁₂ = 1 := by
-  simp
-  have hV := V.prop
-  rw [mem_unitaryGroup_iff] at hV
-  have ht := congrFun (congrFun hV 1) 1
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
-  rw [hcb] at ht
-  rw [mul_comm (V.1 1 0) _, mul_comm (V.1 1 1) _] at ht
-  simp at ht
-  exact ht
-
 lemma ext_Rows {U V : CKMMatrix} (hu : [U]u = [V]u) (hc : [U]c = [V]c) (ht : [U]t = [V]t) :
     U = V := by
   apply CKMMatrix_ext
@@ -319,7 +322,7 @@ open CKMMatrix
 
 variable (V : CKMMatrix) (a b c d e f : ℝ)
 
-
+/-- The cross product of the conjugate of the `u` and `c` rows of a CKM matrix. -/
 def ucCross  : Fin 3 → ℂ :=
   conj [phaseShiftApply V a b c d e f]u ×₃ conj [phaseShiftApply V a b c d e f]c
 
@@ -350,39 +353,39 @@ lemma ucCross_thd (V : CKMMatrix) : (ucCross V a b c d e f) 2 =
 lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) :
     [phaseShiftApply V a b c 0 0 0]u = cexp (a * I) • [V]u  := by
   funext i
-  simp
+  simp only [Pi.smul_apply, smul_eq_mul]
   fin_cases i <;>
     change (phaseShiftApply V a b c 0 0 0).1 0 _ = _
   rw [ud, uRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
   rw [us, uRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
   rw [ub, uRow]
   simp
 
 lemma cRow_mul (V : CKMMatrix) (a b c : ℝ) :
     [phaseShiftApply V a b c 0 0 0]c = cexp (b * I) • [V]c  := by
   funext i
-  simp
+  simp only [Pi.smul_apply, smul_eq_mul]
   fin_cases i <;>
     change (phaseShiftApply V a b c 0 0 0).1 1 _ = _
   rw [cd, cRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
   rw [cs, cRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
   rw [cb, cRow]
   simp
 
 lemma tRow_mul (V : CKMMatrix) (a b c : ℝ) :
     [phaseShiftApply V a b c 0 0 0]t = cexp (c * I) • [V]t  := by
   funext i
-  simp
+  simp only [Pi.smul_apply, smul_eq_mul]
   fin_cases i <;>
     change (phaseShiftApply V a b c 0 0 0).1 2 _ = _
   rw [td, tRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
   rw [ts, tRow]
-  simp
+  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
   rw [tb, tRow]
   simp
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index 4bccf33..b98ac01 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -8,14 +8,25 @@ import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+/-!
+# Standard parameterization for the CKM Matrix
 
+This file defines the standard parameterization of CKM matrices in terms of
+four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
+
+We will show that every CKM matrix can be written within this standard parameterization
+in the file `FlavorPhysics.CKMMatrix.StandardParameters`.
+
+
+-/
 open Matrix Complex
 open ComplexConjugate
 open CKMMatrix
 
 noncomputable section
 
--- to be renamed stanParamAsMatrix ...
+/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
+as a `3×3` complex matrix. -/
 def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ  :=
   ![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)],
     ![(-Real.sin θ₁₂ * Real.cos θ₂₃) - (Real.cos θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃)),
@@ -87,6 +98,8 @@ lemma standParamAsMatrix_unitary  (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
     rw [sin_sq, sin_sq]
     ring
 
+/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
+as a CKM matrix. -/
 def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
   ⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
    rw [mem_unitaryGroup_iff']
@@ -137,13 +150,13 @@ lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h
     standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
   simp [standParam, standParamAsMatrix]
   apply CKMMatrix_ext
-  simp
+  simp only
   rw [show  exp (I * δ₁₃) = exp (I * δ₁₃') by rw [mul_comm, h, mul_comm]]
   rw [show cexp (-(I * ↑δ₁₃)) = cexp (-(I * ↑δ₁₃')) by rw [exp_neg, exp_neg, mul_comm, h, mul_comm]]
 
 open Invariant in
 lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂)
-      (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) :
+    (h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) :
     VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ =
     Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by
   simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, standParam, standParamAsMatrix,
@@ -152,7 +165,8 @@ lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Rea
     VcbAbs, VudAbs, Complex.abs_ofReal]
   by_cases hx : Real.cos θ₁₃ ≠ 0
   · rw [Complex.abs_exp]
-    simp
+    simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
+      neg_zero, Real.exp_zero, mul_one, _root_.sq_abs]
     rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2,
       _root_.abs_of_nonneg h4]
     simp [sq]
@@ -175,7 +189,7 @@ lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤
     Quotient.lift_mk, jarlskogℂCKM, Fin.isValue, cons_val', cons_val_one, head_cons,
     empty_val', cons_val_fin_one, cons_val_zero, cons_val_two, tail_cons, _root_.map_mul, ←
     exp_conj, map_neg, conj_I, conj_ofReal, neg_neg, map_sub]
-  simp
+  simp only [ofReal_sin, ofReal_cos, ofReal_mul, ofReal_pow]
   ring_nf
   rw [exp_neg]
   have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index 139d373..e23e6d6 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -9,33 +9,63 @@ import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arg
+/-!
+# Standard parameters for the CKM Matrix
 
+Given a CKM matrix `V` we can extract  four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
+These, when used in the standard parameterization return `V` up to equivalence.
+
+This leads to the theorem `standParam.exists_for_CKMatrix` which says that up to equivalence every
+CKM matrix can be written using the standard parameterization.
+
+
+-/
 open Matrix Complex
 open ComplexConjugate
 open CKMMatrix
 
 noncomputable section
 
+/-- Given a CKM matrix `V` the real number corresponding to `sin θ₁₂` in the
+standard parameterization.  --/
 def S₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V / (√ (VudAbs V ^ 2 + VusAbs V ^ 2))
 
+/-- Given a CKM matrix `V` the real number corresponding to `sin θ₁₃` in the
+standard parameterization.  --/
 def S₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := VubAbs V
 
+/-- Given a CKM matrix `V` the real number corresponding to `sin θ₂₃` in the
+standard parameterization.  --/
 def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
   if VubAbs V = 1 then VcdAbs V
   else VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2)
 
+/-- Given a CKM matrix `V` the real number corresponding to `θ₁₂` in the
+standard parameterization.  --/
 def θ₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₂ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to `θ₁₃` in the
+standard parameterization.  --/
 def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to `θ₂₃` in the
+standard parameterization.  --/
 def θ₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₂₃ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to `cos θ₁₂` in the
+standard parameterization.  --/
 def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to `cos θ₁₃` in the
+standard parameterization.  --/
 def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to `sin θ₂₃` in the
+standard parameterization.  --/
 def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V)
 
+/-- Given a CKM matrix `V` the real number corresponding to the phase `δ₁₃` in the
+standard parameterization.  --/
 def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
   arg (Invariant.mulExpδ₁₃ V)
 
@@ -69,7 +99,7 @@ lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
   apply Or.inl
   simp_all
   rw [Real.le_sqrt (VAbs_ge_zero 0 1 V) (le_of_lt h3)]
-  simp
+  simp only [Fin.isValue, le_add_iff_nonneg_left]
   exact sq_nonneg (VAbs 0 0 V)
 
 lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 :=
@@ -91,7 +121,7 @@ lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by
   simp_all
   rw [Real.le_sqrt (VAbs_ge_zero 1 2 V) (le_of_lt h3)]
   rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq]
-  simp
+  simp only [Fin.isValue, VcbAbs, VtbAbs, le_add_iff_nonneg_right]
   exact sq_nonneg (VAbs 2 2 V)
 
 lemma S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₂ V) = S₁₂ V :=
@@ -158,19 +188,19 @@ lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (
 lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₂ V)) =
     cos (θ₁₂ V):= by
   rw [C₁₂_eq_ℂcos_θ₁₂, Complex.abs_ofReal]
-  simp
+  simp only [ofReal_inj, abs_eq_self]
   exact Real.cos_arcsin_nonneg _
 
 lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) =
     cos (θ₁₃ V):= by
   rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal]
-  simp
+  simp only [ofReal_inj, abs_eq_self]
   exact Real.cos_arcsin_nonneg _
 
 lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) =
     cos (θ₂₃ V):= by
   rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal]
-  simp
+  simp only [ofReal_inj, abs_eq_self]
   exact Real.cos_arcsin_nonneg _
 
 lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := by
@@ -198,12 +228,12 @@ lemma C₁₂_eq_Vud_div_sqrt {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠
     C₁₂ V = VudAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
   rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂, div_pow, Real.sq_sqrt]
   rw [one_sub_div]
-  simp
+  simp only [VudAbs, Fin.isValue, VusAbs, add_sub_cancel_right]
   rw [Real.sqrt_div]
   rw [Real.sqrt_sq]
   exact VAbs_ge_zero 0 0 V
   exact sq_nonneg (VAbs 0 0 V)
-  exact VAbs_thd_neq_one_fst_snd_sq_neq_zero ha
+  exact VAbsub_neq_zero_Vud_Vus_neq_zero ha
   exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))
 
 --rename
@@ -222,7 +252,7 @@ lemma C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1
   rw [Real.sqrt_div (sq_nonneg (VAbs 2 2 V))]
   rw [Real.sqrt_sq (VAbs_ge_zero 2 2 V)]
   rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq ]
-  exact VAbs_thd_neq_one_fst_snd_sq_neq_zero ha
+  exact VAbsub_neq_zero_Vud_Vus_neq_zero ha
   exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))
 
 end cosines
@@ -235,12 +265,12 @@ lemma VudAbs_eq_C₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VudAbs V =
   change VAbs 0 0 V = C₁₂ V * C₁₃ V
   rw [VAbs_thd_eq_one_fst_eq_zero ha]
   rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃, ha]
-  simp
+  simp only [one_pow, sub_self, Real.sqrt_zero, mul_zero]
   rw [C₁₂_eq_Vud_div_sqrt ha, C₁₃, θ₁₃, Real.cos_arcsin, S₁₃]
   have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by
     linear_combination - (VAbs_sum_sq_row_eq_one V 0)
   rw [h1, mul_comm]
-  exact (mul_div_cancel₀ (VudAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm
+  exact (mul_div_cancel₀ (VudAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
 
 lemma VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V = S₁₂ V * C₁₃ V := by
   rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₂, S₁₃]
@@ -254,7 +284,7 @@ lemma VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V =
   rw [← h1]
   simp only [Real.sqrt_zero, div_zero, mul_zero]
   exact VAbs_thd_eq_one_snd_eq_zero ha
-  have h2 := VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha
+  have h2 := VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha
   exact (mul_div_cancel₀ (VusAbs V) h2).symm
 
 lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rfl
@@ -262,20 +292,20 @@ lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V :=
 lemma VcbAbs_eq_S₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VcbAbs V = S₂₃ V * C₁₃ V := by
   by_cases ha : VubAbs V = 1
   rw [C₁₃_of_Vub_eq_one ha]
-  simp
+  simp only [VcbAbs, Fin.isValue, mul_zero]
   exact VAbs_fst_col_eq_one_snd_eq_zero ha
   rw [S₂₃_of_Vub_neq_one ha, C₁₃_eq_add_sq]
   rw [mul_comm]
-  exact (mul_div_cancel₀ (VcbAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm
+  exact (mul_div_cancel₀ (VcbAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
 
 lemma VtbAbs_eq_C₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VtbAbs V = C₂₃ V * C₁₃ V := by
   by_cases ha : VubAbs V = 1
   rw [C₁₃_of_Vub_eq_one ha]
-  simp
+  simp only [VtbAbs, Fin.isValue, mul_zero]
   exact VAbs_fst_col_eq_one_thd_eq_zero ha
   rw [C₂₃_of_Vub_neq_one ha, C₁₃_eq_add_sq]
   rw [mul_comm]
-  exact (mul_div_cancel₀ (VtbAbs V) (VAbs_thd_neq_one_sqrt_fst_snd_sq_neq_zero ha)).symm
+  exact (mul_div_cancel₀ (VtbAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
 
 lemma VubAbs_of_cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) :
     VubAbs V = 1 := by
@@ -288,7 +318,7 @@ lemma VubAbs_of_cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos
   rw [h2] at h3
   simp at h3
   linarith
-  simp
+  simp only [VubAbs, Fin.isValue, sub_nonneg, sq_le_one_iff_abs_le_one]
   rw [_root_.abs_of_nonneg (VAbs_ge_zero 0 2 V)]
   exact VAbs_leq_one 0 2 V
 
@@ -309,7 +339,8 @@ open Invariant
 
 lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) :
     mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ =
-    sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃)  := by
+    sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧)
+    * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃)  := by
   refine mulExpδ₁₃_eq _ _ _ _ ?_ ?_ ?_ ?_
   rw [S₁₂_eq_sin_θ₁₂]
   exact S₁₂_nonneg _
@@ -321,14 +352,15 @@ lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) :
 lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :
     mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ = 0 ↔
      VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by
-  rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃,  VtbAbs_eq_C₂₃_mul_C₁₃,
-  ← ofReal_inj,
+  rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃,
+   VtbAbs_eq_C₂₃_mul_C₁₃, ← ofReal_inj,
   ← ofReal_inj, ← ofReal_inj,  ← ofReal_inj, ← ofReal_inj]
   simp only [ofReal_mul]
   rw [← S₁₃_eq_ℂsin_θ₁₃, ← S₁₂_eq_ℂsin_θ₁₂, ← S₂₃_eq_ℂsin_θ₂₃,
   ← C₁₃_eq_ℂcos_θ₁₃, ← C₂₃_eq_ℂcos_θ₂₃,← C₁₂_eq_ℂcos_θ₁₂]
   rw [mulExpδ₁₃_on_param_δ₁₃]
-  simp
+  simp only [mul_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff,
+    ofReal_zero]
   have h1 := exp_ne_zero (I * δ₁₃)
   simp_all
   aesop
@@ -348,13 +380,15 @@ lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ)
     cexp (δ₁₃ * I) := by
   have h1a := mulExpδ₁₃_on_param_δ₁₃ V δ₁₃
   have habs := mulExpδ₁₃_on_param_abs V δ₁₃
-  have h2 : mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ =
-      Complex.abs (mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by
+  have h2 : mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ = Complex.abs
+      (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by
     rw [habs, h1a]
     ring_nf
-  nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ )] at h2
-  have habs_neq_zero : (Complex.abs (mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by
-    simp
+  nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₁₃
+    ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧ )] at h2
+  have habs_neq_zero :
+      (Complex.abs (mulExpδ₁₃  ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃  ⟦V⟧) (θ₂₃  ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by
+    simp only [ne_eq, ofReal_eq_zero, map_eq_zero]
     exact h1
   rw [← mul_right_inj' habs_neq_zero]
   rw [← h2]
@@ -387,14 +421,14 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   apply Or.inr
   rfl
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero, neg_inj]
   field_simp
   ring
   ring
   field_simp
   ring
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero]
   field_simp
   ring
   ring
@@ -413,7 +447,7 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
   rfl
   ring_nf
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero]
   ring
   field_simp
   ring
@@ -441,14 +475,14 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   apply Or.inr
   rfl
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero, neg_inj]
   ring
   field_simp
   ring
   field_simp
   ring
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero, neg_inj]
   ring
   field_simp
   ring
@@ -467,7 +501,7 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
   apply Or.inr
   rfl
   change _ = _ + _ * 0
-  simp
+  simp only [mul_zero, add_zero, neg_inj]
   ring
   ring
   field_simp
@@ -480,8 +514,8 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 
   have hb' : VubAbs ⟦V⟧ ≠ 1 := by
     rw [ud_us_neq_zero_iff_ub_neq_one] at hb
     simp [VAbs, hb]
-  have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)   * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) )
-    = ofReal ((VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ) := by
+  have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
+    ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal ((VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ) := by
     rw [Real.mul_self_sqrt ]
     apply add_nonneg (sq_nonneg _) (sq_nonneg _)
   simp at h1
@@ -496,14 +530,14 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 
   simp [C₁₂, C₁₃]
   simp [uRow, standParam, standParamAsMatrix]
   rw [hV.2.1, VusAbs_eq_S₁₂_mul_C₁₃ ⟦V⟧, ← S₁₂_eq_sin_θ₁₂ ⟦V⟧, C₁₃]
-  simp
+  simp only [ofReal_mul, ofReal_sin, ofReal_cos]
   simp [uRow, standParam, standParamAsMatrix]
   nth_rewrite 1 [← abs_mul_exp_arg_mul_I (V.1 0 2)]
   rw [show Complex.abs (V.1 0 2) = VubAbs ⟦V⟧ from rfl]
   rw [VubAbs_eq_S₁₃, ← S₁₃_eq_sin_θ₁₃ ⟦V⟧]
-  simp
+  simp only [ofReal_sin, Fin.isValue, mul_eq_mul_left_iff]
   ring_nf
-  simp
+  simp only [true_or]
   funext i
   fin_cases i
   simp [cRow, standParam, standParamAsMatrix]
@@ -543,15 +577,15 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
   fin_cases i
   simp [uRow, standParam, standParamAsMatrix]
   rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.1]
-  simp
+  simp only [ofReal_zero, mul_zero]
   simp [uRow, standParam, standParamAsMatrix]
   rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.1]
-  simp
+  simp only [ofReal_zero, mul_zero]
   simp [uRow, standParam, standParamAsMatrix]
   rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
   simp [VAbs]
   rw [hV.2.2.2.1]
-  simp
+  simp only [_root_.map_one, ofReal_one]
   funext i
   fin_cases i
   simp [cRow, standParam, standParamAsMatrix]
@@ -560,13 +594,14 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
   rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1]
   rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃_of_Vub_one h1]
   rw [hV.2.2.2.2.2.1]
-  simp
+  simp only [VcdAbs, Fin.isValue, ofReal_zero, zero_mul, neg_zero, ofReal_one, mul_one, one_mul,
+    zero_sub]
   simp [cRow, standParam, standParamAsMatrix]
   rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1]
   rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1]
   rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1]
   rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃_of_Vub_one h1]
-  simp
+  simp only [Fin.isValue, ofReal_one, one_mul, ofReal_zero, mul_one, VcdAbs, zero_mul, sub_zero]
   have h3 : (Real.cos (θ₂₃ ⟦V⟧) : ℂ) = √(1 - S₂₃ ⟦V⟧ ^ 2) := by
     rw [θ₂₃, Real.cos_arcsin]
   simp at h3