Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hx : ∀ (x : ι), ¬(P.root x = P.root ↑i + P.root l ∧ P.root ↑i = P.root x - P.root ↑i)
⊢ ((∑ x,
          if True then
            ↑|b.cartanMatrix i x| *
              Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = ↑i then 1 else 0)
                (Matrix.of fun i' j ↦ if i' = -↑i then ↑|b.cartanMatrix i j| else 0)
                (Matrix.of fun i' j ↦ if P.root i' = P.root j - P.root ↑i then ↑(chainTopCoeff (↑i) j) + 1 else 0)
                (Sum.inl x) (Sum.inr l)
          else 0) +
        ∑ a₂,
          if P.root a₂ = P.root l - P.root ↑i ∧ False then
            (↑(chainBotCoeff (↑i) a₂) + 1) * (↑(chainTopCoeff (↑i) l) + 1)
          else 0) -
      ((∑ x,
          if False then
            ↑|b.cartanMatrix i x| *
              Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
                (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
                (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
                (Sum.inl x) (Sum.inr l)
          else 0) +
        ∑ a₂,
          if P.root a₂ = P.root ↑i + P.root l ∧ P.root ↑i = P.root a₂ - P.root ↑i then
            (↑(chainTopCoeff (↑i) a₂) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
          else 0) =
    Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (↑i) l

Tactic:
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]

Goal state after:
case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hx : ∀ (x : ι), ¬(P.root x = P.root ↑i + P.root l ∧ P.root ↑i = P.root x - P.root ↑i)
⊢ ((if True then
          ↑|b.cartanMatrix i i| *
            Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = ↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = -↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root j - P.root ↑i then ↑(chainTopCoeff (↑i) j) + 1 else 0)
              (Sum.inl i) (Sum.inr l)
        else 0) +
        ∑ a₂,
          if P.root a₂ = P.root l - P.root ↑i ∧ False then
            (↑(chainBotCoeff (↑i) a₂) + 1) * (↑(chainTopCoeff (↑i) l) + 1)
          else 0) -
      ((∑ x,
          if False then
            ↑|b.cartanMatrix i x| *
              Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
                (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
                (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
                (Sum.inl x) (Sum.inr l)
          else 0) +
        ∑ a₂,
          if P.root a₂ = P.root ↑i + P.root l ∧ P.root ↑i = P.root a₂ - P.root ↑i then
            (↑(chainTopCoeff (↑i) a₂) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
          else 0) =
    Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (↑i) l