Theorem: DirectSum.mk_apply_of_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 = f ⟨n, hn⟩
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) = f ⟨n, hn⟩

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) = f ⟨n, hn⟩
Tactic:
rw [dif_pos hn]
State after:
no goals