awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
f : L
h : Transcendental K f
g : K[X]
⊢ Eq.{u_1 + 1} (α := K⟮X⟯)
    (((algEquivOfTranscendental f h).symm : (a : ↥K⟮f⟯) → K⟮X⟯)
        ((aeval (AdjoinSimple.gen K f) : (a : K[X]) → ↥K⟮f⟯) g) :
      K⟮X⟯)
    ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) g : K⟮X⟯)

Tactic:
simp [algEquivOfTranscendental, ← algebraMap_eq_gen_self, aeval_algebraMap_apply]

Premises used: IntermediateField.algebraAdjoinAdjoin.algebraMap_eq_gen_self, Polynomial.aeval_algebraMap_apply, RatFunc.algEquivOfTranscendental
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
rw : Transcendental K (A := Polynomial K) Polynomial.X
⊢ Transcendental K (A := K⟮X⟯) X

Tactic:
rw [← RatFunc.algebraMap_X, transcendental_algebraMap_iff (algebraMap_injective K)]

Premises used: RatFunc.algebraMap_X, RatFunc.algebraMap_injective, transcendental_algebraMap_iff
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Transcendental K (A := Polynomial K) Polynomial.X

Tactic:
Polynomial.transcendental_X K

Premises used: Polynomial.transcendental_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Transcendental K (A := Polynomial K) Polynomial.X

Tactic:
exact Polynomial.transcendental_X K

Premises used: Polynomial.transcendental_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
⊢ Algebra.Transcendental K K⟮X⟯

Tactic:
⟨X, transcendental_X⟩

Premises used: RatFunc.transcendental_X, RatFunc.X, Algebra.Transcendental.mk, Exists.intro
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
rw : Prime.{u_1} (M := K[X]) X
rw₁ : Ne.{u_1 + 1} (α := K[X]) X 0
⊢ Ideal.IsPrime (α := K[X]) (Ideal.span {X})

Tactic:
rw [Ideal.span_singleton_prime]

Premises used: Ideal.span_singleton_prime
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ Prime.{u_1} (M := K[X]) X

Tactic:
Polynomial.prime_X

Premises used: Polynomial.prime_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ Ne.{u_1 + 1} (α := K[X]) X 0

Tactic:
Polynomial.X_ne_zero

Premises used: Polynomial.X_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ Prime.{u_1} (M := K[X]) X

Tactic:
exacts [Polynomial.prime_X, Polynomial.X_ne_zero]

Premises used: Polynomial.X_ne_zero, Polynomial.prime_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
rw : ¬Eq.{u_1 + 1} (α := K[X]) X 0
⊢ Ne (α := Ideal K[X]) (Ideal.span {X}) ⊥

Tactic:
rw [ne_eq, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, ne_eq
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ ¬Eq.{u_1 + 1} (α := K[X]) X 0

Tactic:
Polynomial.X_ne_zero

Premises used: Polynomial.X_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K_1 : Type u
K : Type u_1
inst : Field K
⊢ ¬Eq.{u_1 + 1} (α := K[X]) X 0

Tactic:
exact Polynomial.X_ne_zero

Premises used: Polynomial.X_ne_zero
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := Ideal K[X]) (asIdeal (idealX K)) (Ideal.span {X})

Tactic:
rfl

Premises used: Set.Mem, setOf, Submodule.span, rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₂ rw₃ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-1)) (exp (-1))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton
      _ (Polynomial.X_ne_zero) (idealX_span K)]

