α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.254718
ι₂ : Sort ?u.254721
κ : ι → Sort u_5
κ₁ : ι → Sort ?u.254731
κ₂ : ι → Sort ?u.254736
κ' : ι' → Sort ?u.254741
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ (x : α),
    x ∈ s → ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.254718
ι₂ : Sort ?u.254721
κ : ι → Sort u_5
κ₁ : ι → Sort ?u.254731
κ₂ : ι → Sort ?u.254736
κ' : ι' → Sort ?u.254741
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), image2 f s (t i j)
simp_rw [image2_subset_iff, mem_iInter]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort ?u.254718
ι₂ : Sort ?u.254721
κ : ι → Sort u_5
κ₁ : ι → Sort ?u.254731
κ₂ : ι → Sort ?u.254736
κ' : ι' → Sort ?u.254741
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ (x : α),
    x ∈ s → ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)