From 835e917f0d53c1f8edde94bd7d90420c266ea46b Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 9 Jun 2024 21:33:31 +0200
Subject: [PATCH 1/2] golf proofs in `Rows.lean`

---
 HepLean/FlavorPhysics/CKMMatrix/Rows.lean | 175 +++++++++-------------
 1 file changed, 70 insertions(+), 105 deletions(-)

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index cc1d70b..406e1b8 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -57,7 +57,8 @@ lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
   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
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three,
+    one_apply_eq] at ht
   rw [mul_comm (V.1 1 0) _, mul_comm (V.1 1 1) _, mul_comm (V.1 1 2) _] at ht
   exact ht
 
@@ -66,7 +67,8 @@ lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 1) 0
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    one_ne_zero, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
@@ -75,7 +77,8 @@ lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 0
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
@@ -84,7 +87,8 @@ lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 0) 1
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    zero_ne_one, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
@@ -93,7 +97,8 @@ lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 1
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
@@ -102,7 +107,8 @@ lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 2) 2
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three,
+    one_apply_eq] at ht
   rw [mul_comm (V.1 2 0) _, mul_comm (V.1 2 1) _, mul_comm (V.1 2 2) _] at ht
   exact ht
 
@@ -111,7 +117,8 @@ lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 0) 2
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
@@ -120,32 +127,35 @@ lemma tRow_cRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]c = 0 := by
   have hV := V.prop
   rw [mem_unitaryGroup_iff] at hV
   have ht := congrFun (congrFun hV 1) 2
-  simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
+  simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, ne_eq,
+    Fin.reduceEq, not_false_eq_true, one_apply_ne] at ht
   rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
   exact ht
 
 lemma uRow_cross_cRow_conj (V : CKMMatrix) : conj (conj [V]u ×₃ conj [V]c) =  [V]u ×₃ [V]c := by
-  simp [crossProduct]
+  simp only [crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, LinearMap.mk₂_apply,
+    Pi.conj_apply]
   funext i
   fin_cases i <;> simp
 
 lemma cRow_cross_tRow_conj (V : CKMMatrix) : conj (conj [V]c ×₃ conj [V]t) =  [V]c ×₃ [V]t := by
-  simp [crossProduct]
+  simp only [crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, LinearMap.mk₂_apply,
+    Pi.conj_apply]
   funext i
   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
-  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]
+  rw [uRow_cross_cRow_conj, cross_dot_cross, dotProduct_comm, uRow_normalized,
+    dotProduct_comm, cRow_normalized, 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
-  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]
+  rw [cRow_cross_tRow_conj, cross_dot_cross, dotProduct_comm, cRow_normalized,
+    dotProduct_comm, tRow_normalized, dotProduct_comm, tRow_cRow_orthog,
+    dotProduct_comm, cRow_tRow_orthog]
   simp
 
 /-- A map from `Fin 3` to each row of a CKM matrix. -/
@@ -160,7 +170,7 @@ lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V)
   apply Fintype.linearIndependent_iff.mpr
   intro g hg
   rw [Fin.sum_univ_three] at hg
-  simp at hg
+  simp only [Fin.isValue, rows] at hg
   have h0 := congrArg (fun X => conj [V]u  ⬝ᵥ X) hg
   have h1 := congrArg (fun X => conj [V]c  ⬝ᵥ X) hg
   have h2 := congrArg (fun X => conj [V]t  ⬝ᵥ X) hg
@@ -169,15 +179,15 @@ lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V)
   rw [uRow_normalized, uRow_cRow_orthog, uRow_tRow_orthog] at h0
   rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog] at h1
   rw [tRow_normalized, tRow_uRow_orthog, tRow_cRow_orthog] at h2
-  simp at h0 h1 h2
+  simp only [Fin.isValue, mul_one, mul_zero, add_zero, zero_add] at h0 h1 h2
   intro i
   fin_cases i
