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,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f) →
    support f ⊆ s ∧ ∀ (i : ι), 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)
⊢ (support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f
ι : 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 ∈ dfinsupp s t ↔ support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
refine' mem_map.trans ⟨_, _⟩
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 → (fun i => α i) a
hf : f ∈ pi s t
⊢ support
        (↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          f) ⊆
      s ∧
    ∀ (i : ι),
      i ∈ s →
        ↑(↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                    inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑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)
⊢ (∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f) →
    support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
rintro ⟨f, hf, rfl⟩
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 → (fun i => α i) a
hf : f ∈ pi s t
⊢ support (Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
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 → (fun i => α i) a
hf : f ∈ pi s t
⊢ support
        (↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          f) ⊆
      s ∧
    ∀ (i : ι),
      i ∈ s →
        ↑(↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                    inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
                f)
            i ∈
          t i
rw [Function.Embedding.coeFn_mk]
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 → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
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 → (fun i => α i) a
hf : f ∈ pi s t
⊢ support (Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
refine' ⟨support_mk_subset, fun i hi => _⟩
case h.e'_4
ι : 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 → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i = f i hi
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 → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
convert mem_pi.1 hf i hi
no goals
case h.e'_4
ι : 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 → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i = f i hi
exact mk_of_mem hi
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 : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
          inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
      fun i x => ↑f i) =
    f
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)
⊢ (support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
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 : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          fun i x => ↑f i)
      i =
    ↑f 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)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
          inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
      fun i x => ↑f i) =
    f
ext i
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 : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ (if i ∈ s then ↑f i else 0) = ↑f i
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 : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := fun f => Dfinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (Dfinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          fun i x => ↑f i)
      i =
    ↑f i
dsimp
no goals
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 : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ (if i ∈ s then ↑f i else 0) = ↑f i
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm