awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p q : K[X]
h : q ≠ 0
h0 :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
    0
h1 :
  LT.lt.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
      Γ)
    (1 : Γ)
h0₁ : ¬p = 0 ∧ ¬q = 0
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
have h1₁ : HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) <
  1
Tactic: simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p q : K[X]
h : ¬q = 0
h0 : ¬p = 0 ∧ ¬q = 0
h1 :
  HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) <
    1
⊢ ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∨
    ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) (1 : Γ)
have rw : ¬(Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧
    Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) (1 : Γ))
Tactic: rw [← not_and_or]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p q : K[X]
h : ¬q = 0
h0 : ¬p = 0 ∧ ¬q = 0
h1 :
  HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) <
    1
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬p = 0}
have hor : ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∨
  ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) (1 : Γ)
Tactic: have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; aesop
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p q : K[X]
h : ¬q = 0
h0 : ¬p = 0 ∧ ¬q = 0
h1 :
  HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) <
    1
hor :
  ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∨
    ¬Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) (1 : Γ)
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬p = 0}
have f : ∀ (r : K[X]),
  Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑r : K⟮X⟯) : Γ) (1 : Γ) →
    r ≠ 0 →
      Set.Nonempty.{u_1} (α := K[X])
        {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬p = 0}
Tactic: suffices ∀ r : K[X], v (↑r) ≠ 1 → r ≠ 0 → {p : K[X] | v ↑p < 1 ∧ ¬p = 0}.Nonempty by
      exact Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
w : K⟮X⟯
h0 : w ≠ 0
h1 : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) w : Γ) (1 : Γ)
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
have f : ∀ (p q : K[X]),
  q ≠ 0 →
    ∀
      (h0 :
        HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
          0)
      (h1 :
        LT.lt.{u_2} (α := Γ)
          ((v : (a : K⟮X⟯) → Γ)
              (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
                ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
            Γ)
          (1 : Γ)),
      Set.Nonempty.{u_1} (α := K[X])
        {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
Tactic: induction w using RatFunc.induction_on with
  | f p q =>
    simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *
    have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; aesop
    suffices ∀ r : K[X], v (↑r) ≠ 1 → r ≠ 0 → {p : K[X] | v ↑p < 1 ∧ ¬p = 0}.Nonempty by
      exact Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)
    exact fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr
      ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩
Cleared hypotheses: w, h0, h1
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
a b : K[X]
hab : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
⊢ a.degree < πᵥ.degree
have hbpos : 0 < b.degree
Tactic: have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
a b : K[X]
hab : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < b.degree
⊢ a.degree < πᵥ.degree
have simp_rw : ∀ (hbpos : LT.lt (α := WithBot ℕ) 0 (↑b.natDegree : WithBot ℕ)),
  (↑a.natDegree : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑a.natDegree : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
Tactic: simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢
Cleared hypotheses: hbpos
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
a b : K[X]
hab : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : LT.lt (α := WithBot ℕ) 0 (↑b.natDegree : WithBot ℕ)
⊢ (↑a.natDegree : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑a.natDegree : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
have norm_cast : a.natDegree < a.natDegree + b.natDegree
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
a b : K[X]
hab : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
⊢ LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
have hda : a.degree < πᵥ.degree
Tactic: have hda : a.degree < πᵥ.degree := by
    have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb
    simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢
    norm_cast
    simpa using hbpos
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
a b : K[X]
hab : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hda : a.degree < πᵥ.degree
⊢ LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
have hlea : a ∉ {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
Tactic: have hlea := imp_not_comm.mp (degree_lt_wf.not_lt_min _) hda
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
⊢ Irreducible πᵥ
have hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
Tactic: have hπᵥ : v πᵥ < 1 ∧ πᵥ ≠ 0 := degree_lt_wf.min_mem _ hne
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
⊢ Irreducible πᵥ
have refine_1 : ¬IsUnit πᵥ
Tactic: refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
refine_1 : ¬IsUnit πᵥ
⊢ Irreducible πᵥ
have refine_2 : ∀ (a b : K[X]) (hab : πᵥ = a * b), IsUnit a ∨ IsUnit b
Tactic: refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
⊢ ¬IsUnit πᵥ
have refine_1 : ¬∃ (r : K), r ≠ 0 ∧ (Polynomial.C : (a : K) → K[X]) r = πᵥ
Tactic: simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
a : K
ha0 : a ≠ 0
ha : (Polynomial.C : (a : K) → K[X]) a = πᵥ
⊢ False
have hπᵥ₁ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K K⟮X⟯ : (a : K) → K⟮X⟯) a : K⟮X⟯) : Γ) (1 : Γ) ∧
  Ne (α := K[X]) ((Polynomial.C : (a : K) → K[X]) a : K[X]) (0 : K[X])
Tactic: rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ
Cleared hypotheses: hπᵥ, ha0, ha
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
a b : K[X]
hab : πᵥ = a * b
⊢ IsUnit a ∨ IsUnit b
have refine_2 : ∀ (H : ¬IsUnit a ∧ ¬IsUnit b), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
⊢ False
have hπᵥ₁ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬a = 0 ∧ ¬b = 0
Tactic: simp only [hab, ne_eq, mul_eq_zero, not_or] at hπᵥ
Cleared hypotheses: hπᵥ
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬a = 0 ∧ ¬b = 0
⊢ False
have hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
Tactic: have hva := one_le_valuation_factor hne hπᵥ hab H.2
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬a = 0 ∧ ¬b = 0
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
⊢ False
have hπᵥ₁ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(b * a) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬b = 0 ∧ ¬a = 0
Tactic: simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab
Cleared hypotheses: hab, hπᵥ
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
hab : πᵥ = a * b
H : ¬IsUnit a ∧ ¬IsUnit b
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(a * b) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬a = 0 ∧ ¬b = 0
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
hπᵥ₁ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(b * a) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬b = 0 ∧ ¬a = 0
⊢ False
have hab₁ : πᵥ = b * a
Tactic: simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab
Cleared hypotheses: hab, hπᵥ
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
H : ¬IsUnit a ∧ ¬IsUnit b
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(b * a) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬b = 0 ∧ ¬a = 0
hab : πᵥ = b * a
⊢ False
have this : 1 ≤ HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) (↑b : K⟮X⟯) : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
Tactic: have := Right.one_le_mul (one_le_valuation_factor hne hπᵥ hab H.1) hva
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
H : ¬IsUnit a ∧ ¬IsUnit b
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(b * a) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬b = 0 ∧ ¬a = 0
hab : πᵥ = b * a
this : 1 ≤ HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) (↑b : K⟮X⟯) : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
⊢ False
have hπᵥ₁ : HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) b : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) a : K⟮X⟯) : Γ) <
    1 ∧
  ¬b = 0 ∧ ¬a = 0
Tactic: simp only [coePolynomial_eq_algebraMap, map_mul] at hπᵥ this
Cleared hypotheses: hπᵥ
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
⊢ πᵥ ≠ 0
have this : Membership.mem (γ := Set K[X]) {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
  (WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) sorry
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} sorry)
Tactic: have := degree_lt_wf.min_mem _ (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle)
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ)
        ((↑π : K⟮X⟯) ^
          Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
      Γ)
have hne : Set.Nonempty.{u_1} (α := K[X]) {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
Tactic: have hne := setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ)
        ((↑π : K⟮X⟯) ^
          Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
      Γ)
have hπirr : Irreducible π
Tactic: have hπirr : Irreducible π := irreducible_min_polynomial_valuation_lt_one_and_ne_zero hne