-- Mathlib/Data/Finset/NAry.lean
theorem subset_set_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
    ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ image2 f s t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rw [← Set.image_prod, subset_set_image_iff] at hu

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ s', ↑s' ⊆ s ×ˢ t ∧ image (fun x => f x.1 x.2) s' = u
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑u ⊆ Prod.fst ⁻¹' s ∧ ↑u ⊆ Prod.snd ⁻¹' t ∧ ∀ x ∈ u, f x.1 x.2 ∈ image₂ (fun a b => f a.1 b.2) u u

Tactic:
exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑(image Prod.fst u) ⊆ s ∧
    ↑(image Prod.snd u) ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)

Tactic:
simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
  image_subset_iff]

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑u ⊆ Prod.fst ⁻¹' s ∧ ↑u ⊆ Prod.snd ⁻¹' t ∧ ∀ x ∈ u, f x.1 x.2 ∈ image₂ (fun a b => f a.1 b.2) u u

Proof state:
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f s' t'

Tactic:
classical
use u.image Prod.fst, u.image Prod.snd
simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
  image_subset_iff]
exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f s' t'

Tactic:
use u.image Prod.fst, u.image Prod.snd

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑(image Prod.fst u) ⊆ s ∧
    ↑(image Prod.snd u) ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ s', ↑s' ⊆ s ×ˢ t ∧ image (fun x => f x.1 x.2) s' = u
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ image (fun x => f x.1 x.2) u ⊆ image₂ f s' t'