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

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ f ≠ 0
Tactic:
refine' not_iff_not.mp _
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (¬∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ ¬f ≠ 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (¬∃ n d, (weight w) d = n ∧ (coeff α d) f ≠ 0) ↔ ¬f ≠ 0
Tactic:
push_neg
State after:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) ↔ f = 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) ↔ f = 0
Tactic:
constructor
State after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) → f = 0

case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = 0 → ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0

State before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ (∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0) → f = 0
Tactic:
intro h
State after:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
⊢ f = 0

State before:
case mp
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
⊢ f = 0
Tactic:
ext d
State after:
case mp.h
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0

State before:
case mp.h
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
h : ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) 0
Tactic:
exact h _ d rfl
State after:
no goals

State before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = 0 → ∀ (n : ℕ) (d : σ →₀ ℕ), (weight w) d = n → (coeff α d) f = 0
Tactic:
rintro rfl n d _
State after:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
n : ℕ
d : σ →₀ ℕ
_✝ : (weight w) d = n
⊢ (coeff α d) 0 = 0

State before:
case mpr
σ : Type u_1
α : Type u_2
inst✝ : Semiring α
w : σ → ℕ
n : ℕ
d : σ →₀ ℕ
_✝ : (weight w) d = n
⊢ (coeff α d) 0 = 0
Tactic:
exact coeff_zero _
State after:
no goals