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

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding 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 : IsOpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed S✝
hS'' : IsIrreducible (f '' S✝)
⊢ ∃ x, IsGenericPoint x S✝

Proof state:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ f '' (f ⁻¹' closure (T ∩ range f)) = f '' (f ⁻¹' T)

Tactic:
ext z

Result:
case h.a.h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ f '' (f ⁻¹' closure (T ∩ range f)) ↔ z ∈ f '' (f ⁻¹' T)

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Tactic:
have hxT : x ∈ T := by
  rw [← hT.closure_eq]
  exact closure_mono inter_subset_left hx.mem

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ IsGenericPoint y (f ⁻¹' T)

Tactic:
change _ = _

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ closure {y} = f ⁻¹' T

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ ∃ x, IsGenericPoint x (f ⁻¹' T)

Tactic:
use y

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ IsGenericPoint y (f ⁻¹' T)

Proof state:
case h.a.h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ range f → (z ∈ closure (T ∩ range f) ↔ z ∈ T)

Tactic:
exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono inter_subset_left h,
  fun h => subset_closure ⟨h, hy⟩⟩

Result:
no goals

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

Tactic:
obtain ⟨T, hT, rfl⟩ := hf.isInducing.isClosed_iff.mp hS'

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

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ f ⁻¹' closure (T ∩ range f) = f ⁻¹' T

Tactic:
apply image_injective.mpr hf.injective

Result:
case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure (T ∩ range f))
hxT : f y ∈ T
⊢ f '' (f ⁻¹' closure (T ∩ range f)) = f '' (f ⁻¹' T)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f

Tactic:
rw [hx.mem_open_set_iff hf.isOpen_range]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ (closure (T ∩ range f) ∩ range f).Nonempty

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
hxT : x ∈ T
⊢ T ∩ range f ⊆ closure (T ∩ range f) ∩ range f

Tactic:
simpa using subset_closure

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure (T ∩ range f))
⊢ x ∈ closure T

Tactic:
exact closure_mono inter_subset_left hx.mem

Result:
no goals