-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
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
k : ι
hki : k ≠ (↑i : ι)
hki' : k ≠ (P.reflectionPerm (↑i : ι) : (a : ι) → ι) (↑i : ι)
have :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
have₁ :
  ∀
    (h_lin_ind :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)),
    ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
have₂ :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)
have₃ have₄ :
  ∀
    (h_lin_ind :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)),
    ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)
have have₅ : ∀
  (h_lin_ind :
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) k] : Fin (Nat.succ 0).succ → M)),
  HSub.hSub (α := R)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) k =
              HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
          HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) 1
        else 0) =
    HSub.hSub (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
Tactic: classical
  have h_lin_ind : LinearIndependent R ![P.root i, P.root k] := by
    rw [LinearIndependent.pair_symm_iff, IsReduced.linearIndependent_iff]
    refine ⟨hki, ?_⟩
    rwa [ne_eq, root_eq_neg_iff]
  suffices (∑ x, if P.root k = P.root i + P.root x then
              (P.chainBotCoeff i x + 1 : R) * (P.chainTopCoeff i k + 1) else 0) -
            (∑ x, if P.root k = P.root x - P.root i then
              (P.chainTopCoeff i x + 1 : R) * (P.chainBotCoeff i k + 1) else 0) =
      P.chainBotCoeff i k - P.chainTopCoeff i k by
    have aux (x : ι) : P.root x = P.root k - P.root i ↔ P.root k = P.root i + P.root x := by
      rw [eq_sub_iff_add_eq', eq_comm]
    have aux' (x : ι) : P.root x = P.root i + P.root k ↔ P.root k = P.root x - P.root i := by
      rw [eq_sub_iff_add_eq', eq_comm]
    simpa [e, f, h, hki, hki', aux, aux', ← ite_and, ← P.chainBotCoeff_sub_chainTopCoeff h_lin_ind]
  rcases exists_or_forall_not (fun x ↦ P.root k = P.root i + P.root x) with ⟨x, hx⟩ | h₁ <;>
  rcases exists_or_forall_not (fun x ↦ P.root k = P.root x - P.root i) with ⟨y, hy⟩ | h₂
  · have h_lin_ind_x : LinearIndependent R ![P.root i, P.root x] := by simpa [hx] using h_lin_ind
    have h_lin_ind_y : LinearIndependent R ![P.root i, P.root y] := by
      rw [← add_eq_of_eq_sub hy, add_comm]; simpa
    have hx' : P.chainBotCoeff i k = P.chainBotCoeff i x + 1 :=
      chainBotCoeff_of_add h_lin_ind_x (add_comm (P.root i) _ ▸ hx)
    have hy' : P.chainTopCoeff i k = P.chainTopCoeff i y + 1 := chainTopCoeff_of_sub h_lin_ind_y hy
    rw [Finset.sum_eq_single_of_mem x (Finset.mem_univ _) (by aesop),
      Finset.sum_eq_single_of_mem y (Finset.mem_univ _) (by aesop)]
    simp only [hx, hy.symm, hx', hy', reduceIte, Nat.cast_add]
    ring
  · simp_rw [if_neg (h₂ _), Finset.sum_const_zero, sub_zero]
    replace h₂ : P.chainTopCoeff i k = 0 :=
      P.chainTopCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₂ x <| by simp [hx]
    have h_lin_ind_x : LinearIndependent R ![P.root i, P.root x] := by simpa [hx] using h_lin_ind
    have hx' : P.chainBotCoeff i k = P.chainBotCoeff i x + 1 :=
      chainBotCoeff_of_add h_lin_ind_x (add_comm (P.root i) _ ▸ hx)
    simp [hx, hx', h₂]
  · simp_rw [if_neg (h₁ _), Finset.sum_const_zero, zero_sub]
    replace h₁ : P.chainBotCoeff i k = 0 :=
      P.chainBotCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₁ x <| by simp [hx]
    have h_lin_ind_y : LinearIndependent R ![P.root i, P.root y] := by
      rw [← add_eq_of_eq_sub hy, add_comm]; simpa
    have hy' : P.chainTopCoeff i k = P.chainTopCoeff i y + 1 := chainTopCoeff_of_sub h_lin_ind_y hy
    simp [hy, hy', h₁]
  · suffices P.chainBotCoeff i k = 0 ∧ P.chainTopCoeff i k = 0 by simp [h₁, h₂, this]
    exact ⟨P.chainBotCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₁ x <| by simp [hx],
           P.chainTopCoeff_eq_zero_iff.mpr <| Or.inr fun ⟨x, hx⟩ ↦ h₂ x <| by simp [hx]⟩