-- 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₁₂ :
  S₂ = (fun (z : ℤ) ↦ -(↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) + z) '' S₁
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)) :
        ℤ)
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
⊢ 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) : ℤ)

Tactic:
rw [hS₁, hS₂, image_const_add_Icc, neg_add_cancel, Icc_eq_Icc_iff (by simp), neg_eq_iff_eq_neg,
    neg_add_rev, neg_neg, neg_neg] at hS₁₂

Premises used: neg_add_rev, neg_neg, neg_eq_iff_eq_neg, Set.image_const_add_Icc, Set.Icc_eq_Icc_iff, neg_add_cancel