no goals
α : Type u_3
ι : Type ?u.32313
γ : Type ?u.32316
A : Type ?u.32319
B : Type ?u.32322
C : Type ?u.32325
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : AddCommMonoid C
t : ι → A → C
h0✝ : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g✝ : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.35455
M : Type u_2
M' : Type u_1
N : Type u_4
P : Type ?u.35467
G : Type ?u.35470
H✝ : Type ?u.35473
R : Type ?u.35476
S : Type ?u.35479
inst✝² : Zero M
inst✝¹ : Zero M'
inst✝ : CommMonoid N
f : M → M'
hf : f 0 = 0
g : α →₀ M
h : α → M' → N
h0 : ∀ (a : α), h a 0 = 1
x✝¹ : α
x✝ : x✝¹ ∈ g.support
H : ¬x✝¹ ∈ (mapRange f hf g).support
⊢ h x✝¹ (↑(mapRange f hf g) x✝¹) = 1
rw [not_mem_support_iff.1 H, h0]