-- Module: Mathlib.Data.Set.Lattice.Image
Goal:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst : γ
snd : δ
h : (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
h₁ : ((∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i) → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂ h₃ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i
h₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₅ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₆ h₇ h₈ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₉ h₁₀ h₁₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₁₂ h₁₃ h₁₄ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₁₅ h₁₆ h₁₇ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₁₈ h₁₉ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ s, fst ∈ f i
h₂₀ h₂₁ : ∀ (w : α) (w_1 : β), w ∈ s → w_1 ∈ t → fst ∈ f w → snd ∈ g w_1 → ∃ i ∈ t, snd ∈ g i
h₂₂ h₂₃ :
  ∀ (w : α) (w_1 : β),
    w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b
h₂₄ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₅ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₆ :
  ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → ∃ (b : β), (w ∈ s ∧ b ∈ t) ∧ fst ∈ f w ∧ snd ∈ g b
h₂₇ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₂₈ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₂₉ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₀ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₁ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → (w ∈ s ∧ w_1 ∈ t) ∧ fst ∈ f w ∧ snd ∈ g w_1
h₃₂ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₃ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₄ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → w ∈ s ∧ w_1 ∈ t
h₃₅ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → fst ∈ f w ∧ snd ∈ g w_1
h₃₆ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₃₇ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₃₈ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → w ∈ s ∧ w_1 ∈ t
h₃₉ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → fst ∈ f w ∧ snd ∈ g w_1
h₄₀ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → β
h₄₁ : (w : α) → (w_1 : β) → w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → α
h₄₂ h₄₃ : ∀ (w : α) (w_1 : β), w ∈ s → fst ∈ f w → w_1 ∈ t → snd ∈ g w_1 → fst ∈ f w ∧ snd ∈ g w_1
⊢ (∃ (a : α) (b : β), (a ∈ s ∧ b ∈ t) ∧ fst ∈ f a ∧ snd ∈ g b) ↔ (∃ i ∈ s, fst ∈ f i) ∧ ∃ i ∈ t, snd ∈ g i

Tactic:
tauto