awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
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)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ (P.coroot' i : (a : M) → R)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))) =
    P.pairing j i +
      HMul.hMul (α := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) s : R) ((algebraMap ℤ R : (a : ℤ) → R) 2 : R)

Tactic:
simp
-- 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 :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
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)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
⊢ P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2

Tactic:
have h₄ : P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2 := by
    apply algebraMap_injective ℤ R
    rw [algebraMap_pairingIn, map_add, map_mul, algebraMap_pairingIn, ← root_coroot'_eq_pairing, hl]
    simp
-- 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 :
  ∀ (s t : ℤ),
    HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) j : M) = 0 →
      s = 0 ∧ t = 0
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)))}
hS₀ : 0 ∈ S
h_fin : S.Finite
h_ne : S.Nonempty
r : ℤ
h_1 : r ∈ S
s : ℤ
h_2 : s ∈ S
hrs : Disjoint (Ioo r s) S
k : ι
hk :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M))
l : ι
hl :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) s ((P.root : (a : ι) → M) i : M))
contra : r + 1 < s
hki_notMem :
  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hki_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli_notMem :
  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
hli_ne : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
h₁ : 0 ≤ P.pairingIn ℤ k i
h₂ : P.pairingIn ℤ k i = P.pairingIn ℤ j i + r * 2
h₃ : P.pairingIn ℤ l i ≤ 0
h₄ : P.pairingIn ℤ l i = P.pairingIn ℤ j i + s * 2
⊢ False

Tactic:
lia
-- 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)
⊢ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0

Tactic:
simp only [chainTopCoeff, h, reduceDIte]

Premises used: reduceDIte, RootPairing.chainTopCoeff
-- 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)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j = 0

Tactic:
simp only [chainBotCoeff, h, reduceDIte]

Premises used: reduceDIte, RootPairing.chainBotCoeff
-- 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 : ℕ
⊢ let 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 =
    {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)))}

Tactic:
set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def

Premises used: Int, RootPairing.root, Set.range, DFunLike.coe, Set
-- 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)))}
this : (↑n : ℤ) ∈ S ↔ n ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ 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) n ((P.root : (a : ι) → M) i : M))) ↔
    n ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j

Tactic:
simpa only [S_def, mem_setOf_eq, natCast_zsmul] using this

Premises used: Set.mem_setOf_eq, natCast_zsmul
-- 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)))}
suffices : (↑n : ℤ) ∈ S ↔ n ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ 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) n ((P.root : (a : ι) → M) i : M))) ↔
    n ≤ chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j

Tactic:
suffices (n : ℤ) ∈ S ↔ n ≤ P.chainTopCoeff i j by
    simpa only [S_def, mem_setOf_eq, natCast_zsmul] using this
-- 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)))}
⊢ 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

Tactic:
simp [chainTopCoeff, h]

Premises used: RootPairing.chainTopCoeff
-- 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)))}
⊢ 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

Tactic:
have aux : P.chainTopCoeff i j =
      (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose.toNat := by
    simp [chainTopCoeff, h]
-- 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
⊢ ⋯.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

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
-- 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)))}
this : -(↑n : ℤ) ∈ S ↔ n ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M))) ↔
    n ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j

Tactic:
simpa only [S_def, mem_setOf_eq, neg_smul, natCast_zsmul, ← sub_eq_add_neg] using this

Premises used: neg_smul, sub_eq_add_neg, Set.mem_setOf_eq, natCast_zsmul
-- 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)))}
suffices : -(↑n : ℤ) ∈ S ↔ n ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M))) ↔
    n ≤ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j

Tactic:
suffices -(n : ℤ) ∈ S ↔ n ≤ P.chainBotCoeff i j by
    simpa only [S_def, mem_setOf_eq, neg_smul, natCast_zsmul, ← sub_eq_add_neg] using this
-- 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)))}
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j =
    (-⋯.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)).toNat

Tactic:
simp [chainBotCoeff, h]

Premises used: RootPairing.chainBotCoeff