-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain 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
i j : ι
aux :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M) ↔
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i,
          (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
        Fin (Nat.succ 0).succ → M)
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
h' :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
S₁ : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S₁_def :
  S₁ =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S₂ : Set ℤ :=
  {z : ℤ |
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HAdd.hAdd (α := M)
        ((P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M)
        (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
S₂_def :
  S₂ =
    {z : ℤ |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M)
          ((P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : M)
          (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)))}
hS₁₂ :
  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ) =
      HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
        (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) ∧
    Eq (α := ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      0
hS₁ :
  S₁ =
    Icc (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
hS₂ :
  S₂ =
    Icc
      (-(↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
              (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
          ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
pos pos₁ pos₂ pos₃ :
  ∀
    (hS₁₂ :
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
          chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
            chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
          0),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
        chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
          chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
        0
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ∧
    chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) =
      0

Tactic:
norm_cast at hS₁₂