-- Mathlib/Topology/Sober.lean
lemma Topology.IsClosedEmbedding.quasiSober {f : α → β} (hf : IsClosedEmbedding f) [QuasiSober β] :
    QuasiSober α where
  sober hS hS'

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ IsGenericPoint y S✝

Tactic:
apply image_injective.mpr hf.injective

Result:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ f '' closure {y} = f '' S✝

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
obtain ⟨x, hx⟩ := QuasiSober.sober hS'' (hf.isClosedMap _ hS')

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
x : β
hx : IsGenericPoint x (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
x : β
hx : IsGenericPoint x (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
obtain ⟨y, -, rfl⟩ := hx.mem

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Proof state:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ f '' closure {y} = f '' S✝

Tactic:
rw [← hx.def, ← hf.closure_image_eq, image_singleton]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
have hS'' := hS.image f hf.continuous.continuousOn

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
use y

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
y : α
hx : IsGenericPoint (f y) (f '' S✝)
⊢ IsGenericPoint y S✝