Premises used: Polynomial.idealX_span, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, RatFunc.algebraMap_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
f g : K[X]
hg : g ≠ 0
⊢ ((valuation (R := K[X]) K⟮X⟯ (idealX K) : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
        (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      (RatFunc.mk f g) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((intValuation (idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (((intValuation (idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          g :
        WithZero (Multiplicative ℤ))

Tactic:
simp only [RatFunc.mk_eq_mk' _ hg, valuation_of_mk']

Premises used: RatFunc.mk_eq_mk', IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
n : ℕ
a : K
ha : a ≠ 0
⊢ (v : (a : K⟮X⟯) → Γ) (↑((monomial n : (a : K) → K[X]) a) : K⟮X⟯) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) n

Tactic:
simp_all [← RatFunc.algebraMap_eq_C, hv.eq_one]

Premises used: Valuation.IsTrivialOn.eq_one, RatFunc.algebraMap_eq_C
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p : K[X]
hp : p ≠ 0
⊢ (v : (a : K⟮X⟯) → Γ) ((aeval RatFunc.X : (a : K[X]) → K⟮X⟯) p : K⟮X⟯) =
    HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) p.natDegree

Tactic:
valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X .X hlt hp

Premises used: Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p : K[X]
hp : p ≠ 0
h : Eq.{u_1 + 1} (α := (P : K[X]) → K⟮X⟯) coePolynomial (⇑(aeval RatFunc.X) : (a : K[X]) → K⟮X⟯)
⊢ (v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) = HPow.hPow (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) p.natDegree

Tactic:
convert! valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X .X hlt hp

Premises used: Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p : K[X]
hp : p ≠ 0
h : ∀ (p : K[X]), (↑p : K⟮X⟯) = (aeval RatFunc.X : (a : K[X]) → K⟮X⟯) p
⊢ Eq.{u_1 + 1} (α := (P : K[X]) → K⟮X⟯) coePolynomial (⇑(aeval RatFunc.X) : (a : K[X]) → K⟮X⟯)

Tactic:
ext p
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p_1 : K[X]
hp : p_1 ≠ 0
p : K[X]
h :
  Eq.{u_1 + 1} (α := K⟮X⟯) (↑((aeval X : (a : K[X]) → K[X]) p) : K⟮X⟯)
    (((aeval ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) : K[X] →ₐ[K] K⟮X⟯) : (a : K[X]) → K⟮X⟯) p)
⊢ (↑p : K⟮X⟯) = (aeval RatFunc.X : (a : K[X]) → K⟮X⟯) p

Tactic:
nth_rw 1 [RatFunc.X, ← aeval_X_left_apply p (R := K)]

Premises used: RatFunc.X, Polynomial.aeval_X_left_apply
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p_1 : K[X]
hp : p_1 ≠ 0
p : K[X]
⊢ Eq.{u_1 + 1} (α := K⟮X⟯) (↑((aeval X : (a : K[X]) → K[X]) p) : K⟮X⟯)
    (((aeval ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) : K[X] →ₐ[K] K⟮X⟯) : (a : K[X]) → K⟮X⟯) p)

Tactic:
(aeval_algebraMap_apply K⟮X⟯ X p).symm

Premises used: RatFunc.coePolynomial, RatFunc, Eq.symm, Polynomial.X, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : LT.lt.{u_2} (α := Γ) (1 : Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ)
p_1 : K[X]
hp : p_1 ≠ 0
p : K[X]
⊢ Eq.{u_1 + 1} (α := K⟮X⟯) (↑((aeval X : (a : K[X]) → K[X]) p) : K⟮X⟯)
    (((aeval ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) X) : K[X] →ₐ[K] K⟮X⟯) : (a : K[X]) → K⟮X⟯) p)

Tactic:
exact (aeval_algebraMap_apply K⟮X⟯ X p).symm

Premises used: RatFunc, Eq.symm, Polynomial.X, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
rw :
  LE.le.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (∑ x ∈ Finset.range (p.natDegree + 1),
          (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial x : (a : K) → K[X]) (p.coeff x))) :
      Γ)
    (1 : Γ)
⊢ LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑p : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
rw [as_sum_range p, RatFunc.coePolynomial, map_sum]

Premises used: RatFunc.coePolynomial, Polynomial.as_sum_range, map_sum
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
apply :
  ∀ i ∈ Finset.range (p.natDegree + 1),
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)
⊢ LE.le.{u_2} (α := Γ)
    ((v : (a : K⟮X⟯) → Γ)
        (∑ x ∈ Finset.range (p.natDegree + 1),
          (algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial x : (a : K) → K[X]) (p.coeff x))) :
      Γ)
    (1 : Γ)

Tactic:
apply map_sum_le v

Premises used: Valuation.map_sum_le
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
pos :
  ∀ (h0 : p.coeff i = 0),
    i ∈ Finset.range (p.natDegree + 1) →
      LE.le.{u_2} (α := Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
          Γ)
        (1 : Γ)
