Theorem: MvPowerSeries.weightedOrder_finite_iff_ne_zero (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ↑(toNat (weightedOrder w f)) = weightedOrder w f ↔ f ≠ 0
Tactic:
simp only [weightedOrder]
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) ↔ f ≠ 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) ↔ f ≠ 0
Tactic:
constructor
State after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) → f ≠ 0

case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f ≠ 0 → ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)

State before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)) → f ≠ 0
Tactic:
split_ifs with h <;> intro H
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ f ≠ 0

case neg
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ¬f = 0
H : ↑(toNat ↑(Nat.find ⋯)) = ↑(Nat.find ⋯)
⊢ f ≠ 0

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ f ≠ 0
Tactic:
exfalso
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ False

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f = 0
H : ↑(toNat ⊤) = ⊤
⊢ False
Tactic:
apply ENat.coe_ne_top _ H
State after:
no goals

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ¬f = 0
H : ↑(toNat ↑(Nat.find ⋯)) = ↑(Nat.find ⋯)
⊢ f ≠ 0
Tactic:
exact h
State after:
no goals

State before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f ≠ 0 → ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Tactic:
intro h
State after:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f ≠ 0
⊢ ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)

State before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : f ≠ 0
⊢ ↑(toNat (if x : f = 0 then ⊤ else ↑(Nat.find ⋯))) = if x : f = 0 then ⊤ else ↑(Nat.find ⋯)
Tactic:
simp only [h, not_false_iff, dif_neg, toNat_coe]
State after:
no goals