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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ support f
H : ↑t i = 0
⊢ ↑f i = 0
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
⊢ f ∈ dfinsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i
refine' mem_dfinsupp_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⟩⟩)
case pos
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i

case neg
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑f i ∈ ↑t i
by_cases hi : i ∈ s
no goals
case pos
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i
exact h.2 hi
case neg
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
case neg
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 (not_mem_mono ht hi)]
no goals
case neg
ι : 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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
exact zero_mem_zero
no goals
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)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ support f
H : ↑t i = 0
⊢ ↑f i = 0
rwa [H, mem_zero] at h