-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ HAdd.hAdd (α := R)
      (∑ x : ↥b.support,
        if x = i ∧ l = -(↑i : ι) then
          HMul.hMul (α := R)
            (Matrix.fromBlocks (m := ι) (o := ι) 1 0 0
              ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inl k)
              (Sum.inl x))
            1
        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) then
          0 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) =
    ∑ 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' =
                    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 k) (Sum.inl x))
          (0 x l) +
      if Membership.mem (γ := Finset ι) Finset.univ (-l) then
        HMul.hMul (α := R) (if k = i ∧ -l = (↑i : ι) then 1 else 0) 1
      else 0
have a : ((if i = i ∧ l = -(↑i : ι) then
      HMul.hMul (α := R)
        (Matrix.fromBlocks (m := ι) (o := ι) 1 0 0
          ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inl k)
          (Sum.inl i))
        1
    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) then
        0 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) =
  ∑ 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' =
                  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 k) (Sum.inl x))
        (0 x l) +
    if Membership.mem (γ := Finset ι) Finset.univ (-l) then
      HMul.hMul (α := R) (if k = i ∧ -l = (↑i : ι) then 1 else 0) 1
    else 0
Tactic: rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]