-- 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 : ↥b.support
inst_10 : P.IsReduced
this_1 : InvolutiveNeg ι := P.indexNeg
this_2 : Module.IsReflexive R M
this : IsAddTorsionFree M
a : ∀ (k l : ↥b.support), ⁅e i, f i⁆ (Sum.inl k) (Sum.inl l) = h i (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
a₄ : ∀ (k : ↥b.support) (l : ι), ⁅e i, f i⁆ (Sum.inl k) (Sum.inr l) = h i (Sum.inl k) (Sum.inr l)
a₅ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
a₆ : ∀ (k l : ι), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
a₇ : ∀ (k : ι) (l : ↥b.support), ⁅e i, f i⁆ (Sum.inr k) (Sum.inl l) = h i (Sum.inr k) (Sum.inl l)
a₈ a₉ : ∀ (k l : ι), ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
⊢ ⁅e i, f i⁆ = h i

Tactic:
classical
  ext (k | k) (l | l)
  · simp [e, f, h]
  · have h₁ (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ k = i ∧ x = -i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero, sub_eq_add_neg] at contra
    have h₂ (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ k = i ∧ x = i) := by
      simp only [not_and]
      rintro contra rfl rfl
      simp [P.ne_zero] at contra
    simp [e, f, h, h₁, h₂, -indexNeg_neg, ← ite_and]
  · simp [e, f, h]
  · rcases eq_or_ne k i with rfl | hki
    · have hx (x : ι) : ¬ (P.root x = P.root i + P.root l ∧ P.root i = P.root x - P.root i) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := i) ⟨x, ?_⟩
        rwa [eq_sub_iff_add_eq, ← two_smul ℕ, eq_comm] at contra
      simp only [e, f, h, P.ne_zero, P.ne_neg, Ring.lie_def, Fintype.sum_sum_type, Matrix.sub_apply,
        Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, Matrix.fromBlocks_apply₂₂,
        left_eq_add, zero_mul, mul_zero, ite_mul, mul_ite, ← ite_and]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [hx, eq_comm]
    rcases eq_or_ne k (-i) with rfl | hki'
    · have hx (x : ι) : ¬ (P.root x = P.root l - P.root i ∧ P.root (-i) = P.root i + P.root x) := by
        rintro ⟨-, contra⟩
        refine P.nsmul_notMem_range_root (n := 2) (i := -i) ⟨x, ?_⟩
        replace contra : P.root x = -(P.root i + P.root i) := by
          simpa [neg_eq_iff_add_eq_zero, ← add_assoc, add_eq_zero_iff_eq_neg'] using contra
        simp [contra, two_smul]
      have aux (x : ι) : ¬ P.root (-i) = P.root x - P.root i := by
        simp [P.ne_zero x, eq_comm]
      simp only [e, f, h, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
        Matrix.fromBlocks_apply₂₁, Matrix.of_apply, hki, reduceIte, zero_mul, Finset.sum_const_zero,
        Matrix.fromBlocks_apply₂₂, mul_ite, ite_mul, mul_zero, ← ite_and, if_neg (hx _), add_zero,
        aux, zero_sub, Matrix.diagonal_apply]
      rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]
      simp [eq_comm, apply_ite ((-·) : R → R)]
    rcases eq_or_ne k l with rfl | hkl
    · exact lie_e_f_same_aux i k hki hki'
    · simp_all [h, e, f]

Premises used: Finset.mem_univ, left_eq_add, Finset.sum_eq_single_of_mem, Matrix.fromBlocks_apply₂₂, RootPairing.GeckConstruction.f, RootPairing.ne_zero, MulZeroClass.zero_mul, RootPairing.GeckConstruction.h, Fintype.sum_sum_type, Matrix.sub_apply, mul_ite, apply_ite, Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, eq_comm, Finset.sum_const_zero, MulZeroClass.mul_zero, ite_mul, Matrix.diagonal_apply, reduceIte, Ring.lie_def, RootPairing.ne_neg, ite_and, add_zero, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e, Neg.neg, rfl, zero_sub