[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
⊢ f ∈ Finset.finsupp s t ↔ f.support ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
refine' mem_map.trans ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
rintro ⟨f, hf, rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' ⟨support_indicator_subset _ _, fun i hi => _⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
convert mem_pi.1 hf i hi
[GOAL]
case h.e'_4
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact indicator_of_mem hi _
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
ext i
[GOAL]
case refine'_2.h
ι : Type u_1
α : Type u_2
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
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
⊢ f ∈ Finset.finsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i
[PROOFSTEP]
refine'
  mem_finsupp_iff.trans
    (forall_and.symm.trans <|
      forall_congr' fun i =>
        ⟨fun h => _, fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi _, fun _ => h⟩⟩)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
by_cases hi : i ∈ s
[GOAL]
case pos
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
exact h.2 hi
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 fun H => hi <| ht H]
[GOAL]
case neg
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : (i ∈ f.support → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
[PROOFSTEP]
exact zero_mem_zero
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι →₀ Finset α
ht : t.support ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ f.support
H : ↑t i = 0
⊢ ↑f i = 0
[PROOFSTEP]
rwa [H, mem_zero] at h 
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
rw [pi, card_finsupp]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
⊢ ∏ i in f.support, card (↑f i) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f✝ : ι →₀ α
f : ι →₀ Finset α
i : ι
x✝ : i ∈ f.support
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
[PROOFSTEP]
simp only [Pi.nat_apply, Nat.cast_id]
