-- Mathlib/Data/Finsupp/Weight.lean
theorem weight_eq_zero_iff_eq_zero
    (w : σ → M) [NonTorsionWeight ℕ w] {f : σ →₀ ℕ} :
    weight w f = 0 ↔ f = 0

Proof state:
case mp
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
⊢ f = 0

Tactic:
ext s

Result:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0 s

Proof state:
case mp
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 → f = 0

Tactic:
intro h

Result:
case mp
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
⊢ f = 0

Proof state:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s = 0

Tactic:
rw [← nonpos_iff_eq_zero, ← h]

Result:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s ≤ (weight w) f

Proof state:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0

Tactic:
by_contra hs

Result:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ False

Proof state:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s ≤ (weight w) f

Tactic:
exact le_weight_of_ne_zero' w hs

Result:
no goals

Proof state:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0 s

Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply]

Result:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
⊢ f s = 0

Proof state:
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 ↔ f = 0

Tactic:
constructor

Result:
case mp
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ (weight w) f = 0 → f = 0

case mpr
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0

Proof state:
case mpr
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) f = 0

Tactic:
rw [h, map_zero]

Result:
no goals

Proof state:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ False

Tactic:
apply NonTorsionWeight.ne_zero ℕ w s

Result:
case mp.h
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : (weight w) f = 0
s : σ
hs : ¬f s = 0
⊢ w s = 0

Proof state:
case mpr
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
⊢ f = 0 → (weight w) f = 0

Tactic:
intro h

Result:
case mpr
σ : Type u_1
M : Type u_4
inst✝² : OrderedAddCommMonoid M
inst✝¹ : CanonicallyOrderedAdd M
w : σ → M
inst✝ : NonTorsionWeight ℕ w
f : σ →₀ ℕ
h : f = 0
⊢ (weight w) f = 0