awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
y : F
hy : y ∈ Y
⊢ QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X fun (x : E) ↦ φ x y

Tactic:
convert! (hfy' y hy).monotone_comp ι.monotone

Premises used: OrderEmbedding.monotone, QuasiconvexOn.monotone_comp
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
⊢ ∀ (y : F) (hy : y ∈ Y), QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X fun (x : E) ↦ φ x y

Tactic:
have hφy' (y) (hy : y ∈ Y) : QuasiconvexOn ℝ X fun x ↦ φ x y := by
    convert! (hfy' y hy).monotone_comp ι.monotone
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
hφy' : ∀ (y : F) (hy : y ∈ Y), QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X fun (x : E) ↦ φ x y
obtain :
  ∀ (a : E) (ha : a ∈ X) (b : F) (hb : b ∈ Y) (hab : IsSaddlePointOn X Y φ a b),
    ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
obtain ⟨a, ha, b, hb, hab⟩ :=
    exists_isSaddlePointOn' ne_X kX hφy hφy' cY kY hφx hφx' cX ne_Y

Premises used: Sion.exists_isSaddlePointOn'
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
hφy' : ∀ (y : F) (hy : y ∈ Y), QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X fun (x : E) ↦ φ x y
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
hab : IsSaddlePointOn X Y φ a b
right : IsSaddlePointOn X Y f a b
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
use a, ha, b, hb
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
inst : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn.{u_1, u_3} (β := β) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn.{0, u_1, u_3} ℝ (β := β) X fun (x : E) ↦ f x y
inst_6 : TopologicalSpace F
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : IsTopologicalAddGroup F
inst_10 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn.{u_2, u_3} (β := β) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn.{0, u_2, u_3} ℝ (β := β) Y fun (y : F) ↦ f x y
inst_11 : TopologicalSpace β
inst_12 : OrderTopology β
γ : Type u_5
inst_13 : CompleteLinearOrder γ
inst_14 : DenselyOrdered γ
inst_15 : TopologicalSpace γ
inst_16 : OrderTopology γ
ι : β ↪o γ
hι : Continuous.{u_3, u_5} (X := β) (Y := γ) (⇑ι : (a : β) → γ)
φ : E → F → γ := fun (x : E) (y : F) ↦ (ι : (a : β) → γ) (f x y)
hφx : ∀ (x : E) (hx : x ∈ X), UpperSemicontinuousOn.{u_2, u_5} (β := γ) (fun (y : F) ↦ φ x y) Y
hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
hφy' : ∀ (y : F) (hy : y ∈ Y), QuasiconvexOn.{0, u_1, u_5} ℝ (β := γ) X fun (x : E) ↦ φ x y
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
hab : IsSaddlePointOn X Y φ a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b

Tactic:
simpa only [OrderEmbedding.le_iff_le, φ] using hab x hx y hy

Premises used: OrderEmbedding.le_iff_le
-- Module: Mathlib.Topology.Sion
Goal:
E : Type u_1
F : Type u_2
X : Set E
Y : Set F
f : E → F → ℝ
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ne_X : X.Nonempty
cX : Convex ℝ X
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (β := ℝ) (fun (x : E) ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ (β := ℝ) X fun (x : E) ↦ f x y
inst_5 : TopologicalSpace F
inst_6 : AddCommGroup F
inst_7 : Module ℝ F
inst_8 : IsTopologicalAddGroup F
inst_9 : ContinuousSMul ℝ F
cY : Convex ℝ Y
ne_Y : Y.Nonempty
kY : IsCompact Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (β := ℝ) (fun (y : F) ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ (β := ℝ) Y fun (y : F) ↦ f x y
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

Tactic:
DMCompletion.exists_isSaddlePointOn ne_X cX kX hfy hfy' cY ne_Y kY hfx hfx'
    (ι := EReal.orderEmbedding) (hι := continuous_coe_real_ereal)

Premises used: Sion.DMCompletion.exists_isSaddlePointOn, continuous_coe_real_ereal
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
h : HasSmallInductiveDimensionLT X 0
⊢ IsEmpty X

Tactic:
cases h
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
inst_1 : IsEmpty X
⊢ IsEmpty X

Tactic:
assumption
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
mp : HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis (α := X) {s : Set X | IsClopen s}
mpr : IsTopologicalBasis (α := X) {s : Set X | IsClopen s} → HasSmallInductiveDimensionLT X 1
⊢ HasSmallInductiveDimensionLT X 1 ↔ IsTopologicalBasis (α := X) {s : Set X | IsClopen s}

Tactic:
constructor
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U) : Type) 0
⊢ IsTopologicalBasis (α := X) {s : Set X | IsClopen s}

Tactic:
hs.of_isOpen_of_subset (fun _ hU ↦ hU.isOpen) (fun U hU ↦ ⟨?_, hs.isOpen hU⟩)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset, IsClopen.isOpen, And.intro
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U) : Type) 0
mp : ∀ (U : Set X) (hU : U ∈ s), IsClosed U
⊢ IsTopologicalBasis (α := X) {s : Set X | IsClopen s}

