case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ powerSeriesPart x = 0 → x = 0

case mpr
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x = 0 → powerSeriesPart x = 0
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ powerSeriesPart x = 0 ↔ x = 0
constructor
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x ≠ 0 → powerSeriesPart x ≠ 0
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ powerSeriesPart x = 0 → x = 0
contrapose!
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ¬x = 0 → ¬powerSeriesPart x = 0
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x ≠ 0 → powerSeriesPart x ≠ 0
simp only [ne_eq]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬powerSeriesPart x = 0
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ ¬x = 0 → ¬powerSeriesPart x = 0
intro h
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ∃ x_1, ¬↑(PowerSeries.coeff R x_1) (powerSeriesPart x) = ↑(PowerSeries.coeff R x_1) 0
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬powerSeriesPart x = 0
rw [PowerSeries.ext_iff, not_forall]
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬↑(PowerSeries.coeff R 0) (powerSeriesPart x) = ↑(PowerSeries.coeff R 0) 0
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ∃ x_1, ¬↑(PowerSeries.coeff R x_1) (powerSeriesPart x) = ↑(PowerSeries.coeff R x_1) 0
refine' ⟨0, _⟩
no goals
case mp
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
h : ¬x = 0
⊢ ¬↑(PowerSeries.coeff R 0) (powerSeriesPart x) = ↑(PowerSeries.coeff R 0) 0
simp [coeff_order_ne_zero h]
case mpr
R : Type u
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0
case mpr
R : Type u
inst✝ : Semiring R
x : LaurentSeries R
⊢ x = 0 → powerSeriesPart x = 0
rintro rfl
no goals
case mpr
R : Type u
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0
simp