-- 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 j k : ↥b.support
l : ι
⊢ ∑ x : ↥b.support,
        HMul.hMul (α := R) (β := R)
          (Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R))
              (Sum.inl k) (Sum.inl x) :
            R)
          ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R)
              (fun (i' : ↥b.support) (j : ι) ↦ if i' = i ∧ j = -(↑i : ι) then 1 else 0) x l :
            R) -
      HAdd.hAdd (α := R)
        (∑ x : ↥b.support,
          HMul.hMul (α := R)
            (Matrix.fromBlocks (m := ι) (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 k) (Sum.inl x))
            0)
        (∑ x : ι,
          HMul.hMul (α := R) (β := R)
            ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R)
                (fun (i' : ↥b.support) (j : ι) ↦ if i' = i ∧ j = -(↑i : ι) then 1 else 0) k x :
              R)
            (Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
                (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) (Sum.inr x) (Sum.inr l) :
              R)) =
    HSMul.hSMul (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (b.cartanMatrix i j)
      (Matrix.fromBlocks 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 k) (Sum.inr l)
have a : ∑ x : ↥b.support,
      HMul.hMul (α := R) (β := R)
        (Matrix.fromBlocks (m := ι) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) (Sum.inl k)
            (Sum.inl x) :
          R)
        ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R)
            (fun (i' : ↥b.support) (j : ι) ↦ if i' = i ∧ j = -(↑i : ι) then 1 else 0) x l :
          R) -
    (∑ x : ↥b.support,
        HMul.hMul (α := R)
          (Matrix.fromBlocks (m := ι) (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 k) (Sum.inl x))
          0 +
      if Membership.mem (γ := Finset ι) Finset.univ l then
        HMul.hMul (α := R) (β := R)
          ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R)
              (fun (i' : ↥b.support) (j : ι) ↦ if i' = i ∧ j = -(↑i : ι) then 1 else 0) k l :
            R)
          (Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
              (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) (Sum.inr l) (Sum.inr l) :
            R)
      else 0) =
  HSMul.hSMul (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (b.cartanMatrix i j)
    (Matrix.fromBlocks 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 k) (Sum.inr l)
Tactic: rw [Finset.sum_eq_ite l (by aesop)]