neg :
  ∀ (h0 : ¬p.coeff i = 0),
    i ∈ Finset.range (p.natDegree + 1) →
      LE.le.{u_2} (α := Γ)
        ((v : (a : K⟮X⟯) → Γ)
            ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
          Γ)
        (1 : Γ)
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)

Tactic:
by_cases h0 : p.coeff i = 0

Premises used: Polynomial.coeff
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
h0 : p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)

Tactic:
simp_all
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
neg :
  i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) : Γ) (1 : Γ)
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ)
      ((v : (a : K⟮X⟯) → Γ)
          ((algebraMap K[X] K⟮X⟯ : (a : K[X]) → K⟮X⟯) ((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) :
        Γ)
      (1 : Γ)

Tactic:
rw [← RatFunc.coePolynomial]

Premises used: RatFunc.coePolynomial
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (1 : Γ)
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) →
    LE.le.{u_2} (α := Γ) ((v : (a : K⟮X⟯) → Γ) (↑((monomial i : (a : K) → K[X]) (p.coeff i)) : K⟮X⟯) : Γ) (1 : Γ)

Tactic:
simp_all [pow_le_one', ← RatFunc.algebraMap_eq_C, hv.eq_one _ h0]

Premises used: Valuation.IsTrivialOn.eq_one, pow_le_one', RatFunc.algebraMap_eq_C
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation.{u_1, u_2} K⟮X⟯ Γ
hv : IsTrivialOn K v
n : ℕ
a : K
ha : a ≠ 0
⊢ (v : (a : K⟮X⟯) → Γ) (HDiv.hDiv (α := K⟮X⟯) 1 (↑((monomial n : (a : K) → K[X]) a) : K⟮X⟯)) =
    HPow.hPow (α := Γ) (β := ℤ) ((v : (a : K⟮X⟯) → Γ) RatFunc.X : Γ) (-(↑n : ℤ))

Tactic:
simp [← RatFunc.algebraMap_eq_C, hv.eq_one _ ha]

Premises used: Valuation.IsTrivialOn.eq_one, RatFunc.algebraMap_eq_C
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
x : K⟮X⟯
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (((IsDedekindDomain.HeightOneSpectrum.valuation (R := K[X]) K⟮X⟯ (idealX K) :
            Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
pos :
  ∀ (hn0 : n = 0),
    ∃ (a : K⟮X⟯),
      ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
neg :
  ∀ (hn0 : ¬n = 0),
    ∃ (a : K⟮X⟯),
      ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
h : ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 = n
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n

Tactic:
use 0
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 = n

Tactic:
simp [hn0]
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
h :
  ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟮X⟯) X (-n.log)) =
    n
⊢ ∃ (a : K⟮X⟯),
    ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) a = n

Tactic:
use (RatFunc.X ^ (-WithZero.log n))

Premises used: RatFunc.X, WithZero.log, HPow.hPow, Neg.neg
-- Module: Mathlib.FieldTheory.RatFunc.AsPolynomial
Goal:
K : Type u_1
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟮X⟯) X (-n.log)) =
    n

Tactic:
simp [WithZero.exp_log hn0]

Premises used: WithZero.exp_log
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
⊢ Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } 0

Tactic:
zero_def.symm

Premises used: RatFunc.zero_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
p q : FractionRing K[X]
⊢ { toFractionRing := p + q : K⟮X⟯ } = { toFractionRing := p : K⟮X⟯ } + { toFractionRing := q : K⟮X⟯ }

Tactic:
(add_def _ _).symm

Premises used: RatFunc.add_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
p q : FractionRing K[X]
⊢ { toFractionRing := p - q : K⟮X⟯ } = { toFractionRing := p : K⟮X⟯ } - { toFractionRing := q : K⟮X⟯ }

Tactic:
(sub_def _ _).symm

Premises used: RatFunc.sub_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
p : FractionRing K[X]
⊢ { toFractionRing := -p : K⟮X⟯ } = -{ toFractionRing := p }

Tactic:
(neg_def _).symm

Premises used: RatFunc.neg_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
⊢ Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 1 } 1

Tactic:
one_def.symm

Premises used: RatFunc.one_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
p q : FractionRing K[X]
⊢ { toFractionRing := p * q : K⟮X⟯ } = { toFractionRing := p : K⟮X⟯ } * { toFractionRing := q : K⟮X⟯ }

