awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
⊢ ∀ (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:
fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr
      ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩

Premises used: Iff.mpr, lt_iff_le_and_ne, Polynomial.valuation_le_one_of_valuation_X_le_one, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
⊢ ∀ (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:
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⟩
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : Γ)
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}
⊢ 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⟩

Premises used: ne_eq, not_or, map_div₀, RatFunc.induction_on, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
hπᵥ :
  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
hb : ¬IsUnit b
⊢ let πᵥ :=
    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

Tactic:
set πᵥ := degree_lt_wf.min _ hne

Premises used: Polynomial.degree_lt_wf, WellFounded.min
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ 0 < b.degree

Tactic:
have hbpos := degree_pos_of_ne_zero_of_nonunit hab.2.2 hb
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
simp_rw :
  ∀ (hbpos : LT.lt (α := WithBot ℕ) 0 (↑b.natDegree : WithBot ℕ)),
    (↑a.natDegree : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑a.natDegree : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
⊢ a.degree < πᵥ.degree

Tactic:
simp_rw [hπᵥ, degree_mul, degree_eq_natDegree hab.2.1, degree_eq_natDegree hab.2.2] at hbpos ⊢

Premises used: Polynomial.degree_eq_natDegree, And.right, And.left, Polynomial.degree_mul
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 ℕ)
norm_cast : a.natDegree < a.natDegree + b.natDegree
⊢ (↑a.natDegree : WithBot ℕ) < HAdd.hAdd (α := WithBot ℕ) (↑a.natDegree : WithBot ℕ) (↑b.natDegree : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 < a.natDegree + b.natDegree

Tactic:
simpa using hbpos
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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

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
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ 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
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
hlea : a ∉ {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
⊢ LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)

Tactic:
grind
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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}
set :
  let πᵥ :=
    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 πᵥ
⊢ Irreducible
    (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)

Tactic:
set πᵥ := degree_lt_wf.min _ hne

Premises used: Polynomial.degree_lt_wf, WellFounded.min
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ) ∧ πᵥ ≠ 0

Tactic:
have hπᵥ : v πᵥ < 1 ∧ πᵥ ≠ 0 := degree_lt_wf.min_mem _ hne
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 πᵥ

Tactic:
irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩

Premises used: Iff.mpr, And.intro, irreducible_iff
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 πᵥ
refine_2 : ∀ (a b : K[X]) (hab : πᵥ = a * b), IsUnit a ∨ IsUnit b
⊢ Irreducible πᵥ

Tactic:
refine irreducible_iff.mpr ⟨?_, fun a b hab ↦ ?_⟩

Premises used: Iff.mpr, And.intro, irreducible_iff
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : ¬∃ (r : K), r ≠ 0 ∧ (Polynomial.C : (a : K) → K[X]) r = πᵥ
⊢ ¬IsUnit πᵥ

Tactic:
simp only [Polynomial.isUnit_iff, isUnit_iff_ne_zero]

Premises used: Polynomial.isUnit_iff, isUnit_iff_ne_zero
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 = πᵥ
⊢ 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πᵥ

Premises used: RatFunc.coePolynomial, RatFunc.algebraMap_eq_C, RatFunc.algebraMap_C
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 = πᵥ
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])
⊢ a ≠ 0

Tactic:
rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ

Premises used: RatFunc.coePolynomial, RatFunc.algebraMap_eq_C, RatFunc.algebraMap_C
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 = πᵥ
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])
ha0₁ : a ≠ 0
⊢ (Polynomial.C : (a : K) → K[X]) a = πᵥ

Tactic:
rw [← ha, coePolynomial, algebraMap_C, ← algebraMap_eq_C] at hπᵥ

Premises used: RatFunc.coePolynomial, RatFunc.algebraMap_eq_C, RatFunc.algebraMap_C
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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 : K
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])
ha0 : a ≠ 0
ha : (Polynomial.C : (a : K) → K[X]) a = πᵥ
⊢ False

Tactic:
grind
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
refine_2 : ∀ (H : ¬IsUnit a ∧ ¬IsUnit b), False
⊢ IsUnit a ∨ IsUnit b

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ 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πᵥ

Premises used: mul_eq_zero, ne_eq, not_or
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)

Tactic:
have hva := one_le_valuation_factor hne hπᵥ hab H.2
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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⟯) : Γ)
⊢ 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

Premises used: and_comm, mul_comm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ πᵥ = b * a

Tactic:
simp only [mul_comm a b, @and_comm (¬a = 0)] at hπᵥ hab

Premises used: and_comm, mul_comm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
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
⊢ 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