α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
b : M
⊢ f.support ⊆ {a} ∧ ↑f a = b → f = single a b
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
b : M
⊢ f = single a b ↔ f.support ⊆ {a} ∧ ↑f a = b
refine' ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, _⟩
case intro
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a (↑f a)
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b✝ : M
f : α →₀ M
a : α
b : M
⊢ f.support ⊆ {a} ∧ ↑f a = b → f = single a b
rintro ⟨h, rfl⟩
case intro.h
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ ↑f x = ↑(single a (↑f a)) x
case intro
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
⊢ f = single a (↑f a)
ext x
case neg
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ ↑f x = 0
case intro.h
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
⊢ ↑f x = ↑(single a (↑f a)) x
by_cases hx : a = x <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne.def, not_false_iff]
no goals
case neg
α : Type u_1
β : Type ?u.54288
γ : Type ?u.54291
ι : Type ?u.54294
M : Type u_2
M' : Type ?u.54300
N : Type ?u.54303
P : Type ?u.54306
G : Type ?u.54309
H : Type ?u.54312
R : Type ?u.54315
S : Type ?u.54318
inst✝ : Zero M
a✝ a' : α
b : M
f : α →₀ M
a : α
h : f.support ⊆ {a}
x : α
hx : ¬a = x
⊢ ↑f x = 0
exact not_mem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx)).symm) hx)