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 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
grind only
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
⊢ Ne (α := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) (0 : K⟮X⟯)

Tactic:
grind only
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
f :
  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⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
        (intDegree.{u_1} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p)) /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
        (intDegree.{u_1} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q))
⊢ (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⟯) → Γ) 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⟯)).intDegree

Tactic:
rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]

Premises used: RatFunc.intDegree_div, Valuation.map_div, ne_zero_of_lt, zpow_sub₀
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
f :
  HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) q.natDegree
⊢ 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⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
        (intDegree.{u_1} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p)) /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
        (intDegree.{u_1} (K := K) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q))

Tactic:
simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap]

Premises used: zpow_natCast, RatFunc.intDegree_polynomial, 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 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
contrapose :
  ∀ (hf : p = 0),
    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:
contrapose hf
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
p q : K[X]
hq : q ≠ 0
hf : p = 0
⊢ 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

Tactic:
simp [hf]
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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:
have hp : p ≠ 0 := by contrapose hf; simp [hf]
-- 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
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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
hp : p ≠ 0
f :
  HDiv.hDiv (β := Γ) (HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree)
      ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) q.natDegree
f₁ f₂ :
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) q.natDegree =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) q.natDegree
⊢ HDiv.hDiv (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) ((v : (a : K⟮X⟯) → Γ) (↑q : K⟮X⟯) : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) p.natDegree /
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) q.natDegree

Tactic:
rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp,
      valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq]

Premises used: Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
-- 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⟯ Γ
f : K⟮X⟯
inst_2 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
hf : f ≠ 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),
    (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⟯) → Γ) 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⟯)).intDegree
⊢ (v : (a : K⟮X⟯) → Γ) f = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) f.intDegree

Tactic:
induction f using RatFunc.induction_on with
  | f p q hq =>
    rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]
    simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap]
    have hp : p ≠ 0 := by contrapose hf; simp [hf]
    rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp,
      valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq]

Premises used: zpow_natCast, RatFunc.intDegree_div, Valuation.map_div, ne_zero_of_lt, zpow_sub₀, RatFunc.intDegree_polynomial, RatFunc.induction_on, 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
⊢ v.IsEquiv (inftyValuation K)

Tactic:
isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_

Premises used: Iff.mpr, Valuation.isEquiv_iff_val_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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
refine :
  ∀ {f : K⟮X⟯},
    LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ v.IsEquiv (inftyValuation K)

Tactic:
refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_

Premises used: Iff.mpr, Valuation.isEquiv_iff_val_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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
f : K⟮X⟯
inl :
  LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) 0 : Γ) (1 : Γ) ↔
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
inr :
  ∀ (hf : f ≠ 0),
    LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rcases eq_or_ne f 0 with rfl | hf

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) 0 : Γ) (1 : Γ) ↔
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
f : K⟮X⟯
hf : f ≠ 0
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))

Tactic:
simp [← exp_zero]

Premises used: WithZero.exp_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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
f : K⟮X⟯
hf : f ≠ 0
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))

Tactic:
have hlt' : 1 < inftyValuation K X := by simp [← exp_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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
f : K⟮X⟯
hf : f ≠ 0
hlt' :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))
inr :
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) f.intDegree < 1 ↔
    HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            X :
          WithZero (Multiplicative ℤ))
        f.intDegree <
      1
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf,
      valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt' hf]

Premises used: RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X
-- 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
f : K⟮X⟯
hf : f ≠ 0
hlt' :
  LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) X :
      WithZero (Multiplicative ℤ))
⊢ HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) f.intDegree < 1 ↔
    HPow.hPow (α := WithZero (Multiplicative ℤ))
        (((inftyValuation K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            X :
          WithZero (Multiplicative ℤ))
        f.intDegree <
      1

Tactic:
grind [one_le_zpow_iff_right₀]

Premises used: one_le_zpow_iff_right₀
-- 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 : Γ)
obtain :
  ∀ (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}
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}

Tactic:
obtain ⟨w, h0, h1⟩ := IsNontrivial.exists_lt_one (v := v)

Premises used: Valuation.IsNontrivial.exists_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 : Γ)
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 : Γ)
⊢ ¬p = 0 ∧ ¬q = 0

Tactic:
simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *

Premises used: ne_eq, not_or, map_div₀, 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⟯ Γ
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
⊢ 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 *

Premises used: ne_eq, not_or, map_div₀, 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⟯ Γ
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
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 : Γ))
⊢ ¬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]

Premises used: not_and_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 : 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 : Γ))

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 : Γ)
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 : Γ)

Tactic:
have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; 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 : Γ)
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 : Γ)
this :
  ∀ (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}
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬p = 0}

Tactic:
Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)

Premises used: And.right, And.left, Or.elim
-- 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 : Γ)
this :
  ∀ (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}
⊢ 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 Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)

Premises used: And.right, And.left, Or.elim
-- 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 : Γ)
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}
⊢ 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)