awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ s.carrier = (↑s : Set α)

Tactic:
rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
x : α
rw : IsGenericPoint x (closure {x})
⊢ IsGenericPoint x (closure (closure {x}))

Tactic:
rw [closure_closure]

Premises used: closure_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
x : α
⊢ IsGenericPoint x (closure {x})

Tactic:
isGenericPoint_closure

Premises used: isGenericPoint_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
x : α
⊢ IsGenericPoint x (closure {x})

Tactic:
exact isGenericPoint_closure

Premises used: isGenericPoint_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ LE.le (α := α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
        α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
        α) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }

Tactic:
specializes_iff_closure_subset.trans ?_

Premises used: Iff.trans, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
refine :
  Subset (α := Set α)
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
            α)))
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
            α))) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }
⊢ LE.le (α := α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
        α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
        α) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }

Tactic:
refine specializes_iff_closure_subset.trans ?_

Premises used: Iff.trans, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
simp :
  s ⊆ t ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }
⊢ Subset (α := Set α)
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
            α)))
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
            α))) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }

Tactic:
simp
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ s ⊆ t ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }

Tactic:
rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : T0Space α
x : α
⊢ (↑((OrderIso.symm irreducibleSetEquivPoints : (a : α) → TopologicalSpace.IrreducibleCloseds α) x :
          TopologicalSpace.IrreducibleCloseds α) :
      Set α) =
    closure {x}

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
⊢ IsIrreducible (f '' S)

Tactic:
have hS'' := hS.image f hf.continuous.continuousOn
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
obtain : ∀ (x : β) (hx : IsGenericPoint x (f '' S)), ∃ (x : α), IsGenericPoint x S
⊢ ∃ (x : α), IsGenericPoint x S

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

Premises used: Topology.IsClosedEmbedding.isClosedMap, QuasiSober.sober
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
x : β
hx : IsGenericPoint x (f '' S)
obtain : ∀ (y : α) (hx : IsGenericPoint (f y) (f '' S)), ∃ (x : α), IsGenericPoint x S
⊢ ∃ (x : α), IsGenericPoint x S

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

Premises used: IsGenericPoint.mem, rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
h : IsGenericPoint y S
⊢ ∃ (x : α), IsGenericPoint x S

Tactic:
use y
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
h : f '' closure[inst] {y} = f '' S
⊢ IsGenericPoint y S

Tactic:
apply image_injective.mpr hf.injective

Premises used: Iff.mpr, Set.image_injective, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
h : f '' closure[inst] {y} = closure[inst_1] {f y}
h₁ : closure[inst_1] (f '' {y}) = closure[inst_1] {f y}
h₂ h₃ : Eq (α := Set β) (closure[inst_1] {f y}) (closure[inst_1] {f y})
⊢ f '' closure[inst] {y} = f '' S

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

Premises used: IsGenericPoint.def, Set.image_singleton, Topology.IsClosedEmbedding.closure_image_eq
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
⊢ IsIrreducible (f '' S)

Tactic:
have hS'' := hS.image f hf.continuous.continuousOn
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
obtain : ∀ (x : β) (hx : IsGenericPoint x (closure[inst_1] (f '' S))), ∃ (x : α), IsGenericPoint x S
⊢ ∃ (x : α), IsGenericPoint x S

Tactic:
obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure

