Lean4
/-- Lemma 3.3 (a) from [Geck](Geck2017). -/
theorem lie_h_e : ⁅h j, e i⁆ = b.cartanMatrix i j • e i := by
classical
ext (k | k) (l | l)
· simp [h, e]
· simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₁₂,
Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]
rw [Finset.sum_eq_ite l (by aesop)]
aesop
· simp only [h, e]
aesop
· simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂, Matrix.of_apply, mul_ite, mul_one,
mul_zero, ite_self, Finset.sum_const_zero, Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul,
Matrix.smul_apply, smul_ite, smul_add, zsmul_eq_mul, smul_zero]
rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ { k, l }) (by aesop)]
rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true, reduceIte, right_eq_add,
ite_self, add_zero, zero_add, ite_sub_ite, sub_self, Base.cartanMatrix, Base.cartanMatrixIn_def]
refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
ring
