R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom ↔ φ ≠ 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (order φ).Dom ↔ φ ≠ 0
simp only [order]
case mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom → φ ≠ 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ φ ≠ 0 → (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom ↔ φ ≠ 0
constructor
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : φ = 0
H : ⊤.Dom
⊢ φ ≠ 0

case mp.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ¬φ = 0
H : (↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
⊢ φ ≠ 0
case mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom → φ ≠ 0
split_ifs with h <;> intro H
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h H : φ = 0
⊢ ¬⊤.Dom
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : φ = 0
H : ⊤.Dom
⊢ φ ≠ 0
contrapose! H
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h H : φ = 0
⊢ ⊤ = Part.none
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h H : φ = 0
⊢ ¬⊤.Dom
simp only [← Part.eq_none_iff']
no goals
case mp.inl
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h H : φ = 0
⊢ ⊤ = Part.none
rfl
no goals
case mp.inr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ¬φ = 0
H : (↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
⊢ φ ≠ 0
exact h
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : φ ≠ 0
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ φ ≠ 0 → (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
intro h
no goals
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : φ ≠ 0
⊢ (if h : φ = 0 then ⊤ else ↑(Nat.find (_ : ∃ n, ↑(coeff R n) φ ≠ 0))).Dom
simp [h]