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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
h₁ :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
h₂ :
  LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
    (1 : Γ)
rw :
  ∀
    (h₂ :
      LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
        ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)),
    Eq.{u_2 + 1} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          (HAdd.hAdd (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯)) :
        Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)
⊢ Eq.{u_2 + 1} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (HAdd.hAdd (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯)) :
      Γ)
    (1 : Γ)

Tactic:
rw [← h₁] at 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
h₁ :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
h₂ :
  LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)
⊢ Eq.{u_2 + 1} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (HAdd.hAdd (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯)) :
      Γ)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)

Tactic:
Valuation.map_add_eq_of_lt_left _ h₂

Premises used: Valuation.map_add_eq_of_lt_left
-- 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
h₁ :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
h₂ :
  LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)
⊢ Eq.{u_2 + 1} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (HAdd.hAdd (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯)) :
      Γ)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ)

Tactic:
exact Valuation.map_add_eq_of_lt_left _ h₂

Premises used: Valuation.map_add_eq_of_lt_left
-- 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
suffices :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ) ∧
    LT.lt.{u_2} (α := Γ) ((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⟯) → Γ)
        (HAdd.hAdd (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯)) :
      Γ)
    (1 : Γ)

Tactic:
suffices v (algebraMap K[X] (RatFunc K) (q % π)) = 1 ∧
      v (algebraMap K[X] (RatFunc K) (π * (q / π))) < 1 by
    obtain ⟨h₁, h₂⟩ := this
    rw [← h₁] at h₂ ⊢
    exact Valuation.map_add_eq_of_lt_left _ 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
left :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
right :
  LT.lt.{u_2} (α := Γ) ((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⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ) ∧
    LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
      (1 : Γ)

Tactic:
constructor
-- 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
left : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
rw [← coePolynomial_eq_algebraMap]

Premises used: RatFunc.coePolynomial_eq_algebraMap
-- 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ q % π ∉ {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}

Tactic:
have hnπ : q % π ∉ {p : K[X] | v ↑p < 1 ∧ p ≠ 0} :=
      imp_not_comm.mp (degree_lt_wf.not_lt_min _) (EuclideanDomain.remainder_lt q 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
hnπ : q % π ∉ {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
have := Polynomial.valuation_le_one_of_valuation_X_le_one _ hle (q % π)
-- 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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
hnπ : q % π ∉ {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
this : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)

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 : 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
    (1 : Γ)

Tactic:
simpa only [map_mul, ← coePolynomial_eq_algebraMap]
      using mul_lt_one_of_lt_of_le hπ.1 <| (q / π).valuation_le_one_of_valuation_X_le_one _ hle

Premises used: mul_lt_one_of_lt_of_le, HDiv.hDiv, Polynomial.valuation_le_one_of_valuation_X_le_one, map_mul, And.left, RatFunc.coePolynomial_eq_algebraMap
-- 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 : Γ)
f : K⟮X⟯
hf : f ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)

Tactic:
simpa using uniformizingPolynomial_ne_zero hle

Premises used: RatFunc.uniformizingPolynomial_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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
f : K⟮X⟯
hf : f ≠ 0
⊢ Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)

Tactic:
have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle
-- 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 : Γ)
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
p q : K[X]
hq : q ≠ 0
hf :
  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
h :
  (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⟯)) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ)
      (HSub.hSub (α := ℤ)
        (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) : ℤ)
        (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ))
⊢ ∃ (z : ℤ),
    (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⟯)) =
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) z

Tactic:
use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors -
      (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors
-- 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 : Γ)
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
p q : K[X]
hq : q ≠ 0
hf :
  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
⊢ p ≠ 0

Tactic:
aesop
-- 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 : Γ)
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
p q : K[X]
hq : q ≠ 0
hf :
  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
⊢ (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⟯)) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ)
      (HSub.hSub (α := ℤ)
        (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) : ℤ)
        (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ))

Tactic:
simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle
        (p := p) (by aesop)]

