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
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
H : ¬IsUnit a ∧ ¬IsUnit b
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
hπᵥ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑(b * a) : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬b = 0 ∧ ¬a = 0
hab : πᵥ = b * a
this : 1 ≤ HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) (↑b : K⟮X⟯) : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) b : K⟮X⟯) : Γ)
        ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) a : K⟮X⟯) : Γ) <
      1 ∧
    ¬b = 0 ∧ ¬a = 0

Tactic:
simp only [coePolynomial_eq_algebraMap, map_mul] at hπᵥ this

Premises used: map_mul, 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
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
πᵥ : K[X] :=
  WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} hne
a b : K[X]
H : ¬IsUnit a ∧ ¬IsUnit b
hva : LE.le.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) (↑a : K⟮X⟯) : Γ)
hab : πᵥ = b * a
this :
  1 ≤
    HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) b : K⟮X⟯) : Γ)
      ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) a : K⟮X⟯) : Γ)
hπᵥ :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) b : K⟮X⟯) : Γ)
        ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) a : K⟮X⟯) : Γ) <
      1 ∧
    ¬b = 0 ∧ ¬a = 0
⊢ False

Tactic:
grind
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
⊢ Membership.mem (γ := Set K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
    (WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
      {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} ⋯)

Tactic:
have := degree_lt_wf.min_mem _ (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty 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 : Γ)
this :
  Membership.mem (γ := Set K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
    (WellFounded.min (r := fun (p q : K[X]) ↦ p.degree < q.degree) ⋯
      {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0} ⋯)
⊢ πᵥ ≠ 0

Tactic:
simp_all [uniformizingPolynomial]

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

Tactic:
simpa using (degree_lt_wf.min_mem _
    (setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty hle)).1

Premises used: WellFounded.min_mem, Polynomial.degree_lt_wf, And.left, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty
-- 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 : Γ)
⊢ Ne (α := Ideal K[X]) (K[X] ∙ πᵥ) ⊥

Tactic:
simpa using uniformizingPolynomial_ne_zero hle

Premises used: RatFunc.uniformizingPolynomial_ne_zero
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
set :
  let π := πᵥ;
  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})))) :
      Γ)
⊢ 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:
set π := πᵥ
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
⊢ Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}

Tactic:
have hne := setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty 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 : Γ)
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}
⊢ Irreducible π

Tactic:
have hπirr : Irreducible π := irreducible_min_polynomial_valuation_lt_one_and_ne_zero hne
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
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})))) :
        Γ)
⊢ 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

Premises used: WfDvdMonoid.max_power_factor
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
⊢ 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
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
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} π
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0

Tactic:
simp only [ne_eq, mem_setOf] at hπ

Premises used: ne_eq, Set.mem_setOf
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
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})))) :
      Γ)
⊢ 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:
nth_rw 1 [heq]
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
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}))))
⊢ 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:
simp only [map_mul, map_pow]

Premises used: map_pow, map_mul
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
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 : Γ)
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}))))
⊢ 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 [this, mul_one]

Premises used: mul_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 : 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 : Γ)
e_a : k = Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))
⊢ 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:
congr
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
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 : Γ)
⊢ k = Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))

Tactic:
(Ideal.count_associates_eq (irreducible_iff_prime.mp hπirr) hnq heq).symm

Premises used: Set.Mem, setOf, Ideal.count_associates_eq, Submodule.span, Iff.mp, irreducible_iff_prime, Eq.symm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
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 : Γ)
⊢ k = Associates.count (Associates.mk Pᵥ.asIdeal) (Associates.factors (Associates.mk (Ideal.span {p})))

Tactic:
exact (Ideal.count_associates_eq (irreducible_iff_prime.mp hπirr) hnq heq).symm

Premises used: Ideal.count_associates_eq, Iff.mp, irreducible_iff_prime, Eq.symm
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
suffices :
  Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) (1 : Γ)
⊢ 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:
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
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
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 : Γ)
⊢ Eq.{u_2 + 1} (α := Γ) ((v : (a : K⟮X⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) q : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
rw [← mod_add_div q π, map_add]

Premises used: map_add, EuclideanDomain.mod_add_div
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
⊢ ¬q % π = 0

Tactic:
rw [← mod_eq_zero] at hnq

Premises used: EuclideanDomain.mod_eq_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 : Γ)
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
hnq₁ : ¬q % π = 0
⊢ p = π ^ k * q

Tactic:
rw [← mod_eq_zero] at hnq

Premises used: EuclideanDomain.mod_eq_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 : Γ)
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
hnq₁ : ¬q % π = 0
heq₁ : p = π ^ k * q
⊢ LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0

Tactic:
rw [← mod_eq_zero] at hnq

Premises used: EuclideanDomain.mod_eq_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 : Γ)
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⟯) → Γ) ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) (q % π) : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
obtain ⟨h₁, h₂⟩ := this
-- Module: Mathlib.NumberTheory.RatFunc.Ostrowski
Goal:
K : Type u_1
Γ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
inst_2 : v.IsNontrivial
inst_3 : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) X : Γ) (1 : Γ)
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne :
  Set.Nonempty.{u_1} (α := K[X])
    {p : K[X] | LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ) ∧ p ≠ 0}
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : LT.lt.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑π : K⟮X⟯) : Γ) (1 : Γ) ∧ ¬π = 0
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 : Γ)
⊢ 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