ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
⊢ ↑(indicator s f).support ⊆ ↑s
intro i hi
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
⊢ i ∈ ↑s
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s
rw [mem_coe, mem_support_iff] at hi
ι : 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
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i✝ i : ι
hi : ↑(indicator s f) i ≠ 0
⊢ i ∈ ↑s
by_contra h
no goals
ι : 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
exact hi (indicator_of_not_mem h _)