Tactic:
(mul_def _ _).symm

Premises used: Eq.symm, RatFunc.mul_def
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p q : FractionRing K[X]
⊢ { toFractionRing := p / q : K⟮X⟯ } = { toFractionRing := p : K⟮X⟯ } / { toFractionRing := q : K⟮X⟯ }

Tactic:
(div_def _ _).symm

Premises used: RatFunc.div_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
⊢ { toFractionRing := p⁻¹ : K⟮X⟯ } = { toFractionRing := p }⁻¹

Tactic:
(inv_def _).symm

Premises used: RatFunc.inv_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
hp : p = 0
rw : Eq.{u + 1} (α := K⟮X⟯) { toFractionRing := 0 } 0
rw₁ rw₂ : Eq.{u + 1} (α := K⟮X⟯) 0 0
⊢ { toFractionRing := p : K⟮X⟯ } = 0

Tactic:
rw [hp, ofFractionRing_zero]

Premises used: RatFunc.ofFractionRing_zero
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
⊢ p ≠ 0

Tactic:
have : p ≠ 0 := fun hp => h <| by rw [hp, ofFractionRing_zero]
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
inst_1 : IsDomain K
p : FractionRing K[X]
h : { toFractionRing := p : K⟮X⟯ } ≠ 0
this : p ≠ 0
⊢ { toFractionRing := p : K⟮X⟯ } * { toFractionRing := p : K⟮X⟯ }⁻¹ = 1

Tactic:
simpa only [← ofFractionRing_inv, ← ofFractionRing_mul, ← ofFractionRing_one,
        ofFractionRing.injEq] using
      mul_inv_cancel₀ this

Premises used: RatFunc.ofFractionRing.injEq, mul_inv_cancel₀, RatFunc.ofFractionRing_one, RatFunc.ofFractionRing_inv, RatFunc.ofFractionRing_mul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : SMul.{u_1, u} R (FractionRing K[X])
c : R
p : FractionRing K[X]
⊢ { toFractionRing := c • p : K⟮X⟯ } = c • { toFractionRing := p : K⟮X⟯ }

Tactic:
(smul_def _ _).symm

Premises used: RatFunc.smul_def, Eq.symm
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : SMul.{u_1, u} R (FractionRing K[X])
c : R
p : K⟮X⟯
ofFractionRing :
  ∀ (toFractionRing : FractionRing K[X]),
    (c • { toFractionRing := toFractionRing : K⟮X⟯ }).toFractionRing =
      c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing
⊢ (c • p).toFractionRing = c • p.toFractionRing

Tactic:
cases p
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
R : Type u_1
inst_1 : SMul.{u_1, u} R (FractionRing K[X])
c : R
toFractionRing : FractionRing K[X]
ofFractionRing ofFractionRing₁ :
  { toFractionRing := c • toFractionRing : K⟮X⟯ }.toFractionRing =
    c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing
⊢ (c • { toFractionRing := toFractionRing : K⟮X⟯ }).toFractionRing =
    c • { toFractionRing := toFractionRing : K⟮X⟯ }.toFractionRing

Tactic:
rw [← ofFractionRing_smul]

Premises used: RatFunc.ofFractionRing_smul
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
x : K⟮X⟯
r : K
obtain :
  ∀ (x : FractionRing K[X]),
    r • { toFractionRing := x : K⟮X⟯ } =
      HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) { toFractionRing := x : K⟮X⟯ }
⊢ r • x = HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) x

Tactic:
obtain ⟨x⟩ := x
-- Module: Mathlib.FieldTheory.RatFunc.Basic
Goal:
K : Type u
inst : CommRing K
r : K
x : FractionRing K[X]
H :
  ∀ (y : K[X] × ↥K[X]⁰),
    r • { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ } =
      HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X])
        { toFractionRing := Localization.mk y.1 y.2 : K⟮X⟯ }
⊢ r • { toFractionRing := x : K⟮X⟯ } =
    HSMul.hSMul (α := K[X]) ((Polynomial.C : (a : K) → K[X]) r : K[X]) { toFractionRing := x : K⟮X⟯ }

Tactic:
induction x using Localization.induction_on