case h.e'_2.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ (∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ X ^ n ∣ φ ↔ ∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0
convert@MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0
m : Unit →₀ ℕ
hm : ↑m () < n
⊢ ↑(MvPowerSeries.coeff R m) φ = 0

case h.e'_2.a.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ ↑(coeff R m) φ = 0
case h.e'_2.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
⊢ (∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0) ↔ ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
constructor <;> intro h m hm
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0
m : Unit →₀ ℕ
hm : ↑m () < n
⊢ ↑(MvPowerSeries.coeff R (single default (↑m default))) φ = 0
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0
m : Unit →₀ ℕ
hm : ↑m () < n
⊢ ↑(MvPowerSeries.coeff R m) φ = 0
rw [Finsupp.unique_single m]
no goals
case h.e'_2.a.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : ℕ), m < n → ↑(coeff R m) φ = 0
m : Unit →₀ ℕ
hm : ↑m () < n
⊢ ↑(MvPowerSeries.coeff R (single default (↑m default))) φ = 0
convert h _ hm
case h.e'_2.a.mpr.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ ↑(single () m) () < n
case h.e'_2.a.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ ↑(coeff R m) φ = 0
apply h
no goals
case h.e'_2.a.mpr.a
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : PowerSeries R
h : ∀ (m : Unit →₀ ℕ), ↑m () < n → ↑(MvPowerSeries.coeff R m) φ = 0
m : ℕ
hm : m < n
⊢ ↑(single () m) () < n
simpa only [Finsupp.single_eq_same] using hm