case inl
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
⊢ order 0 = multiplicity X 0

case inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
⊢ order φ = multiplicity X φ
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ order φ = multiplicity X φ
rcases eq_or_ne φ 0 with (rfl | hφ)
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
ho : order φ = ⊤
⊢ ⊤ = multiplicity X φ

case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
⊢ ↑n = multiplicity X φ
case inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
⊢ order φ = multiplicity X φ
induction' ho : order φ using PartENat.casesOn with n
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ↑n = multiplicity X φ
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
⊢ ↑n = multiplicity X φ
have hn : φ.order.get (order_finite_iff_ne_zero.mpr hφ) = n := by simp [ho]
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ↑(Part.get (order φ) (_ : (order φ).Dom)) = multiplicity X φ
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ↑n = multiplicity X φ
rw [← hn]
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ¬X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) ∣ φ
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ↑(Part.get (order φ) (_ : (order φ).Dom)) = multiplicity X φ
refine'
  le_antisymm (le_multiplicity_of_pow_dvd <| X_pow_order_dvd (order_finite_iff_ne_zero.mpr hφ))
    (PartENat.find_le _ _ _)
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
⊢ False
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
⊢ ¬X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) ∣ φ
rintro ⟨ψ, H⟩
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ)
⊢ False
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
⊢ False
have := congr_arg (coeff R n) H
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R (Part.get (order φ) (_ : (order φ).Dom))) φ = 0
⊢ False

case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
⊢ ↑n < order (X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ)
⊢ False
rw [← (ψ.commute_X.pow_right _).eq, coeff_mul_of_lt_order, ← hn] at this
no goals
case inl
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
⊢ order 0 = multiplicity X 0
simp
no goals
case inr.a
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
ho : order φ = ⊤
⊢ ⊤ = multiplicity X φ
simp [hφ] at ho
no goals
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
⊢ Part.get (order φ) (_ : (order φ).Dom) = n
simp [ho]
no goals
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R (Part.get (order φ) (_ : (order φ).Dom))) φ = 0
⊢ False
exact coeff_order _ this
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(Part.get (order φ) (_ : (order φ).Dom) + 1)
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
⊢ ↑n < order (X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
rw [X_pow_eq, order_monomial]
case inr.a.intro.inl
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

case inr.a.intro.inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(Part.get (order φ) (_ : (order φ).Dom) + 1)
case inr.a.intro
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(Part.get (order φ) (_ : (order φ).Dom) + 1)
split_ifs
no goals
case inr.a.intro.inl
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤
exact PartENat.natCast_lt_top _
case inr.a.intro.inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : ¬1 = 0
⊢ Part.get (order φ) (_ : (order φ).Dom) < Part.get (order φ) (_ : (order φ).Dom) + 1
case inr.a.intro.inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(Part.get (order φ) (_ : (order φ).Dom) + 1)
rw [← hn, PartENat.coe_lt_coe]
no goals
case inr.a.intro.inr
R✝ : Type ?u.4264976
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
hφ : φ ≠ 0
x✝ : PartENat
ho✝ : order φ = x✝
n : ℕ
ho : order φ = ↑n
hn : Part.get (order φ) (_ : (order φ).Dom) = n
ψ : PowerSeries R
H : φ = X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1) * ψ
this : ↑(coeff R n) φ = ↑(coeff R n) (ψ * X ^ (Part.get (order φ) (_ : (order φ).Dom) + 1))
h✝ : ¬1 = 0
⊢ Part.get (order φ) (_ : (order φ).Dom) < Part.get (order φ) (_ : (order φ).Dom) + 1
exact Nat.lt_succ_self _