-- 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 : ι
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)
n : ℕ
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)))}
aux :
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j =
    ⋯.choose (p := fun (p : ℤ) ↦
        p ≥ 0 ∧
          {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)))} =
            Icc
              (⋯.choose (p := fun (q : ℤ) ↦
                q ≤ 0 ∧
                  ∃ p ≥ 0,
                    {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)))} =
                      Icc q p))
              p).toNat
hp :
  ⋯.choose (p := fun (p : ℤ) ↦
      p ≥ 0 ∧
        {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)))} =
          Icc
            (⋯.choose (p := fun (q : ℤ) ↦
              q ≤ 0 ∧
                ∃ p ≥ 0,
                  {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)))} =
                    Icc q p))
            p) ≥
    0
⊢ S =
    Icc
      (⋯.choose (p := fun (q : ℤ) ↦
        q ≤ 0 ∧
          ∃ p ≥ 0,
            {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)))} =
              Icc q p))
      (⋯.choose (p := fun (p : ℤ) ↦
        p ≥ 0 ∧
          {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)))} =
            Icc
              (⋯.choose (p := fun (q : ℤ) ↦
                q ≤ 0 ∧
                  ∃ p ≥ 0,
                    {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)))} =
                      Icc q p))
              p))

Tactic:
obtain ⟨hp, h₂ : S = _⟩ :=
    (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose_spec

Premises used: Exists.choose_spec, RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent, And.right