-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_eq_emultiplicity_X {R : Type*} [Semiring R] (φ : R⟦X⟧) :
    order φ = emultiplicity X φ

Proof state:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (X ^ (φ.order.lift ⋯ + 1) * ψ)
⊢ False

Tactic:
rw [← (ψ.commute_X.pow_right _).eq, coeff_mul_of_lt_order, ← hn] at this

Result:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R (φ.order.lift ⋯)) φ = 0
⊢ False

case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
⊢ ↑n < (X ^ (φ.order.lift ⋯ + 1)).order

Proof state:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ↑n = emultiplicity X φ

Tactic:
rw [← hn, eq_comm]

Result:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ = ↑(φ.order.lift ⋯)

Proof state:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = emultiplicity X φ

Tactic:
rcases eq_or_ne φ 0 with (rfl | hφ)

Result:
case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0

case inr
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
⊢ φ.order = emultiplicity X φ

Proof state:
case h
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ¬X ^ (φ.order.lift ⋯ + 1) ∣ φ

Tactic:
rintro ⟨ψ, H⟩

Result:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
⊢ False

Proof state:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
⊢ φ.order.lift ⋯ = n

Tactic:
simp [ho]

Result:
no goals

Proof state:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ = ↑(φ.order.lift ⋯)

Tactic:
apply le_antisymm _

Result:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ↑(φ.order.lift ⋯) ≤ emultiplicity X φ

R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ ≤ ↑(φ.order.lift ⋯)

Proof state:
case h
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ < ↑(φ.order.lift ⋯) + 1

Tactic:
rw [← not_le, ← Nat.cast_one, ← Nat.cast_add, ← pow_dvd_iff_le_emultiplicity]

Result:
case h
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ¬X ^ (φ.order.lift ⋯ + 1) ∣ φ

Proof state:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.lift ⋯ + 1)

Tactic:
rw [← hn, ENat.coe_lt_coe]

Result:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : ¬1 = 0
⊢ φ.order.lift ⋯ < φ.order.lift ⋯ + 1

Proof state:
case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

Tactic:
simp

Result:
no goals

Proof state:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
⊢ ↑n = emultiplicity X φ

Tactic:
have hn : φ.order.lift (order_finite_iff_ne_zero.mpr hφ) = n := by simp [ho]

Result:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ↑n = emultiplicity X φ

Proof state:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R (φ.order.lift ⋯)) φ = 0
⊢ False

Tactic:
exact coeff_order _ this

Result:
no goals

Proof state:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ ↑(φ.order.lift ⋯) ≤ emultiplicity X φ

Tactic:
apply le_emultiplicity_of_pow_dvd

Result:
case inr.coe.hk
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ X ^ φ.order.lift ⋯ ∣ φ

Proof state:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(φ.order.lift ⋯ + 1)

Tactic:
split_ifs

Result:
case pos
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.lift ⋯ + 1)

Proof state:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
h✝ : ¬1 = 0
⊢ φ.order.lift ⋯ < φ.order.lift ⋯ + 1

Tactic:
simp

Result:
no goals

Proof state:
case inr.top
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
ho : φ.order = ⊤
⊢ ⊤ = emultiplicity X φ

Tactic:
simp [hφ] at ho

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ ≤ ↑(φ.order.lift ⋯)

Tactic:
apply Order.le_of_lt_add_one

Result:
case h
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ emultiplicity X φ < ↑(φ.order.lift ⋯) + 1

Proof state:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
⊢ False

Tactic:
have := congr_arg (coeff R n) H

Result:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (X ^ (φ.order.lift ⋯ + 1) * ψ)
⊢ False

Proof state:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
⊢ ↑n < (X ^ (φ.order.lift ⋯ + 1)).order

Tactic:
rw [X_pow_eq, order_monomial]

Result:
case h.intro
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.lift ⋯ + 1) * ψ
this : (coeff R n) φ = (coeff R n) (ψ * X ^ (φ.order.lift ⋯ + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(φ.order.lift ⋯ + 1)

Proof state:
case inr.coe.hk
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.lift ⋯ = n
⊢ X ^ φ.order.lift ⋯ ∣ φ

Tactic:
apply X_pow_order_dvd

Result:
no goals