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 : Γ)
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 = γ) →
    ∀ (k : ℤ)
      (hk : 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
hH₁ :
  (∃ (a : K⟮X⟯),
      ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x) →
    ∀ (a : K⟮X⟯) (ha : ¬a = 0) (b : K⟮X⟯)
      (hab : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) b),
      ∃ (k : ℤ),
        IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
⊢ (∃ (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:
refine ⟨fun ⟨k, hk⟩ ↦ ?_, fun ⟨a, ha, b, hab⟩ ↦ ?_⟩
-- 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 : Γ)
γ : Γˣ
h_1 :
  ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
k : ℤ
hk : IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
h : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) 1 : Γ) (↑γ : Γ) = (v : (a : 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:
use 1, one_ne_zero, πᵥ ^ k

Premises used: one_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
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
γ : Γˣ
h : ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
k : ℤ
hk : IsUnit.unit (a := (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⟯) : Γ) k = (↑γ : Γ)

Tactic:
simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val, h0.isUnit.unit_spec] at hk

Premises used: Ne.isUnit, Units.val_zpow_eq_zpow_val, 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 : Γ)
γ : Γˣ
h : ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
k : ℤ
hk : HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) k = (↑γ : Γ)
⊢ HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) 1 : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) ((↑πᵥ : K⟮X⟯) ^ k)

Tactic:
simp [← hk]
-- 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 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) b
hH :
  ∀ (ka : ℤ) (hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka),
    ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
⊢ ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ

Tactic:
obtain ⟨ka, hka⟩ := exists_zpow_uniformizingPolynomial hle ha

Premises used: RatFunc.exists_zpow_uniformizingPolynomial
-- 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 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) b
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
⊢ b ≠ 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 : Γ)
hv : v.IsRankOneDiscrete
h0 : Ne.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) (0 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) b
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
hH :
  ∀ (kb : ℤ) (hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb),
    ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
⊢ ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ

Tactic:
obtain ⟨kb, hkb⟩ := exists_zpow_uniformizingPolynomial hle (f := b) (by aesop)

Premises used: RatFunc.exists_zpow_uniformizingPolynomial
-- 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 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) b
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
kb : ℤ
hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
hH :
  ∀ (hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka) (kb : ℤ)
    (hab :
      HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka * (↑γ : Γ) =
        HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb)
    (hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb),
    ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ
⊢ ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ

Tactic:
rw [hka, hkb] at hab
-- 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 : Γ)
γ : Γˣ
h_1 :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
kb : ℤ
hab :
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka * (↑γ : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
h : IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ (kb - ka) = γ
⊢ ∃ (k : ℤ), IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ k = γ

Tactic:
use kb - ka
-- 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 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
kb : ℤ
hab :
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka * (↑γ : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
⊢ HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka ≠ 0

Tactic:
have : v ↑πᵥ ^ ka ≠ 0 := zpow_ne_zero _ h0
-- 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 : Γ)
γ : Γˣ
h :
  ∃ (a : K⟮X⟯), ¬a = 0 ∧ ∃ (x : K⟮X⟯), HMul.hMul (α := Γ) ((v : (a : K⟮X⟯) → Γ) a : Γ) (↑γ : Γ) = (v : (a : K⟮X⟯) → Γ) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : (v : (a : K⟮X⟯) → Γ) a = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka
kb : ℤ
hab :
  HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka * (↑γ : Γ) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
hkb : (v : (a : K⟮X⟯) → Γ) b = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) kb
this : HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑πᵥ : K⟮X⟯) : Γ) ka ≠ 0
⊢ IsUnit.unit (a := (v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) πᵥ : K⟮X⟯)) ⋯ ^ (kb - ka) = γ

Tactic:
simp only [zpow_sub, ← Units.val_inj, Units.val_mul, Units.val_zpow_eq_zpow_val,
        h0.isUnit.unit_spec, Units.val_inv_eq_inv_val, ← hab, field]

Premises used: Ne.isUnit, Units.val_inv_eq_inv_val, Units.val_zpow_eq_zpow_val, Units.val_inj, IsUnit.unit_spec, Units.val_mul, 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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
rw :
  ∀ {x : K⟮X⟯},
    LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) x : Γ) (1 : Γ) ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            x :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ v.IsEquiv (valuation K⟮X⟯ Pᵥ)

Tactic:
rw [isEquiv_iff_val_le_one]

Premises used: Valuation.isEquiv_iff_val_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 : Γ)
inst_4 : v.IsRankOneDiscrete
f : K⟮X⟯
inl :
  LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) 0 : Γ) (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          0 :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
inr :
  ∀ (hf0 : f ≠ 0),
    LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) f : Γ) (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : 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 | hf0

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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) 0 : Γ) (1 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : 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 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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:
simp_all
-- 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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 hp0 : p ≠ 0 := by simp_all
-- 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
⊢ let pi := πᵥ;
  pi = πᵥ

Tactic:
set pi := πᵥ with hpi_def

Premises used: Set.pi
-- 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
⊢ v.IsUniformizer (↑pi : K⟮X⟯)

Tactic:
have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
inr :
  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 ↔
    HMul.hMul (α := WithZero (Multiplicative ℤ))
        (exp
            (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
              ℤ))⁻¹
        (exp
          (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
      1
⊢ LE.le.{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 : Γ) ↔
    LE.le (α := WithZero (Multiplicative ℤ))
      (((valuation K⟮X⟯ Pᵥ : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
          (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⟯)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0,
        if_neg hq0, div_inv_eq_mul]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, map_div₀, IsDedekindDomain.HeightOneSpectrum.intValuation_def, div_inv_eq_mul, if_neg, WithZero.exp_neg
-- 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
inr :
  HDiv.hDiv (α := Γ) (β := Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((↑πᵥ : K⟮X⟯) ^
              Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
          Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((↑πᵥ : K⟮X⟯) ^
              Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) :
          Γ) ≤
      1 ↔
    HMul.hMul (α := WithZero (Multiplicative ℤ))
        (exp
            (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
              ℤ))⁻¹
        (exp
          (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
      1
⊢ 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 ↔
    HMul.hMul (α := WithZero (Multiplicative ℤ))
        (exp
            (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
              ℤ))⁻¹
        (exp
          (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
      1

Tactic:
rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]

Premises used: 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
⊢ 0 < (↑(IsRankOneDiscrete.generator v) : Γ)

Tactic:
simp_all
-- 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 : Γ)
inst_4 : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 :
  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
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer (↑pi : K⟮X⟯)
⊢ HDiv.hDiv (α := Γ) (β := Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((↑πᵥ : K⟮X⟯) ^
              Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
          Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((↑πᵥ : K⟮X⟯) ^
              Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) :
          Γ) ≤
      1 ↔
    HMul.hMul (α := WithZero (Multiplicative ℤ))
        (exp
            (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))) :
              ℤ))⁻¹
        (exp
          (↑(Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {q})))) : ℤ)) ≤
      1

Tactic:
simp_all [div_le_one₀, inv_mul_le_one₀,
        (pow_le_pow_iff_right_of_lt_one₀ (by simp_all) (IsRankOneDiscrete.generator_lt_one v))]

Premises used: Valuation.IsRankOneDiscrete.generator_lt_one, pow_le_pow_iff_right_of_lt_one₀, inv_mul_le_one₀, div_le_one₀