case h
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' sSup s ↔ b ∈ sSup (image f '' s)
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
⊢ f '' sSup s = sSup (image f '' s)
ext b
case h
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) ↔ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
case h
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ b ∈ f '' sSup s ↔ b ∈ sSup (image f '' s)
simp only [sSup_eq_sUnion, mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
case h.mp
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) → ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b

case h.mpr
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b) → ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b
case h
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) ↔ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
constructor
case h.mp.intro.intro.intro.intro
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = f a
case h.mp
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b) → ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b
rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
no goals
case h.mp.intro.intro.intro.intro
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
a : α
t : Set α
ht₁ : t ∈ s
ht₂ : a ∈ t
⊢ ∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = f a
exact ⟨t, ht₁, a, ht₂, rfl⟩
case h.mpr.intro.intro.intro.intro
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = f a
case h.mpr
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
b : β
⊢ (∃ i, i ∈ s ∧ ∃ x, x ∈ i ∧ f x = b) → ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = b
rintro ⟨t, ht₁, a, ht₂, rfl⟩
no goals
case h.mpr.intro.intro.intro.intro
F : Type ?u.92960
α : Type u_1
β : Type u_2
γ : Type ?u.92969
δ : Type ?u.92972
ι : Sort ?u.92975
κ : ι → Sort ?u.92980
f : α → β
s : Set (Set α)
t : Set α
ht₁ : t ∈ s
a : α
ht₂ : a ∈ t
⊢ ∃ x, (∃ t, t ∈ s ∧ x ∈ t) ∧ f x = f a
exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