awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
H : Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤ HPow.hPow (β := ℕ) p 2
this : ¬Ideal.map (F := R →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
⊢ False
have H₁ : LE.le.{u_3} (α := Ideal T)
  (Ideal.map (R := S) (F := S →+* T) (algebraMap S T)
    (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p)))
  (Ideal.map (F := S →+* T) (algebraMap S T) (HPow.hPow (β := ℕ) p 2))
Tactic: replace H := Ideal.map_mono (f := algebraMap S T) H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
this : ¬Ideal.map (F := R →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  LE.le.{u_3} (α := Ideal T)
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T)
      (Ideal.map (F := R →+* S) (algebraMap R S) (Ideal.comap (F := R →+* S) (algebraMap R S) p)))
    (Ideal.map (F := S →+* T) (algebraMap S T) (HPow.hPow (β := ℕ) p 2))
⊢ False
have H₁ : Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
  HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
Tactic: rw [Ideal.map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_pow] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
p : Ideal S
P : Ideal T
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R P
inst_11 : EssFiniteType R S
inst_12 : EssFiniteType R T
inst_13 : IsDedekindDomain S
hP₁ : P.primeCompl ≤ nonZeroDivisors T
hP₂ : p ≠ ⊥ → P ≠ ⊥
p₀ : Ideal R := Ideal.under R p
this_1 : P.LiesOver p₀
this_2 : Algebra.{u_1, u_2} (Localization.AtPrime p₀) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver p₀ p
this_3 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this_4 : Algebra.{u_1, u_3} (Localization.AtPrime p₀) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p₀ P
hp₀ : p₀ = Ideal.under R P
this_5 : EssFiniteType S T
this_6 : IsNoetherianRing T
h₁ : Algebra.IsSeparable.{u_1, u_3} p₀.ResidueField P.ResidueField
h₂ :
  Eq.{u_3 + 1} (α := Ideal (Localization.AtPrime P))
    (Ideal.map (F := RingHom.{u_1, u_3} R (Localization.AtPrime P)) (algebraMap R (Localization.AtPrime P)) p₀)
    (maximalIdeal (Localization.AtPrime P))
hp : ¬p = ⊥
this : ¬Ideal.map (F := R →+* T) (algebraMap R T) p₀ ≤ HPow.hPow (β := ℕ) P 2
H :
  Ideal.map (F := R →+* T) (algebraMap R T) (Ideal.comap (F := R →+* S) (algebraMap R S) p) ≤
    HPow.hPow (α := Ideal T) (β := ℕ) (Ideal.map (F := S →+* T) (algebraMap S T) p) 2
⊢ False
have neg : Ideal.map (F := S →+* T) (algebraMap S T) p ≤ P
Tactic: refine this (H.trans (Ideal.pow_right_mono ?_ _))
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
⊢ IsUnramifiedAt R p ↔ e(p|R) = 1
have rw : Algebra.IsSeparable.{u_1, u_2} (Ideal.ResidueField (Ideal.under R p)) p.ResidueField
Tactic: rw [isUnramifiedAt_iff_map_eq R (p.under R) p, and_iff_right,
    Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hp Ideal.map_comap_le]
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
⊢ Algebra.IsSeparable.{u_1, u_2} (Ideal.ResidueField (Ideal.under R p)) p.ResidueField
have this₁ : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
Tactic: have : Finite (R ⧸ p.under R) :=
    Ideal.finiteQuotientOfFreeOfNeBot _ (mt Ideal.eq_bot_of_comap_eq_bot hp)
-- Lean 4 proof step from Mathlib.NumberTheory.RamificationInertia.Unramified (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : IsDedekindDomain S
inst_5 : EssFiniteType R S
inst_6 : IsDomain R
inst_7 : Module.Finite ℤ R
inst_8 : CharZero R
inst_9 : Algebra.IsIntegral R S
hp : p ≠ ⊥
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime (Ideal.under R p)) (Localization.AtPrime p) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R p) p
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.under R p))
⊢ Algebra.IsSeparable.{u_1, u_2} (Ideal.ResidueField (Ideal.under R p)) p.ResidueField
have this₁ : Finite.{u_1 + 1} (Ideal.ResidueField (Ideal.under R p))
Tactic: have : Finite ((p.under R).ResidueField) := IsLocalization.finite _
    (nonZeroDivisors (R ⧸ p.under R))
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
⊢ (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
have 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))
Tactic: rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
⊢ 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))
have 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
Tactic: simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
have 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
Tactic: contrapose hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
⊢ 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
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := by contrapose hf; simp [hf]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (goal)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : IsTrivialOn K v
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
⊢ 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
have 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
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]
-- 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⟯ Γ
f : K⟮X⟯
inst_2 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
hf : f ≠ 0
⊢ (v : (a : K⟮X⟯) → Γ) f = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) f.intDegree
have 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
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]
Cleared hypotheses: f, hf
-- 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
⊢ v.IsEquiv (inftyValuation K)
have 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 ℤ))
Tactic: refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_
-- 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 : DecidableEq K⟮X⟯
inst_3 : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ)
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 ℤ))
have 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 ℤ))
Tactic: rcases eq_or_ne f 0 with rfl | hf
Cleared hypotheses: f
-- 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 : 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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rcases eq_or_ne f 0 with rfl | hf
-- 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 : 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.{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 ℤ))
have hlt' : 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]
-- 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 : 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 ℤ))
⊢ 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 ℤ))
have 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
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]
-- 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 : Γ)
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
have 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}
Tactic: obtain ⟨w, h0, h1⟩ := IsNontrivial.exists_lt_one (v := v)
-- Lean 4 proof step from Mathlib.NumberTheory.RatFunc.Ostrowski (hypothesis)
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p q : K[X]
h : q ≠ 0
h0 :
  HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
      ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) ≠
    0
h1 :
  LT.lt.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (HDiv.hDiv (α := K⟮X⟯) (β := K⟮X⟯) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) p : K⟮X⟯)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯)) :
      Γ)
    (1 : Γ)
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
have h0₁ : ¬p = 0 ∧ ¬q = 0
Tactic: simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *
Cleared hypotheses: h0, h1