-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_eq_LaurentSeries_valuation (P : RatFunc K) :
    (Polynomial.idealX K).valuation _ P = (PowerSeries.idealX K).valuation K⸨X⸩ P

Proof state:
K : Type u_2
inst✝ : Field K
P : RatFunc K
⊢ ∀ (p q : K[X]),
    q ≠ 0 →
      (valuation (RatFunc K) (Polynomial.idealX K)) (RatFunc.mk p q) =
        (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(RatFunc.mk p q)

Tactic:
intro f g h

Result:
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (valuation (RatFunc K) (Polynomial.idealX K)) (RatFunc.mk f g) =
    (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(RatFunc.mk f g)

Proof state:
case h.e'_2.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ ↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) = IsLocalization.mk' K⸨X⸩ ↑f ⟨↑g, ⋯⟩

Tactic:
simp only [IsFractionRing.mk'_eq_div, coe_div, LaurentSeries.coe_algebraMap, coe_coe]

Result:
case h.e'_2.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ ↑((algebraMap K[X] (RatFunc K)) f) / ↑((algebraMap K[X] (RatFunc K)) g) = ↑↑f / ↑↑g

Proof state:
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (valuation (RatFunc K) (Polynomial.idealX K)) (RatFunc.mk f g) =
    (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(RatFunc.mk f g)

Tactic:
rw [Polynomial.valuation_of_mk K f h, RatFunc.mk_eq_mk' f h, Eq.comm]

Result:
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) =
    (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g

Proof state:
case h.e'_2.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ ↑((algebraMap K[X] (RatFunc K)) f) / ↑((algebraMap K[X] (RatFunc K)) g) = ↑↑f / ↑↑g

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) =
    (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g

Tactic:
convert @valuation_of_mk' K⟦X⟧ _ _ K⸨X⸩ _ _ _ (PowerSeries.idealX K) f
      ⟨g, mem_nonZeroDivisors_iff_ne_zero.2 <| coe_ne_zero h⟩

Result:
case h.e'_2.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ ↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) = IsLocalization.mk' K⸨X⸩ ↑f ⟨↑g, ⋯⟩

case h.e'_3.h.e'_5
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (Polynomial.idealX K).intValuation f = (PowerSeries.idealX K).intValuation ↑f

case h.e'_3.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (Polynomial.idealX K).intValuation g = (PowerSeries.idealX K).intValuation ↑⟨↑g, ⋯⟩

Proof state:
case h.e'_3.h.e'_5
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (Polynomial.idealX K).intValuation f = (PowerSeries.idealX K).intValuation ↑f

case h.e'_3.h.e'_6
K : Type u_2
inst✝ : Field K
P : RatFunc K
f g : K[X]
h : g ≠ 0
⊢ (Polynomial.idealX K).intValuation g = (PowerSeries.idealX K).intValuation ↑⟨↑g, ⋯⟩

Tactic:
exacts [intValuation_eq_of_coe _, intValuation_eq_of_coe _]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
P : RatFunc K
⊢ (valuation (RatFunc K) (Polynomial.idealX K)) P = (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑P

Tactic:
refine RatFunc.induction_on' P ?_

Result:
K : Type u_2
inst✝ : Field K
P : RatFunc K
⊢ ∀ (p q : K[X]),
    q ≠ 0 →
      (valuation (RatFunc K) (Polynomial.idealX K)) (RatFunc.mk p q) =
        (valuation K⸨X⸩ (PowerSeries.idealX K)) ↑(RatFunc.mk p q)