awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure U)
have rw : IsOpen.{u_1} (X := X) (closure ((⇑e.symm : (a : Y) → X) '' U))
Tactic: rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have obtain : ∀ (U V : Set X) (hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V),
  ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Tactic: obtain ⟨U, V, hUV⟩ := T2Space.t2 hxy
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
have refine : y ∈ (closure U)ᶜ
Tactic: refine ⟨closure U, (closure U)ᶜ, ExtremallyDisconnected.open_closure U hUV.1,
      by simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_,
      by simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ y ∈ (closure U)ᶜ
have rw : ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
Tactic: rw [Set.mem_compl_iff, mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ¬∀ (o : Set X), IsOpen o → y ∈ o → (o ∩ U).Nonempty
have push : ∃ (o : Set X), IsOpen o ∧ y ∈ o ∧ o ∩ U = ∅
Tactic: push Not
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ ∃ (o : Set X), IsOpen o ∧ y ∈ o ∧ o ∩ U = ∅
have refine : V ∩ U = ∅
Tactic: refine ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
inst_2 : T2Space X
x : X
h : Membership.mem (γ := Set X) univ x
y : X
h_1 : Membership.mem (γ := Set X) univ y
hxy : x ≠ y
U V : Set X
hUV : IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V
⊢ V ∩ U = ∅
have rw : Disjoint U V
Tactic: rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f
have hs : g ∘ s = id
Tactic: have hs : g ∘ s = id := funext fun z => Classical.choose_spec (g_sur z)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f
have ht : Continuous t
Tactic: have ht : Continuous t := continuous_of_discreteTopology
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f
have hh : Continuous h
Tactic: have hh : Continuous h := continuous_stoneCechExtend ht
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ ∃ (h : StoneCech X → Y), Continuous h ∧ g ∘ h = f
have refine : (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
Tactic: refine ⟨h, hh, denseRange_stoneCechUnit.equalizer (hg.comp hh) hf ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
have rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
Tactic: rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
have rw₁ : g ∘ t = f ∘ stoneCechUnit
Tactic: rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₁ : g ∘ t = f ∘ stoneCechUnit
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
have rw₂ : (g ∘ s) ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
Tactic: rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₁ : g ∘ t = f ∘ stoneCechUnit
rw₂ : (g ∘ s) ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
have rw₃ : id ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
Tactic: rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
Y Z : Type u
_tsY : TopologicalSpace Y
_tsZ : TopologicalSpace Z
_csY : CompactSpace Y
_t2Y : T2Space Y
_csZ_1 : CompactSpace Z
_csZ : T2Space Z
f : StoneCech X → Z
g : Y → Z
hf : Continuous f
hg : Continuous g
g_sur : Surjective g
s : Z → Y := fun (z : Z) ↦ Classical.choose (p := fun (x : Y) ↦ g x = z) ⋯
hs : g ∘ s = id
t : X → Y := s ∘ f ∘ stoneCechUnit
ht : Continuous t
h : StoneCech X → Y := stoneCechExtend ht
hh : Continuous h
rw : g ∘ h ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₁ : g ∘ t = f ∘ stoneCechUnit
rw₂ : (g ∘ s) ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
rw₃ : id ∘ f ∘ stoneCechUnit = f ∘ stoneCechUnit
⊢ (g ∘ h) ∘ stoneCechUnit = f ∘ stoneCechUnit
have rw₄ : f ∘ stoneCechUnit = f ∘ stoneCechUnit
Tactic: rw [comp_assoc, stoneCechExtend_extends ht, ← comp_assoc, hs, id_comp]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
⊢ ExtremallyDisconnected X
have refine : ∀ (U : Set X) (hU : IsOpen U), IsOpen (closure U)
Tactic: refine { open_closure := fun U hU => ?_ }
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
⊢ IsOpen (closure U)
have hZ₁₂ : Disjoint Z₁ Z₂
Tactic: have hZ₁₂ : Disjoint Z₁ Z₂ := disjoint_left.2 fun x hx₁ hx₂ => by cases hx₁.2.symm.trans hx₂.2
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
⊢ IsOpen (closure U)
have hZ₁ : IsClosed Z₁
Tactic: have hZ₁ : IsClosed Z₁ := hU.isClosed_compl.prod (T1Space.t1 _)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
⊢ IsOpen (closure U)
have hZ₂ : IsClosed Z₂
Tactic: have hZ₂ : IsClosed Z₂ := isClosed_closure.prod (T1Space.t1 false)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
⊢ IsOpen (closure U)
have hZ : IsClosed Z
Tactic: have hZ : IsClosed Z := hZ₁.union hZ₂
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
⊢ IsOpen (closure U)
have f_cont : Continuous f
Tactic: have f_cont : Continuous f := continuous_fst.comp continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
x : X
⊢ ∃ (a : (↑Z : Type u)), f a = x
have pos : ∀ (hx : x ∈ U), ∃ (a : (↑Z : Type u)), f a = x
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
x : X
pos : ∀ (hx : x ∈ U), ∃ (a : (↑Z : Type u)), f a = x
⊢ ∃ (a : (↑Z : Type u)), f a = x
have neg : ∀ (hx : x ∉ U), ∃ (a : (↑Z : Type u)), f a = x
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
⊢ IsOpen (closure U)
have f_sur : Surjective f
Tactic: have f_sur : Surjective f := by
    intro x
    by_cases hx : x ∈ U
    · exact ⟨⟨(x, false), Or.inr ⟨subset_closure hx, mem_singleton _⟩⟩, rfl⟩
    · exact ⟨⟨(x, true), Or.inl ⟨hx, mem_singleton _⟩⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
⊢ IsOpen (closure U)
have this : CompactSpace.{u} (↑Z : Type u)
Tactic: haveI : CompactSpace Z := isCompact_iff_compactSpace.mp hZ.isCompact
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
⊢ IsOpen (closure U)
have obtain : ∀ (g : X → (↑Z : Type u)) (hg : Continuous g) (g_sec : f ∘ g = id), IsOpen (closure U)
Tactic: obtain ⟨g, hg, g_sec⟩ := h continuous_id f_cont f_sur
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
⊢ IsOpen (closure U)
have hφ : Continuous φ
Tactic: have hφ : Continuous φ := continuous_subtype_val.comp hg
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
⊢ IsOpen (closure U)
have hφ₁ : ∀ (x : X), (φ x).1 = x
Tactic: have hφ₁ : ∀ x, (φ x).1 = x := congr_fun g_sec
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ IsOpen (closure U)
have rw : IsClosed (g ⁻¹' Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z₁ ∪ Z₂) ⁻¹' Z₁)
Tactic: rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
rw : IsClosed (g ⁻¹' Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z₁ ∪ Z₂) ⁻¹' Z₁)
⊢ IsOpen (closure U)
have rw₁ : (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
Tactic: rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
have rw : (Z₁ ∪ Z₂) ∩ ∅ = ∅
Tactic: rw [hZ₁₂.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this_1 : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
this : closure U = φ ⁻¹' Z₂
rw : (Z₁ ∪ Z₂) ∩ ∅ = ∅
⊢ (Z₁ ∪ Z₂) ∩ (Z₁ ∩ Z₂) = ∅
have rw₁ : Eq.{u + 1} (α := Set (X × Bool)) ∅ ∅
Tactic: rw [hZ₁₂.inter_eq, inter_empty]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
h : Projective X
U : Set X
hU : IsOpen U
Z₁ : Set (X × Bool) := SProd.sprod (β := Set Bool) Uᶜ {true}
Z₂ : Set (X × Bool) := SProd.sprod (β := Set Bool) (closure U) {false}
Z : Set (X × Bool) := Z₁ ∪ Z₂
hZ₁₂ : Disjoint Z₁ Z₂
hZ₁ : IsClosed Z₁
hZ₂ : IsClosed Z₂
hZ : IsClosed Z
f : (↑Z : Type u) → X := Prod.fst ∘ Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z)
f_cont : Continuous f
f_sur : Surjective f
this : CompactSpace.{u} (↑Z : Type u)
g : X → (↑Z : Type u)
hg : Continuous g
g_sec : f ∘ g = id
φ : X → X × Bool := Subtype.val (p := fun (x : X × Bool) ↦ x ∈ Z) ∘ g
hφ : Continuous φ
hφ₁ : ∀ (x : X), (φ x).1 = x
⊢ IsOpen (closure U)
have suffices : closure U = φ ⁻¹' Z₂
Tactic: suffices closure U = φ ⁻¹' Z₂ by
    rw [this, preimage_comp, ← isClosed_compl_iff, ← preimage_compl,
      ← preimage_subtype_coe_eq_compl Subset.rfl]
    · exact hZ₁.preimage hφ
    · rw [hZ₁₂.inter_eq, inter_empty]