-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
a₄ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
a₅ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
a₆ : ∀ (k l : ι), ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
a₇ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
a₈ a₉ : ∀ (k l : ι), ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i

Tactic:
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

Premises used: RootPairing.Base.cartanMatrixIn_def, Finset.mem_singleton, zsmul_eq_mul, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Matrix.zero_apply, RootPairing.ne_zero, sub_self, ite_self, MulZeroClass.zero_mul, RootPairing.GeckConstruction.h, Fintype.sum_sum_type, smul_zero, Matrix.sub_apply, mul_ite, Int.cast_add, Matrix.mul_apply, ite_sub_ite, Matrix.smul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, zero_add, Finset.sum_const_zero, MulZeroClass.mul_zero, Finset.sum_singleton, RootPairing.Base.cartanMatrix, smul_ite, Finset.sum_sub_distrib, ite_mul, Matrix.diagonal_apply, reduceIte, Ring.lie_def, mul_one, Finset.sum_insert, right_eq_add, add_zero, ite_congr, not_false_eq_true, RootPairing.indexNeg_neg, Subtype.val, RootPairing.GeckConstruction.e, smul_add, rfl