Pauli Self Adjoint span

lemma pauliSelfAdjoint_span : ⊤ ≤ Submodule.span ℝ (Set.range pauliSelfAdjoint) := by  refine (Submodule.top_le_span_range_iff_forall_exists_fun ℝ).mpr ?_  intro A  let c : Fin 1 ⊕ Fin 3 → ℝ := fun i =>    match i with    | Sum.inl 0 => 1/2 * (Matrix.trace (σ0 * A.1)).re    | Sum.inr 0 => 1/2 * (Matrix.trace (σ1 * A.1)).re    | Sum.inr 1 => 1/2 * (Matrix.trace (σ2 * A.1)).re    | Sum.inr 2 => 1/2 * (Matrix.trace (σ3 * A.1)).re  use c  simp only [one_div, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,    Finset.sum_singleton, Fin.sum_univ_three, c]  apply selfAdjoint_ext  · simp only [pauliSelfAdjoint, AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add,    Algebra.mul_smul_comm, trace_add, trace_smul, σ0_σ0_trace, real_smul, ofReal_mul, ofReal_inv,    ofReal_ofNat, σ0_σ1_trace, smul_zero, σ0_σ2_trace, add_zero, σ0_σ3_trace, mul_re, inv_re,    re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero, zero_div,    ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]    ring  · simp only [pauliSelfAdjoint, AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add,    Algebra.mul_smul_comm, trace_add, trace_smul, σ1_σ0_trace, smul_zero, σ1_σ1_trace, real_smul,    ofReal_mul, ofReal_inv, ofReal_ofNat, σ1_σ2_trace, add_zero, σ1_σ3_trace, zero_add, mul_re,    inv_re, re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero,    zero_div, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]    ring  · simp only [pauliSelfAdjoint, AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add,    Algebra.mul_smul_comm, trace_add, trace_smul, σ2_σ0_trace, smul_zero, σ2_σ1_trace, σ2_σ2_trace,    real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, zero_add, σ2_σ3_trace, add_zero, mul_re,    inv_re, re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero,    zero_div, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]    ring  · simp only [pauliSelfAdjoint, AddSubgroup.coe_add, selfAdjoint.val_smul, mul_add,    Algebra.mul_smul_comm, trace_add, trace_smul, σ3_σ0_trace, smul_zero, σ3_σ1_trace, σ3_σ2_trace,    add_zero, σ3_σ3_trace, real_smul, ofReal_mul, ofReal_inv, ofReal_ofNat, zero_add, mul_re,    inv_re, re_ofNat, normSq_ofNat, div_self_mul_self', ofReal_re, inv_im, im_ofNat, neg_zero,    zero_div, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul]    ring