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
z : ℤ
hz : z ∈ S
this :
  ∀ (z' : ℤ) (hz' : z' ∈ S),
    Eq.{u_1 + 1} (α := ι)
        ((fun (z : (↑S : Type)) ↦
            Exists.choose (p := fun (y : ι) ↦
              (P.root : (a : ι) → M) y =
                HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
                  (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
              ⋯)
          (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
        ((fun (z : (↑S : Type)) ↦
            Exists.choose (p := fun (y : ι) ↦
              (P.root : (a : ι) → M) y =
                HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
                  (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
              ⋯)
          (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz')) →
      Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'
⊢ ∀ ⦃a₂ : (↑S : Type)⦄,
    Eq.{u_1 + 1} (α := ι)
        ((fun (z : (↑S : Type)) ↦
            Exists.choose (p := fun (y : ι) ↦
              (P.root : (a : ι) → M) y =
                HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
                  (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
              ⋯)
          (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
        ((fun (z : (↑S : Type)) ↦
            Exists.choose (p := fun (y : ι) ↦
              (P.root : (a : ι) → M) y =
                HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
                  (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
              ⋯)
          a₂) →
      Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = a₂

Tactic:
⟨z', hz'⟩
-- 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
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
this : Module.IsReflexive R M
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
⊢ HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)

Tactic:
have : z • P.root i = z' • P.root i := by
      rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
-- 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
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)
⊢ Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'

Tactic:
Subtype.ext <| smul_left_injective ℤ (P.ne_zero i) this

Premises used: RootPairing.ne_zero, smul_left_injective, Int, Subtype.ext
-- 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
z : ℤ
hz : z ∈ S
z' : ℤ
hz' : z' ∈ S
hzz :
  Eq.{u_1 + 1} (α := ι)
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz))
    ((fun (z : (↑S : Type)) ↦
        Exists.choose (p := fun (y : ι) ↦
          (P.root : (a : ι) → M) y =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (↑z : ℤ) ((P.root : (a : ι) → M) i : M)))
          ⋯)
      (Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'))
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)
⊢ Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'

Tactic:
exact Subtype.ext <| smul_left_injective ℤ (P.ne_zero i) this

Premises used: RootPairing.ne_zero, smul_left_injective, Int, Subtype.ext
-- 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
⊢ S.Finite

Tactic:
have h_fin : S.Finite := by
    suffices Injective (fun z : S ↦ z.property.choose) from Finite.of_injective _ this
    intro ⟨z, hz⟩ ⟨z', hz'⟩ hzz
    have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
    have : IsAddTorsionFree M := .of_isTorsionFree R M
    have : z • P.root i = z' • P.root i := by
      rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
    exact Subtype.ext <| smul_left_injective ℤ (P.ne_zero i) 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 :
  ∀ (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
⊢ 0 ∈ S

Tactic:
simp [S_def]
-- 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
⊢ S.Nonempty

Tactic:
have h_ne : S.Nonempty := ⟨0, by simp [S_def]⟩
-- 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
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p

Tactic:
⟨sInf S, csInf_le h_fin.bddBelow hS₀, sSup S, le_csSup h_fin.bddAbove hS₀,
    (h_ne.eq_Icc_iff_int h_fin.bddBelow h_fin.bddAbove).mpr fun r ⟨k, hk⟩ s ⟨l, hl⟩ hrs ↦ ?_⟩

Premises used: Iff.mpr, Set.Nonempty.eq_Icc_iff_int, LE.le, Set.Finite.bddBelow, _private.0.RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent.match_2, HAdd.hAdd, And.intro, Exists.intro, le_csSup, Set.Finite.bddAbove, OfNat.ofNat, csInf_le, InfSet.sInf, SupSet.sSup
-- 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
refine :
  ∀ r ∈ S,
    ∀ 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))),
        s ≤ r + 1
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p

Tactic:
refine ⟨sInf S, csInf_le h_fin.bddBelow hS₀, sSup S, le_csSup h_fin.bddAbove hS₀,
    (h_ne.eq_Icc_iff_int h_fin.bddBelow h_fin.bddAbove).mpr fun r ⟨k, hk⟩ s ⟨l, hl⟩ hrs ↦ ?_⟩
-- 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))
by_contra! : ∀ (contra : r + 1 < s), False
⊢ s ≤ r + 1

Tactic:
by_contra! contra
-- 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
rw :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M)))
      ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) (r + 1) ((P.root : (a : ι) → M) i : M))
⊢ HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) (r + 1) ((P.root : (a : ι) → M) i : M))

Tactic:
rw [hk]
-- 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
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) r ((P.root : (a : ι) → M) i : M)))
      ((P.root : (a : ι) → M) i : M) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) (r + 1) ((P.root : (a : ι) → M) i : M))

Tactic:
module