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] 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,