Tactic:
refine hs.of_isOpen_of_subset (fun _ hU ↦ hU.isOpen) (fun U hU ↦ ⟨?_, hs.isOpen hU⟩)
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U) : Type) 0
U : Set X
hU : U ∈ s
mp : closure U ⊆ U
⊢ IsClosed U

Tactic:
rw [← closure_subset_iff_isClosed]

Premises used: closure_subset_iff_isClosed
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U) : Type) 0
U : Set X
hU : U ∈ s
⊢ IsEmpty (↑(frontier U) : Type)

Tactic:
cases h U hU
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
s : Set (Set X)
hs : IsTopologicalBasis s
h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U) : Type) 0
U : Set X
hU : U ∈ s
inst_1 rwa : IsEmpty (↑(frontier U) : Type)
mp : frontier U = ∅ → closure U ⊆ U
mp₁ : closure U \ U = ∅ → closure U ⊆ U
mp₂ mp₃ mp₄ mp₅ : closure U ⊆ U → closure U ⊆ U
⊢ closure U ⊆ U

Tactic:
rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, diff_eq_empty] at ‹_›

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, Set.isEmpty_coe_sort, IsOpen.frontier_eq, Set.diff_eq_empty
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
⊢ IsTopologicalBasis (α := X) {s : Set X | IsClopen s} → HasSmallInductiveDimensionLT X 1

Tactic:
fun h ↦ .succ 0 _ h fun _ hU ↦ hU.frontier_eq ▸ .zero

Premises used: HasSmallInductiveDimensionLT.succ, setOf, Eq.rec, HasSmallInductiveDimensionLT.zero, IsClopen, OfNat.ofNat, Eq.symm, IsClopen.frontier_eq
-- Module: Mathlib.Topology.SmallInductiveDimension
Goal:
X : Type
inst : TopologicalSpace X
⊢ IsTopologicalBasis (α := X) {s : Set X | IsClopen s} → HasSmallInductiveDimensionLT X 1

Tactic:
exact fun h ↦ .succ 0 _ h fun _ hU ↦ hU.frontier_eq ▸ .zero
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
⊢ IsGenericPoint x S ↔ closure {x} = S

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsGenericPoint
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
h : IsGenericPoint x S
⊢ closure {x} = S

Tactic:
h

Premises used: IsGenericPoint
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
⊢ IsGenericPoint x (closure {x})

Tactic:
refl _

Premises used: IsGenericPoint, refl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S

Tactic:
simp only [specializes_iff_mem_closure, IsGenericPoint, Set.ext_iff]

Premises used: IsGenericPoint, specializes_iff_mem_closure, Set.ext_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
S : Set α
h : IsGenericPoint x S
⊢ x ⤳ y ↔ y ∈ S

Tactic:
isGenericPoint_iff_specializes.1 h y

Premises used: isGenericPoint_iff_specializes, Iff.mp
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
S : Set α
h : IsGenericPoint x S
h' : y ∈ S
⊢ x ⤳ y

Tactic:
h.specializes_iff_mem.2 h'

Premises used: Iff.mpr, IsGenericPoint.specializes_iff_mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
h : IsGenericPoint x S
⊢ x ∈ S

Tactic:
h.specializes_iff_mem.1 specializes_rfl

Premises used: IsGenericPoint.specializes_iff_mem, specializes_rfl, Iff.mp
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
h : IsGenericPoint x S
⊢ IsClosed S

Tactic:
h.def ▸ isClosed_closure

Premises used: IsGenericPoint.def, Eq.rec, isClosed_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
h : IsGenericPoint x S
⊢ IsIrreducible S

Tactic:
h.def ▸ isIrreducible_singleton.closure

Premises used: IsGenericPoint.def, Eq.rec, isIrreducible_singleton, IsIrreducible.closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
S : Set α
h : IsGenericPoint x S
h' : IsGenericPoint y S
⊢ Inseparable x y

Tactic:
(h.specializes h'.mem).antisymm (h'.specializes h.mem)

Premises used: IsGenericPoint.specializes, Specializes.antisymm, IsGenericPoint.mem
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
S : Set α
inst_1 : T0Space α
h : IsGenericPoint x S
h' : IsGenericPoint y S
⊢ x = y

Tactic:
(h.inseparable h').eq

Premises used: IsGenericPoint.inseparable, Inseparable.eq
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ x ∈ U ↔ (S ∩ U).Nonempty

Tactic:
⟨fun h' => ⟨x, h.mem, h'⟩, fun ⟨_y, hyS, hyU⟩ => (h.specializes hyS).mem_open hU hyU⟩

Premises used: IsGenericPoint.specializes, Specializes.mem_open, Membership.mem, And.intro, Iff.intro, Exists.intro, IsGenericPoint.mem, _private.0.IsGenericPoint.mem_open_set_iff.match_1
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
rw : Disjoint S U ↔ ¬(S ∩ U).Nonempty
rw₁ : Disjoint S U ↔ ¬¬Disjoint S U
rw₂ rw₃ : Disjoint S U ↔ Disjoint S U
⊢ Disjoint S U ↔ x ∉ U

Tactic:
rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]

