awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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)
⊢ ∃ 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
have 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
Tactic: replace h := LinearIndependent.pair_iff.mp <| h.restrict_scalars' ℤ
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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
⊢ ∃ 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
have set : 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_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)))}),
  ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
Tactic: set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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)))}
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
have hS₀ : 0 ∈ S
Tactic: have hS₀ : 0 ∈ S := by simp [S]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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
have suffices : Injective.{1, 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)))
    sorry
Tactic: suffices Injective (fun z : S ↦ z.property.choose) from Finite.of_injective _ this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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
⊢ ∀ ⦃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₂
have 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)))
            sorry)
        (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)))
            sorry)
        (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'
Tactic: ⟨z', hz'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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'))
⊢ Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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
⊢ Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'
have this₁ : IsAddTorsionFree M
Tactic: have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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)
have rwa : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
Tactic: rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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
rwa :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)
have rwa₁ : (P.root : (a : ι) → M)
    (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)))
      hz) =
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
Tactic: rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
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
rwa :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M)) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
rwa₁ :
  (P.root : (a : ι) → M)
      (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)))
        hz) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (β := M) z ((P.root : (a : ι) → M) i : M) = HSMul.hSMul (β := M) z' ((P.root : (a : ι) → M) i : M)
have rwa₂ : Eq.{u_3 + 1} (α := M)
  ((P.root : (a : ι) → M)
      (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)))
        hz) :
    M)
  ((P.root : (a : ι) → M)
      (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)))
        hz') :
    M)
Tactic: rwa [← add_right_inj (P.root j), ← hz.choose_spec, ← hz'.choose_spec, P.root.injective.eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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
⊢ Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z hz = Subtype.mk (p := fun (x : ℤ) ↦ x ∈ S) z' hz'
have this₁ : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
have h_fin : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
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
⊢ ∃ q ≤ 0, ∃ p ≥ 0, S = Icc q p
have h_ne : S.Nonempty
Tactic: have h_ne : S.Nonempty := ⟨0, by simp [S_def]⟩