-- 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
k l : ι
a :
  ∑ x ∈ {k, k},
      ((if
            (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) then
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) k x *
            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) -
        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 *
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x k
        else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) then
      HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) +
        (↑(b.cartanMatrix i j) : R)
    else 0
a₁ :
  ∀ (hkl : k ≠ l),
    ∑ x ∈ {k, l},
        ((if
              (P.root : (a : ι) → M) x =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) k x *
              HAdd.hAdd (α := R)
                (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1
          else 0) -
          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 *
              Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
          else 0) =
      if
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
        HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
            (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
          (↑(b.cartanMatrix i j) : R)
      else 0
⊢ ∑ x ∈ {k, l},
      ((if
            (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) k x *
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1
        else 0) -
        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 *
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
        else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
        (↑(b.cartanMatrix i j) : R)
    else 0

Tactic:
rcases eq_or_ne k l with rfl | hkl

Premises used: eq_or_ne, rfl