[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s✝ : Finset ι
f✝ : (i : ι) → i ∈ s✝ → α
i✝ : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ map (Embedding.subtype fun x => x ∈ s) (filter (fun i => f ↑i (_ : ↑i ∈ s) ≠ 0) (attach s)) ↔
    (fun i => if H : i ∈ s then f i H else 0) i ≠ 0
[PROOFSTEP]
classical simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s✝ : Finset ι
f✝ : (i : ι) → i ∈ s✝ → α
i✝ : ι
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ i ∈ map (Embedding.subtype fun x => x ∈ s) (filter (fun i => f ↑i (_ : ↑i ∈ s) ≠ 0) (attach s)) ↔
    (fun i => if H : i ∈ s then f i H else 0) i ≠ 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ ↑(indicator s f) i = if hi : i ∈ s then f i hi else 0
[PROOFSTEP]
simp only [indicator, ne_eq, coe_mk]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0
[PROOFSTEP]
congr
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ Injective fun f => indicator s f
[PROOFSTEP]
intro a b h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
⊢ a = b
[PROOFSTEP]
ext i hi
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ a i hi = b i hi
[PROOFSTEP]
rw [← indicator_of_mem hi a, ← indicator_of_mem hi b]
[GOAL]
case h.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ : ι
a b : (i : ι) → i ∈ s → α
h : (fun f => indicator s f) a = (fun f => indicator s f) b
i : ι
hi : i ∈ s
⊢ ↑(indicator s a) i = ↑(indicator s b) i
[PROOFSTEP]
exact FunLike.congr_fun h i
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ ↑(indicator s f).support ⊆ ↑s
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s
[PROOFSTEP]
rw [mem_coe, mem_support_iff] at hi 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
⊢ i ∈ ↑s
[PROOFSTEP]
by_contra h
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
h : ¬i ∈ ↑s
⊢ False
[PROOFSTEP]
exact hi (indicator_of_not_mem h _)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b
[PROOFSTEP]
classical
ext j
simp [single_apply, indicator_apply, @eq_comm _ j]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
b : α
j : ι
⊢ ↑(single i b) j = ↑(indicator {i} fun x x => b) j
[PROOFSTEP]
simp [single_apply, indicator_apply, @eq_comm _ j]
