case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t

case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
apply Subset.antisymm
no goals
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t
calc
  f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ f '' (f ⁻¹' t) := image_inter_subset _ _ _
  _ ⊆ f '' s ∩ t := inter_subset_inter_right _ (image_preimage_subset f t)
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
x : α
h' : x ∈ s
h : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)
rintro _ ⟨⟨x, h', rfl⟩, h⟩
no goals
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.51943
ι : Sort ?u.51946
ι' : Sort ?u.51949
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
x : α
h' : x ∈ s
h : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
exact ⟨x, ⟨h', h⟩, rfl⟩