-  exact h0
-  exact h1
-  exact h2
+  · exact h0
+  · exact h1
+  · exact h2
 
 lemma rows_card :  Fintype.card (Fin 3) = FiniteDimensional.finrank ℂ (Fin 3 → ℂ) := by
-  simp only [Fintype.card_fin, FiniteDimensional.finrank_fintype_fun_eq_card]
+  simp
 
 /-- The rows of a CKM matrix as a basis of `ℂ³`. -/
 @[simps!]
@@ -188,55 +198,40 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
     ∃ (κ : ℝ), [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t) := by
   obtain ⟨g, hg⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span (rowBasis V)
     (conj [V]c ×₃ conj [V]t))
-  rw [Fin.sum_univ_three, rowBasis] at hg
-  simp at hg
+  simp only [Fin.sum_univ_three, rowBasis, Fin.isValue, coe_basisOfLinearIndependentOfCardEqFinrank, rows] at hg
   have h0 := congrArg (fun X => conj [V]c  ⬝ᵥ X) hg
   have h1 := congrArg (fun X => conj [V]t  ⬝ᵥ X) hg
   simp only [Fin.isValue, dotProduct_add, dotProduct_smul, Pi.conj_apply,
     smul_eq_mul, dotProduct_zero] at h0 h1
   rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog, dot_self_cross] at h0
   rw [tRow_normalized, tRow_uRow_orthog, tRow_cRow_orthog, dot_cross_self] at h1
-  simp at h0 h1
-  rw [h0, h1] at hg
-  simp at hg
+  simp only [Fin.isValue, mul_zero, mul_one, zero_add, add_zero] at h0 h1 hg
+  simp only [h0, h1, zero_smul, add_zero] at hg
   have h2 := congrArg (fun X => conj X  ⬝ᵥ X) hg
   simp only [Fin.isValue, dotProduct_smul, Pi.conj_apply, Pi.smul_apply,
-    smul_eq_mul, _root_.map_mul] at h2
-  rw [cRow_cross_tRow_normalized] at h2
+    smul_eq_mul, _root_.map_mul, cRow_cross_tRow_normalized] at h2
   have h3 : conj (g 0 • [V]u)  = conj (g 0) • conj [V]u := by
     funext i
     fin_cases i <;> simp
-  rw [h3] at h2
-  simp only [Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul] at h2
-  rw [uRow_normalized] at h2
-  simp at h2
-  rw [mul_conj] at h2
-  rw [← Complex.sq_abs] at h2
+  simp only [h3, Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul,
+    uRow_normalized, Fin.isValue, mul_one, mul_conj, ← Complex.sq_abs] at h2
   simp at h2
   cases' h2  with h2 h2
   swap
   have hx : Complex.abs (g 0) = -1 := by
-    rw [← ofReal_inj]
-    simp only [Fin.isValue, ofReal_neg, ofReal_one]
-    exact h2
+    simp [← ofReal_inj, Fin.isValue, ofReal_neg, ofReal_one, h2]
   have h3 := Complex.abs.nonneg (g 0)
   simp_all
   have h4 : (0 : ℝ) < 1 := by norm_num
-  exact False.elim (lt_iff_not_le.mp h4 h3)
+  · exact False.elim (lt_iff_not_le.mp h4 h3)
   have hx : [V]u =  (g 0)⁻¹ • (conj ([V]c) ×₃ conj ([V]t)) := by
-    rw [← hg]
-    rw [@smul_smul]
-    rw [inv_mul_cancel]
-    simp only [one_smul]
+    rw [← hg, smul_smul, inv_mul_cancel, one_smul]
     by_contra hn
-    rw [hn] at h2
-    simp at h2
+    simp [hn] at h2
   have hg2 : Complex.abs (g 0)⁻¹ = 1 := by
-    rw [@map_inv₀, h2]
-    simp
+    simp [@map_inv₀, h2]
   have hg22 : ∃ (τ : ℝ), (g 0)⁻¹ = Complex.exp (τ * I) := by
