awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hφx' : ∀ (x : E) (hx : x ∈ X), QuasiconcaveOn.{0, u_2, u_5} ℝ (β := γ) Y fun (y : F) ↦ φ x y
Tactic: have hφx' (x) (hx : x ∈ X) : QuasiconcaveOn ℝ Y fun y ↦ φ x y := by
    convert! (hfx' x hx).monotone_comp ι.monotone
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hφy : ∀ (y : F) (hy : y ∈ Y), LowerSemicontinuousOn.{u_1, u_5} (β := γ) (fun (x : E) ↦ φ x y) X
Tactic: have hφy (y) (hy : y ∈ Y) : LowerSemicontinuousOn (fun x ↦ φ x y) X := by
    convert! Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone
-- Lean 4 proof step from Mathlib.Topology.Sion (hypothesis)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have hφy' : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Sion (goal)
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
have right : IsSaddlePointOn X Y f a b
Tactic: use a, ha, b, hb
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
Goal:
X : Type
inst : TopologicalSpace X
⊢ HasSmallInductiveDimensionLT X 1 ↔ IsTopologicalBasis (α := X) {s : Set X | IsClopen s}
have mp : HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis (α := X) {s : Set X | IsClopen s}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
Goal:
X : Type
inst : TopologicalSpace X
mp : HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis (α := X) {s : Set X | IsClopen s}
⊢ HasSmallInductiveDimensionLT X 1 ↔ IsTopologicalBasis (α := X) {s : Set X | IsClopen s}
have mpr : IsTopologicalBasis (α := X) {s : Set X | IsClopen s} → HasSmallInductiveDimensionLT X 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
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}
have mp : ∀ (U : Set X) (hU : U ∈ s), IsClosed U
Tactic: refine hs.of_isOpen_of_subset (fun _ hU ↦ hU.isOpen) (fun U hU ↦ ⟨?_, hs.isOpen hU⟩)
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
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
⊢ IsClosed U
have mp : closure U ⊆ U
Tactic: rw [← closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (hypothesis)
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
⊢ closure U ⊆ U
have inst : IsEmpty (↑(frontier U) : Type)
Tactic: cases h U hU
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
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)
⊢ closure U ⊆ U
have mp : frontier U = ∅ → closure U ⊆ U
Tactic: rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, diff_eq_empty] at ‹_›
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
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
⊢ closure U ⊆ U
have mp₁ : closure U \ U = ∅ → closure U ⊆ U
Tactic: rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, diff_eq_empty] at ‹_›
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.Topology.SmallInductiveDimension (goal)
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
⊢ closure U ⊆ U
have mp₂ : closure U ⊆ U → closure U ⊆ U
Tactic: rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, diff_eq_empty] at ‹_›
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ x ∉ U
have rw : Disjoint S U ↔ ¬(S ∩ U).Nonempty
Tactic: rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
rw : Disjoint S U ↔ ¬(S ∩ U).Nonempty
⊢ Disjoint S U ↔ x ∉ U
have rw₁ : Disjoint S U ↔ ¬¬Disjoint S U
Tactic: rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ Disjoint S U ↔ x ∉ U
have rw₂ : Disjoint S U ↔ Disjoint S U
Tactic: rw [h.mem_open_set_iff hU, ← not_disjoint_iff_nonempty_inter, Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ S ⊆ Z
have rw : x ∈ Z ↔ closure {x} ⊆ Z
Tactic: rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
rw : x ∈ Z ↔ closure {x} ⊆ Z
⊢ x ∈ Z ↔ S ⊆ Z
have rw₁ : x ∈ Z ↔ {x} ⊆ Z
Tactic: rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ x ∈ Z ↔ S ⊆ Z
have rw₂ : x ∈ Z ↔ x ∈ Z
Tactic: rw [← h.def, hZ.closure_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))
have rw : closure {f x} = closure (f '' S)
Tactic: rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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)
⊢ IsGenericPoint (f x) (closure (f '' S))
have rw₁ : closure {f x} = closure (f '' closure {x})
Tactic: rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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})
⊢ IsGenericPoint (f x) (closure (f '' S))
have rw₂ : closure (f '' {x}) = closure (f '' closure {x})
Tactic: rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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})
⊢ IsGenericPoint (f x) (closure (f '' S))
have rw₃ : closure (f '' {x}) = closure (f '' {x})
Tactic: rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have this : closure {x} ⊆ S
Tactic: have : closure {x} ⊆ S := closure_minimal (singleton_subset_iff.2 hxS) hS
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw : closure {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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₁ : closure {x} ⊆ S ∧ S ⊆ closure {x} ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₂ : True ∧ S ⊆ closure {x} ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₃ : S ⊆ closure {x} ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₄ : S ⊆ ⋂₀ {t : Set α | IsClosed t ∧ {x} ⊆ t} ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have 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
Tactic: simp_rw [IsGenericPoint, subset_antisymm_iff, this, true_and, closure, subset_sInter_iff,
    mem_setOf_eq, and_imp, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₆ : (∀ (t' : Set α), IsClosed t' ∧ {x} ⊆ t' → S ⊆ t') ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
have simp_rw₇ : (∀ (t' : Set α), IsClosed t' → {x} ⊆ t' → S ⊆ t') ↔ ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint (hS.genericPoint (S := S)) S
have h : S = closure S
Tactic: convert! hS.isGenericPoint_genericPoint_closure
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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
have refine : (↑((fun (x : α) ↦
          ({ carrier := closure {x}, isIrreducible' := sorry, isClosed' := sorry } : TopologicalSpace.IrreducibleCloseds α))
        ((fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ sorry.genericPoint (S := s.carrier)) s)) :
    Set α) =
  (↑s : Set α)
Tactic: refine TopologicalSpace.IrreducibleCloseds.ext ?_
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
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)) :
      Set α) =
    (↑s : Set α)
have simp : s.carrier = (↑s : Set α)
Tactic: simp only [IsIrreducible.genericPoint_closure_eq, TopologicalSpace.IrreducibleCloseds.coe_mk,
      closure_eq_iff_isClosed.mpr s.3]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
x : α
⊢ IsGenericPoint x (closure (closure {x}))
have rw : IsGenericPoint x (closure {x})
Tactic: rw [closure_closure]