To Lorentz Group fst col

lemma toLorentzGroup_fst_col (M : SL(2, ℂ)) :    (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = fun μ =>      match μ with      | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)      | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +        (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))      | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im        - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))      | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := by  let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ =>    match μ with    | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)    | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +      (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))    | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))    | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)  change (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = k  have h1 : toSelfAdjointMap M (PauliMatrix.pauliBasis' (Sum.inl 0)) =      ∑ μ, k μ • PauliMatrix.pauliBasis' μ := by    simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,      Finset.sum_singleton, Fin.sum_univ_three]    rw [toSelfAdjointMap_apply_pauliBasis'_inl]    abel  rw [toSelfAdjointMap_basis] at h1  have h1x := sub_eq_zero_of_eq h1  rw [← Finset.sum_sub_distrib] at h1x  funext μ  refine sub_eq_zero.mp ?_  refine Fintype.linearIndependent_iff.mp PauliMatrix.pauliBasis'.linearIndependent    (fun x => ((toLorentzGroup M).1 x (Sum.inl 0) - k x)) ?_ μ  simp only [sub_smul]  exact h1x