-- Mathlib/Data/Finset/Finsupp.lean
theorem mem_finsupp_iff {t : ι → Finset α} :
    f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) → ∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f

Tactic:
refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩

Result:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x => f i) = f

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f) → f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
rintro ⟨f, hf, rfl⟩

Result:
case refine_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
⊢ ({ toFun := indicator s, inj' := ⋯ } f).support ⊆ s ∧ ∀ i ∈ s, ({ toFun := indicator s, inj' := ⋯ } f) i ∈ t i

Proof state:
case refine_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ ({ toFun := indicator s, inj' := ⋯ } f) i ∈ t i

Tactic:
convert mem_pi.1 hf i hi

Result:
case h.e'_5
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ ({ toFun := indicator s, inj' := ⋯ } f) i = f i hi

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Tactic:
refine mem_map.trans ⟨?_, ?_⟩

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f) → f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) → ∃ a ∈ s.pi t, { toFun := indicator s, inj' := ⋯ } a = f

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x => f i) = f

Tactic:
ext i

Result:
case refine_2.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x => f i) i = f i

Proof state:
case refine_2.h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x => f i) i = f i

Tactic:
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm

Result:
no goals

Proof state:
case h.e'_5
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ ({ toFun := indicator s, inj' := ⋯ } f) i = f i hi

Tactic:
exact indicator_of_mem hi _

Result:
no goals

Proof state:
case refine_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
⊢ ({ toFun := indicator s, inj' := ⋯ } f).support ⊆ s ∧ ∀ i ∈ s, ({ toFun := indicator s, inj' := ⋯ } f) i ∈ t i

Tactic:
refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩

Result:
case refine_1.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
t : ι → Finset α
f : (i : ι) → i ∈ s → α
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ ({ toFun := indicator s, inj' := ⋯ } f) i ∈ t i