Theorem: DirectSum.mk_apply_of_not_mem (DividedPowers/ForMathlib/GradedAlgebra.lean)

State before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ ((mk β s) f) n = 0
Tactic:
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
State after:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0

State before:
ι : Type v
inst✝¹ : DecidableEq ι
β : ι → Type w
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ↑↑s) → β ↑i
n : ι
hn : n ∉ s
⊢ (if H : n ∈ s then f ⟨n, H⟩ else 0) = 0
Tactic:
rw [dif_neg hn]
State after:
no goals