Premises used: IsIrreducible.closure, QuasiSober.sober, isClosed_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
x : β
hx : IsGenericPoint x (closure[inst_1] (f '' S))
obtain :
  ∀ (T : Set β) (hT : IsClosed[inst_1] T) (hS : IsIrreducible (f ⁻¹' T)) (hS' : IsClosed[inst] (f ⁻¹' T))
    (hS'' : IsIrreducible (f '' f ⁻¹' T)) (hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))),
    ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
⊢ ∃ (x : α), IsGenericPoint x S

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

Premises used: Topology.IsOpenEmbedding.isInducing, Iff.mp, rfl, Topology.IsInducing.isClosed_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))
⊢ IsIrreducible (T ∩ range f)

Tactic:
rw [image_preimage_eq_inter_range] at hx hS''

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))
hS''₁ : IsIrreducible (T ∩ range f)
⊢ IsGenericPoint x (closure[inst_1] (T ∩ range f))

Tactic:
rw [image_preimage_eq_inter_range] at hx hS''

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
rw : x ∈ closure[inst_1] T
⊢ x ∈ T

Tactic:
rw [← hT.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
⊢ x ∈ closure[inst_1] T

Tactic:
closure_mono inter_subset_left hx.mem

Premises used: Set.inter_subset_left, closure_mono, IsGenericPoint.mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
⊢ x ∈ closure[inst_1] T

Tactic:
exact closure_mono inter_subset_left hx.mem

Premises used: Set.inter_subset_left, closure_mono, IsGenericPoint.mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
⊢ x ∈ T

Tactic:
have hxT : x ∈ T := by
      rw [← hT.closure_eq]
      exact closure_mono inter_subset_left hx.mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
rw : (closure[inst_1] (T ∩ range f) ∩ range f).Nonempty
⊢ x ∈ range f

Tactic:
rw [hx.mem_open_set_iff hf.isOpen_range]

Premises used: Topology.IsOpenEmbedding.isOpen_range, IsGenericPoint.mem_open_set_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
⊢ (closure[inst_1] (T ∩ range f) ∩ range f).Nonempty

Tactic:
Nonempty.mono ?_ hS''.1

Premises used: Set.Nonempty.mono, And.left
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
refine : T ∩ range f ⊆ closure[inst_1] (T ∩ range f) ∩ range f
⊢ (closure[inst_1] (T ∩ range f) ∩ range f).Nonempty

Tactic:
refine Nonempty.mono ?_ hS''.1

Premises used: Set.Nonempty.mono, And.left
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
⊢ T ∩ range f ⊆ closure[inst_1] (T ∩ range f) ∩ range f

Tactic:
simpa using subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
obtain :
  ∀ (y : α) (hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))) (hxT : f y ∈ T),
    ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)

Tactic:
obtain ⟨y, rfl⟩ : x ∈ range f := by
      rw [hx.mem_open_set_iff hf.isOpen_range]
      refine Nonempty.mono ?_ hS''.1
      simpa using subset_closure

Premises used: Set.range, rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
h : IsGenericPoint y (f ⁻¹' T)
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)

Tactic:
use y
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
h : f ⁻¹' closure[inst_1] (T ∩ range f) = f ⁻¹' T
⊢ closure[inst] {y} = f ⁻¹' T

Tactic:
rw [hf.isEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]

Premises used: Set.image_singleton, Topology.IsOpenEmbedding.isEmbedding, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
h : f '' f ⁻¹' closure[inst_1] (T ∩ range f) = f '' f ⁻¹' T
⊢ f ⁻¹' closure[inst_1] (T ∩ range f) = f ⁻¹' T

Tactic:
apply image_injective.mpr hf.injective

Premises used: Iff.mpr, Set.image_injective, Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
h : ∀ (z : β), z ∈ f '' f ⁻¹' closure[inst_1] (T ∩ range f) ↔ z ∈ f '' f ⁻¹' T
⊢ f '' f ⁻¹' closure[inst_1] (T ∩ range f) = f '' f ⁻¹' T

Tactic:
ext z
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
z : β
h : z ∈ range f → (z ∈ closure[inst_1] (T ∩ range f) ↔ z ∈ T)
⊢ z ∈ f '' f ⁻¹' closure[inst_1] (T ∩ range f) ↔ z ∈ f '' f ⁻¹' T

Tactic:
simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]

Premises used: Set.mem_inter_iff, Set.image_preimage_eq_inter_range, and_congr_left_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ range f → (z ∈ closure[inst_1] (T ∩ range f) ↔ z ∈ T)

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

Premises used: subset_closure, IsClosed.closure_eq, Eq.rec, Set.inter_subset_left, closure_mono, And.intro, Iff.intro
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ range f → (z ∈ closure[inst_1] (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⟩⟩
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober.{u_1} ↥(U i)

Tactic:
⟨fun h i ↦ (U i).isOpenEmbedding'.quasiSober, fun hU' ↦ (quasiSober_iff _).mpr ?_⟩

Premises used: quasiSober_iff, Iff.mpr, Topology.IsOpenEmbedding.quasiSober, TopologicalSpace.Opens.isOpenEmbedding', Iff.intro
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
refine :
  ∀ (hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)) {S : Set α}, IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober.{u_1} ↥(U i)

Tactic:
refine ⟨fun h i ↦ (U i).isOpenEmbedding'.quasiSober, fun hU' ↦ (quasiSober_iff _).mpr ?_⟩
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (x : α), IsGenericPoint x t
⊢ ∃ (x : α), IsGenericPoint x t

Tactic:
obtain ⟨i, hi⟩ := hU.exists_mem x

Premises used: TopologicalSpace.IsOpenCover.exists_mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
⊢ IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)

Tactic:
have H : IsIrreducible ((↑) ⁻¹' t : Set (U i)) :=
      ⟨⟨⟨x, hi⟩, hx⟩, h.preimage (U i).isOpenEmbedding'⟩