case refine'_1
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f) →
    f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i

case refine'_2
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ f ∈ Finset.finsupp s t ↔ f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
refine' mem_map.trans ⟨_, _⟩
case refine'_1.intro.intro
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f).support ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
case refine'_1
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f) →
    f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
rintro ⟨f, hf, rfl⟩
case refine'_1.intro.intro
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
case refine'_1.intro.intro
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f).support ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
refine' ⟨support_indicator_subset _ _, fun i hi => _⟩
case h.e'_4
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i = f i hi
case refine'_1.intro.intro
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i ∈ t i
convert mem_pi.1 hf i hi
no goals
case h.e'_4
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } f) i = f i hi
exact indicator_of_mem hi _
case refine'_2
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) = f
case refine'_2
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a, a ∈ pi s t ∧ ↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } a = f
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
case refine'_2.h
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) i = ↑f i
case refine'_2
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) = f
ext i
no goals
case refine'_2.h
ι : Type u_2
α : Type u_1
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := indicator s, inj' := (_ : Function.Injective fun f => indicator s f) } fun i x => ↑f i) i = ↑f i
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm