awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 π
⊢ 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 obtain : ∀ (k : ℕ) (q : K[X]) (hnq : ¬π ∣ q) (heq : p = π ^ k * q),
  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})))) :
      Γ)
Tactic: obtain ⟨k, q, hnq, heq⟩ := WfDvdMonoid.max_power_factor hp hπirr
-- 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
⊢ 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π : Membership.mem (γ := Set K[X]) {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
  π
Tactic: have hπ : π ∈ _ := degree_lt_wf.min_mem _ hne
-- 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ :
  Membership.mem (γ := Set 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π₁ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
Tactic: simp only [ne_eq, mem_setOf] at hπ
Cleared hypotheses: hπ
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 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 nth_rw : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π ^ k * q) : K⟮X⟯) : Γ)
  ((v : (a : K⟮X⟯) → Γ)
      ((↑π : K⟮X⟯) ^
        Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
    Γ)
Tactic: nth_rw 1 [heq]
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π ^ k * q) : K⟮X⟯) : Γ)
    ((v : (a : K⟮X⟯) → Γ)
        ((↑π : K⟮X⟯) ^
          Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
      Γ)
have simp : HMul.hMul (β := Γ)
    (HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) π : K⟮X⟯) : Γ) k)
    ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) =
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ)
    (Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p}))))
Tactic: simp only [map_mul, map_pow]
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
this : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) (1 : Γ)
⊢ HMul.hMul (β := Γ)
      (HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) π : K⟮X⟯) : Γ) k)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ)
      (Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p}))))
have simp : HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) π : K⟮X⟯) : Γ) k =
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ)
    (Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p}))))
Tactic: simp only [this, mul_one]
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
this : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) (1 : Γ)
⊢ HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) π : K⟮X⟯) : Γ) k =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ)
      (Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p}))))
have e_a : k = Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))
Tactic: congr
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ HMul.hMul (β := Γ)
      (HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) π : K⟮X⟯) : Γ) k)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ)
      (Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p}))))
have suffices : Eq.{u_2 + 1} (α := Γ) ((v : (a : 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 by
    simp only [this, mul_one]
    congr
    exact (Ideal.count_associates_eq (irreducible_iff_prime.mp hπirr) hnq heq).symm
-- 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 : 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
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) (1 : Γ)
have rw : 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 [← mod_add_div q π, map_add]
-- 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}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ 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 : Γ)
have hnq₁ : ¬q % π = 0
Tactic: rw [← mod_eq_zero] at hnq
Cleared hypotheses: hnq, heq, 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 : Γ)
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
this :
  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 : Γ)
have h₁ : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
Tactic: obtain ⟨h₁, h₂⟩ := this
Cleared hypotheses: this
-- 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}
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
this :
  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 : Γ)
h₁ :
  Eq.{u_2 + 1} (α := Γ) ((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 : Γ)
have h₂ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
  (1 : Γ)
Tactic: obtain ⟨h₁, h₂⟩ := this
Cleared hypotheses: this
-- 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 : 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 : Γ)
⊢ 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 : Γ)
have 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⟯) : Γ)
Tactic: rw [← h₁] at h₂ ⊢
Cleared hypotheses: h₂
-- 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 : 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
⊢ 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 : Γ)
have 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 : Γ)
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₂
-- 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 : 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
⊢ 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 : Γ)
have left : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
Tactic: constructor
-- 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 : 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 : Γ)
⊢ 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 : Γ)
have right : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (π * (q / π)) : K⟮X⟯) : Γ)
  (1 : Γ)
Tactic: constructor
-- 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 : 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
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)
have left : Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)
Tactic: rw [← coePolynomial_eq_algebraMap]
-- 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}
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
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)
have hnπ : 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)
-- 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}
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}
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(q % π) : K⟮X⟯) : Γ) (1 : Γ)
have this : 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 % π)
-- 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 : Γ)
f : K⟮X⟯
hf : f ≠ 0
⊢ ∃ (z : ℤ), (v : (a : K⟮X⟯) → Γ) f = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) z
have h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
Tactic: have h0 : v πᵥ ≠ 0 := by simpa using uniformizingPolynomial_ne_zero hle