-    rw [← abs_mul_exp_arg_mul_I (g 0)⁻¹]
-    rw [hg2]
+    rw [← abs_mul_exp_arg_mul_I (g 0)⁻¹, hg2]
     use arg (g 0)⁻¹
     simp
   obtain ⟨τ, hτ⟩ := hg22
@@ -255,9 +250,8 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
     smul_eq_mul, dotProduct_zero] at h0 h1
   rw [uRow_normalized, uRow_cRow_orthog, uRow_tRow_orthog, dot_self_cross] at h0
   rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog, dot_cross_self] at h1
-  simp at h0 h1
-  rw [h0, h1] at hg
-  simp at hg
+  simp only [Fin.isValue, mul_one, mul_zero, add_zero, zero_add] at h0 h1
+  simp only [Fin.isValue, h0, zero_smul, h1, add_zero, zero_add] at hg
   have h2 := congrArg (fun X => conj X  ⬝ᵥ X) hg
   simp only [Fin.isValue, dotProduct_smul, Pi.conj_apply, Pi.smul_apply,
     smul_eq_mul, _root_.map_mul] at h2
@@ -265,44 +259,31 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
   have h3 : conj (g 2 • [V]t)  = conj (g 2) • conj [V]t := by
     funext i
     fin_cases i <;> simp
-  rw [h3] at h2
-  simp only [Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul] at h2
-  rw [tRow_normalized] at h2
-  simp at h2
-  rw [mul_conj] at h2
-  rw [← Complex.sq_abs] at h2
-  simp at h2
+  simp only [h3, Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul, tRow_normalized,
+    Fin.isValue, mul_one, mul_conj, ← Complex.sq_abs, ofReal_pow, sq_eq_one_iff,
+    ofReal_eq_one] at h2
   cases' h2  with h2 h2
   swap
   have hx : Complex.abs (g 2) = -1 := by
-    rw [← ofReal_inj]
-    simp only [Fin.isValue, ofReal_neg, ofReal_one]
-    exact h2
+    simp [h2, ← ofReal_inj, Fin.isValue, ofReal_neg, ofReal_one]
   have h3 := Complex.abs.nonneg (g 2)
   simp_all
   have h4 : (0 : ℝ) < 1 := by norm_num
   exact False.elim (lt_iff_not_le.mp h4 h3)
   have hx : [V]t =  (g 2)⁻¹ • (conj ([V]u) ×₃ conj ([V]c)) := by
-    rw [← hg]
-    rw [@smul_smul]
-    rw [inv_mul_cancel]
-    simp only [one_smul]
+    rw [← hg, @smul_smul, inv_mul_cancel, one_smul]
     by_contra hn
-    rw [hn] at h2
-    simp at h2
+    simp [hn] at h2
   have hg2 : Complex.abs (g 2)⁻¹ = 1 := by
-    rw [@map_inv₀, h2]
-    simp
+    simp [@map_inv₀, h2]
   have hg22 : ∃ (τ : ℝ), (g 2)⁻¹ = Complex.exp (τ * I) := by
     rw [← abs_mul_exp_arg_mul_I (g 2)⁻¹]
-    rw [hg2]
     use arg (g 2)⁻¹
-    simp
+    simp [hg2]
   obtain ⟨τ, hτ⟩ := hg22
   use τ
   rw [hx, hτ]
 
-
 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
@@ -328,26 +309,21 @@ def ucCross  : Fin 3 → ℂ :=
 
 lemma ucCross_fst (V : CKMMatrix) : (ucCross V a b c d e f) 0 =
     cexp ((- a * I) +  (- b * I) + ( - e * I) +  (- f * I)) * (conj [V]u ×₃ conj [V]c) 0 := by
