case h₀
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), b ∈ x.support → b ≠ a → ↑(single (f b) (↑x b)) (f a) = 0

case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ¬a ∈ x.support → ↑(single (f a) (↑x a)) (f a) = 0
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ↑(mapDomain f x) (f a) = ↑x a
rw [mapDomain, sum_apply, sum, Finset.sum_eq_single a, single_eq_same]
case h₀
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
a✝ : b ∈ x.support
hba : b ≠ a
⊢ ↑(single (f b) (↑x b)) (f a) = 0
case h₀
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ∀ (b : α), b ∈ x.support → b ≠ a → ↑(single (f b) (↑x b)) (f a) = 0
intro b _ hba
no goals
case h₀
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a b : α
a✝ : b ∈ x.support
hba : b ≠ a
⊢ ↑(single (f b) (↑x b)) (f a) = 0
exact single_eq_of_ne (hf.ne hba)
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : ¬a ∈ x.support
⊢ ↑(single (f a) (↑x a)) (f a) = 0
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ ¬a ∈ x.support → ↑(single (f a) (↑x a)) (f a) = 0
intro h
no goals
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.154448
ι : Type ?u.154451
M : Type u_3
M' : Type ?u.154457
N : Type ?u.154460
P : Type ?u.154463
G : Type ?u.154466
H : Type ?u.154469
R : Type ?u.154472
S : Type ?u.154475
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : ¬a ∈ x.support
⊢ ↑(single (f a) (↑x a)) (f a) = 0
rw [not_mem_support_iff.1 h, single_zero, zero_apply]