-- 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) : ℤ)
x : ℤ
h₁ :
  Membership.mem (γ := 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)))}
      x ↔
    Membership.mem (γ := Set ℤ)
      (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)) :
          ℤ))
      x
h₂ :
  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) x ((P.root : (a : ι) → M) i : M))) ↔
    Membership.mem (γ := Set ℤ)
      (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)) :
          ℤ))
      x
h₃ h₄ :
  Membership.mem (γ := Set ℤ)
      (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)) :
          ℤ))
      x ↔
    Membership.mem (γ := Set ℤ)
      (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)) :
          ℤ))
      x
⊢ x ∈ S₂ ↔
    Membership.mem (γ := Set ℤ)
      (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)) :
          ℤ))
      x

Tactic:
rw [S₂_def, mem_setOf_eq, root_add_zsmul_mem_range_iff h']

Premises used: Set.mem_setOf_eq, RootPairing.root_add_zsmul_mem_range_iff