Premises used: Classical.not_not, Set.not_disjoint_iff_nonempty_inter, IsGenericPoint.mem_open_set_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
rw : x ∈ Z ↔ closure {x} ⊆ Z
rw₁ : x ∈ Z ↔ {x} ⊆ Z
rw₂ rw₃ : x ∈ Z ↔ x ∈ Z
⊢ x ∈ Z ↔ S ⊆ Z

Tactic:
rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, IsGenericPoint.def, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
rw : closure {f x} = closure (f '' S)
rw₁ : closure {f x} = closure (f '' closure {x})
rw₂ : closure (f '' {x}) = closure (f '' closure {x})
rw₃ rw₄ : closure (f '' {x}) = closure (f '' {x})
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]

Premises used: IsGenericPoint.def, Set.image_singleton, closure_image_closure, isGenericPoint_def
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ closure {x} ⊆ S

Tactic:
have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
simp_rw : closure {x} = S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₁ : closure {x} ⊆ S ∧ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₂ : True ∧ S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₃ : S ⊆ closure {x} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₄ : S ⊆ ⋂₀ {t : Set α | IsClosed t ∧ {x} ⊆ t} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₅ :
  (∀ (t' : Set α), Membership.mem (γ := Set (Set α)) {t : Set α | IsClosed t ∧ {x} ⊆ t} t' → S ⊆ t') ↔
    ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₆ : (∀ (t' : Set α), IsClosed t' ∧ {x} ⊆ t' → S ⊆ t') ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
simp_rw₇ : (∀ (t' : Set α), IsClosed t' → {x} ⊆ t' → S ⊆ t') ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and, closure, subset_sInter_iff,
    mem_setOf_eq, and_imp, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, and_imp, IsGenericPoint, Set.mem_setOf_eq, closure, subset_antisymm_iff, Set.subset_sInter_iff, true_and
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
⊢ IsGenericPoint (hS.genericPoint (S := S)) (closure S)

Tactic:
(QuasiSober.sober hS.closure isClosed_closure).choose_spec

Premises used: Exists.choose_spec, IsIrreducible.genericPoint, IsIrreducible.closure, QuasiSober.sober, isClosed_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint (hS.genericPoint (S := S)) (closure S)

Tactic:
hS.isGenericPoint_genericPoint_closure

Premises used: IsIrreducible.isGenericPoint_genericPoint_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
h : S = closure S
⊢ IsGenericPoint (hS.genericPoint (S := S)) S

Tactic:
convert! hS.isGenericPoint_genericPoint_closure

Premises used: IsIrreducible.isGenericPoint_genericPoint_closure
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ S = closure S

Tactic:
hS'.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ S = closure S

Tactic:
exact hS'.closure_eq.symm

Premises used: IsClosed.closure_eq, Eq.symm
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
⊢ closure {hS.genericPoint (S := S)} = closure S

Tactic:
hS.isGenericPoint_genericPoint_closure

Premises used: IsIrreducible.isGenericPoint_genericPoint_closure, IsGenericPoint
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ closure {hS.genericPoint (S := S)} = S

Tactic:
hS.isGenericPoint_genericPoint_closure.trans hS'.closure_eq

Premises used: IsIrreducible.isGenericPoint_genericPoint_closure, IsClosed.closure_eq, Eq.trans
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) univ

Tactic:
simpa using (IrreducibleSpace.isIrreducible_univ α).isGenericPoint_genericPoint_closure

Premises used: IsIrreducible.isGenericPoint_genericPoint_closure, IrreducibleSpace.isIrreducible_univ
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
⊢ Eq (α := Set α) (closure {genericPoint α}) univ

Tactic:
genericPoint_spec α

Premises used: IsGenericPoint, genericPoint_spec
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
x : α
⊢ Membership.mem (γ := Set α) (closure univ) x

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 : TopologicalSpace.IrreducibleCloseds α
⊢ (fun (x : α) ↦
        ({ carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ } : TopologicalSpace.IrreducibleCloseds α))
      ((fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier)) s) =
    s

Tactic:
TopologicalSpace.IrreducibleCloseds.ext ?_

Premises used: TopologicalSpace.IrreducibleCloseds.ext
-- 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 α
refine :
  (↑((fun (x : α) ↦
            ({ carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ } : TopologicalSpace.IrreducibleCloseds α))
          ((fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier)) s)) :
      Set α) =
    (↑s : Set α)
⊢ (fun (x : α) ↦
        ({ carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ } : TopologicalSpace.IrreducibleCloseds α))
      ((fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier)) s) =
    s

Tactic:
refine TopologicalSpace.IrreducibleCloseds.ext ?_

Premises used: TopologicalSpace.IrreducibleCloseds.ext
-- 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 α
simp : s.carrier = (↑s : Set α)
⊢ (↑((fun (x : α) ↦
            ({ carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ } : TopologicalSpace.IrreducibleCloseds α))
          ((fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier)) s)) :
      Set α) =
    (↑s : Set α)

Tactic:
simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
      closure_eq_iff_isClosed.mpr s.3]

Premises used: Iff.mpr, IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk, closure_eq_iff_isClosed, TopologicalSpace.IrreducibleCloseds.isClosed'