-  simp [ucCross, crossProduct]
-  simp [uRow, us, ub, cRow, cs, cb]
-  rw [exp_add, exp_add]
-  simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
+  simp [ucCross, crossProduct, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue,
+    LinearMap.mk₂_apply, Pi.conj_apply, cons_val_zero, neg_mul, uRow, us, ub, cRow, cs, cb,
+    exp_add, exp_sub, ← exp_conj, conj_ofReal]
   ring
 
 lemma ucCross_snd (V : CKMMatrix) : (ucCross V a b c d e f) 1 =
     cexp ((- a * I) +  (- b * I) + ( - d * I) +  (- f * I)) * (conj [V]u ×₃ conj [V]c) 1 := by
-  simp [ucCross, crossProduct]
-  simp [uRow, us, ub, cRow, cs, cb, ud, cd]
-  rw [exp_add, exp_add]
-  simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
+  simp [ucCross, crossProduct, uRow, us, ub, cRow, cs, cb, ud, cd, exp_add,
+    exp_sub, ← exp_conj, conj_ofReal]
   ring
 
 lemma ucCross_thd (V : CKMMatrix) : (ucCross V a b c d e f) 2 =
     cexp ((- a * I) +  (- b * I) + ( - d * I) +  (- e * I)) * (conj [V]u ×₃ conj [V]c) 2 := by
-  simp [ucCross, crossProduct]
-  simp [uRow, us, ub, cRow, cs, cb, ud, cd]
-  rw [exp_add, exp_add]
-  simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
+  simp [ucCross, crossProduct, uRow, us, ub, cRow, cs, cb, ud, cd, exp_add, exp_sub,
+    ← exp_conj, conj_ofReal]
   ring
 
 lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) :
@@ -356,12 +332,9 @@ lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) :
   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 only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
-  rw [us, uRow]
-  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
-  rw [ub, uRow]
-  simp
+  simp [ud, uRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
+  simp [us, uRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
+  simp [ub, uRow]
 
 lemma cRow_mul (V : CKMMatrix) (a b c : ℝ) :
     [phaseShiftApply V a b c 0 0 0]c = cexp (b * I) • [V]c  := by
@@ -369,12 +342,9 @@ lemma cRow_mul (V : CKMMatrix) (a b c : ℝ) :
   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 only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
-  rw [cs, cRow]
-  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
-  rw [cb, cRow]
-  simp
+  simp [cd, cRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
+  simp [cs, cRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
+  simp [cb, cRow]
 
 lemma tRow_mul (V : CKMMatrix) (a b c : ℝ) :
     [phaseShiftApply V a b c 0 0 0]t = cexp (c * I) • [V]t  := by
@@ -382,14 +352,9 @@ lemma tRow_mul (V : CKMMatrix) (a b c : ℝ) :
   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 only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
-  rw [ts, tRow]
-  simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
-  rw [tb, tRow]
-  simp
-
-
+  simp [td, tRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
+  simp [ts, tRow, ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
+  simp [tb, tRow]
 
 end  phaseShiftApply
 

From 5e6dc49028b065b690c42d6ba928647e412cdd72 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 9 Jun 2024 21:34:22 +0200
Subject: [PATCH 2/2] Update Rows.lean

---
 HepLean/FlavorPhysics/CKMMatrix/Rows.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index 406e1b8..e8d7f5b 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -198,7 +198,8 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
     ∃ (κ : ℝ), [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t) := by
   obtain ⟨g, hg⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span (rowBasis V)
     (conj [V]c ×₃ conj [V]t))
-  simp only [Fin.sum_univ_three, rowBasis, Fin.isValue, coe_basisOfLinearIndependentOfCardEqFinrank, rows] at hg
+  simp only [Fin.sum_univ_three, rowBasis, Fin.isValue,
+    coe_basisOfLinearIndependentOfCardEqFinrank, rows] at hg
   have h0 := congrArg (fun X => conj [V]c  ⬝ᵥ X) hg
   have h1 := congrArg (fun X => conj [V]t  ⬝ᵥ X) hg
   simp only [Fin.isValue, dotProduct_add, dotProduct_smul, Pi.conj_apply,