-- Mathlib/Topology/QuasiSeparated.lean
theorem IsQuasiSeparated.image_of_isEmbedding {s : Set α} (H : IsQuasiSeparated s)
    (h : IsEmbedding f) : IsQuasiSeparated (f '' s)

Proof state:
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s

Tactic:
exact hU hx

Result:
no goals

Proof state:
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

Tactic:
rw [h.isCompact_iff]

Result:
case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' U))

Proof state:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s

Tactic:
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]

Result:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s

Proof state:
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ x ∈ s

Tactic:
rw [← h.injective.injOn.mem_image_iff (Set.subset_univ _) trivial]

Result:
case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' U
⊢ f x ∈ f '' s

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ⊆ range f

Tactic:
exact hU.trans (Set.image_subset_range _ _)

Result:
no goals

Proof state:
case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f '' (f ⁻¹' V))

Tactic:
convert hV''

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' V) = V

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)

Tactic:
symm

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f '' (f ⁻¹' U ∩ f ⁻¹' V) = U ∩ V

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
convert
  (H (f ⁻¹' U) (f ⁻¹' V)
    ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image h.continuous

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)

case convert_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' U ⊆ s

case convert_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' U)

case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

case convert_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (f ⁻¹' V)

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ U ∩ V ⊆ range f

Tactic:
exact Set.inter_subset_left.trans (hU.trans (Set.image_subset_range _ _))

Result:
no goals

Proof state:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ f ⁻¹' V ⊆ s

Tactic:
intro x hx

Result:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ x ∈ s

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
⊢ V ⊆ range f

Tactic:
exact hV.trans (Set.image_subset_range _ _)

Result:
no goals

Proof state:
case convert_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen V
hV'' : IsCompact V
x : α
hx : x ∈ f ⁻¹' V
⊢ f x ∈ f '' s

Tactic:
exact hV hx

Result:
no goals