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