Premises used: zpow_natCast, zpow_sub₀, map_pow, map_div₀, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one
-- 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 : Γ)
f : K⟮X⟯
hf : f ≠ 0
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
f₁ :
  ∀ (p q : K[X]) (hq : q ≠ 0)
    (hf :
      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),
    ∃ (z : ℤ),
      (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⟯)) =
        HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) z
⊢ ∃ (z : ℤ), (v : (a : K⟮X⟯) → Γ) f = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) z

Tactic:
induction f using RatFunc.induction_on with
  | f p q hq =>
    use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors -
      (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors
    simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle
        (p := p) (by aesop)]

Premises used: zpow_natCast, zpow_sub₀, map_pow, map_div₀, RatFunc.induction_on
-- 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 : Γ)
hv : v.IsRankOneDiscrete
⊢ Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)

Tactic:
simpa using uniformizingPolynomial_ne_zero hle

Premises used: RatFunc.uniformizingPolynomial_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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
hv : v.IsRankOneDiscrete
⊢ Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)

Tactic:
have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
rw : ⋯.unit = LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.valueGroup v)
⊢ v.IsUniformizer (↑πᵥ : K⟮X⟯)

Tactic:
rw [IsUniformizer, ← hv.valueGroup_genLTOne_eq_generator, ← h0.isUnit.unit_spec, Units.val_inj]

Premises used: Valuation.IsUniformizer, Ne.isUnit, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, Units.val_inj, IsUnit.unit_spec
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
hg : ⋯.unit < 1
hH : Subgroup.zpowers ⋯.unit = MonoidWithZeroHom.valueGroup v
⊢ ⋯.unit = LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.valueGroup v)

Tactic:
apply LinearOrderedCommGroup.Subgroup.genLTOne_unique

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_unique
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
hg : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ)
⊢ ⋯.unit < 1

Tactic:
rw [← Units.val_lt_val, h0.isUnit.unit_spec, Units.val_one]

Premises used: Ne.isUnit, Units.val_one, Units.val_lt_val, IsUnit.unit_spec
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
valuation_uniformizingPolynomial_lt_one hle

Premises used: RatFunc.valuation_uniformizingPolynomial_lt_one
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
exact valuation_uniformizingPolynomial_lt_one hle

Premises used: RatFunc.valuation_uniformizingPolynomial_lt_one
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
hH :
  ∀ (γ : Γˣ),
    Membership.mem (γ := Subgroup Γˣ) (Subgroup.zpowers ⋯.unit) γ ↔
      Membership.mem (γ := Subgroup Γˣ) (MonoidWithZeroHom.valueGroup v) γ
⊢ Subgroup.zpowers ⋯.unit = MonoidWithZeroHom.valueGroup v

Tactic:
ext γ
-- 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
γ : Γˣ
hH :
  (∃ (k : ℤ),
      IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ) ↔
    ∃ (a : K⟮X⟯),
      ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
⊢ Membership.mem (γ := Subgroup Γˣ) (Subgroup.zpowers ⋯.unit) γ ↔
    Membership.mem (γ := Subgroup Γˣ) (MonoidWithZeroHom.valueGroup v) γ

Tactic:
simp only [coePolynomial_eq_algebraMap, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq,
      map_eq_zero, Subgroup.mem_zpowers_iff]

Premises used: map_eq_zero, ne_eq, RatFunc.coePolynomial_eq_algebraMap, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, Subgroup.mem_zpowers_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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
γ : Γˣ
⊢ (∃ (k : ℤ),
      IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ) ↔
    ∃ (a : K⟮X⟯),
      ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x

Tactic:
⟨fun ⟨k, hk⟩ ↦ ?_, fun ⟨a, ha, b, hab⟩ ↦ ?_⟩

Premises used: Units.val, RatFunc.uniformizingPolynomial, HMul.hMul, Algebra.algebraMap, Ne.isUnit, Exists, _private.0.RatFunc.uniformizingPolynomial_isUniformizer.match_3, id, Polynomial, And, RatFunc, HPow.hPow, Iff.intro, Eq.ndrec, IsUnit.unit, Eq.refl, OfNat.ofNat, Eq, DFunLike.coe, Not, _private.0.RatFunc.uniformizingPolynomial_isUniformizer.match_4