-- Mathlib/Data/DFinsupp/Interval.lean
theorem mem_dfinsupp_iff : f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

Proof state:
case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, 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✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ ({ toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } f).support ⊆ s ∧
    ∀ i ∈ s, ({ toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } f) i ∈ t i

Proof state:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) →
    ∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, 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✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
⊢ ({ toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } fun i x => f i) = f

Proof state:
case h.e'_5
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i => f ↑i ⋯) i = f i hi

Tactic:
exact mk_of_mem hi

Result:
no goals

Proof state:
case refine_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i => f ↑i ⋯) i ∈ t i

Tactic:
convert mem_pi.1 hf i hi

Result:
case h.e'_5
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i => f ↑i ⋯) i = f i hi

Proof state:
case refine_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ (if i ∈ s then f i else 0) = 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 refine_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ (DFinsupp.mk s fun i => f ↑i ⋯).support ⊆ s ∧ ∀ i ∈ s, (DFinsupp.mk s fun i => f ↑i ⋯) i ∈ t i

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

Result:
case refine_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (DFinsupp.mk s fun i => f ↑i ⋯) i ∈ t i

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

Tactic:
ext i

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

Proof state:
case refine_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ ({ toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } f).support ⊆ s ∧
    ∀ i ∈ s, ({ toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } f) i ∈ t i

Tactic:
rw [Function.Embedding.coeFn_mk]

Result:
case refine_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → α a
hf : f ∈ s.pi t
⊢ (DFinsupp.mk s fun i => f ↑i ⋯).support ⊆ s ∧ ∀ i ∈ s, (DFinsupp.mk s fun i => f ↑i ⋯) i ∈ t i

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

Tactic:
dsimp

Result:
case refine_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ (if i ∈ s then f i else 0) = f i

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ f ∈ s.dfinsupp 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✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } a = f) →
    f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i

case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i) →
    ∃ a ∈ s.pi t, { toFun := fun f => DFinsupp.mk s fun i => f ↑i ⋯, inj' := ⋯ } a = f