-- 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
l : ι
hx :
  ∀ (x : ι),
    ¬((P.root : (a : ι) → M) x =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
        (P.root : (a : ι) → M) (↑i : ι) =
          HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M))
a :
  HAdd.hAdd (α := R)
        (∑ x : ↥b.support,
          if True then
            HMul.hMul (α := R) (↑|b.cartanMatrix i x| : R)
              (Matrix.fromBlocks (l := ↥b.support) (o := ι) 0
                ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
                  if i' = i ∧ j = (↑i : ι) then 1 else 0)
                ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
                  if i' = -(↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
                ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
                  if
                      (P.root : (a : ι) → M) i' =
                        HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : 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 : ι) j) : R) 1
                  else 0)
                (Sum.inl x) (Sum.inr l))
          else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) (↑i : ι) : M) ∧
                False 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 : ι) l) : R) 1
          else 0) -
      HAdd.hAdd (α := R)
        (∑ x : ↥b.support,
          if False then
            HMul.hMul (α := R) (↑|b.cartanMatrix i x| : R)
              (Matrix.fromBlocks (l := ↥b.support) (o := ι) 0
                ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
                  if i' = i ∧ j = -(↑i : ι) then 1 else 0)
                ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
                  if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
                ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
                  if
                      (P.root : (a : ι) → M) i' =
                        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
                          ((P.root : (a : ι) → M) j : M) then
                    HAdd.hAdd (α := R)
                      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
                  else 0)
                (Sum.inl x) (Sum.inr l))
          else 0)
        (∑ x : ι,
          if
              (P.root : (a : ι) → M) x =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) ∧
                (P.root : (a : ι) → M) (↑i : ι) =
                  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 : ι) l) : R) 1
          else 0) =
    Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) (↑i : ι) l
⊢ ⁅e i, f i⁆ (Sum.inr (↑i : ι)) (Sum.inr l) = h i (Sum.inr (↑i : ι)) (Sum.inr l)

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

Premises used: left_eq_add, Matrix.fromBlocks_apply₂₂, RootPairing.GeckConstruction.f, RootPairing.ne_zero, MulZeroClass.zero_mul, RootPairing.GeckConstruction.h, Fintype.sum_sum_type, Matrix.sub_apply, mul_ite, Matrix.mul_apply, Matrix.fromBlocks_apply₂₁, Matrix.of_apply, MulZeroClass.mul_zero, ite_mul, Ring.lie_def, RootPairing.ne_neg, ite_and, RootPairing.GeckConstruction.e