awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have X₂_cont : Continuous X₂
Tactic: have X₂_cont : Continuous X₂ := continuous_snd.comp continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
⊢ ∃ (h : A → B), Continuous h ∧ f ∘ h = φ
have refine : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
Tactic: refine ⟨E.restrict X₂ ∘ ρ'.symm, ⟨X₂_cont.continuousOn.restrict.comp ρ'.symm.continuous, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
Tactic: rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have rw₁ : comp (β := (↑E : Type u)) (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
Tactic: rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₁ : comp (β := (↑E : Type u)) (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have rw₂ : φ ∘ comp (β := (↑E : Type u)) (⇑ρ' : (a : (↑E : Type u)) → A) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
Tactic: rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₁ : comp (β := (↑E : Type u)) (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₂ : φ ∘ comp (β := (↑E : Type u)) (⇑ρ' : (a : (↑E : Type u)) → A) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have rw₃ : φ ∘ id = φ
Tactic: rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
this : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
rw : (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₁ : comp (β := (↑E : Type u)) (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₂ : φ ∘ comp (β := (↑E : Type u)) (⇑ρ' : (a : (↑E : Type u)) → A) (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
rw₃ : φ ∘ id = φ
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have rw₄ : φ = φ
Tactic: rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ ∘ (⇑ρ'.symm : (a : A) → (↑E : Type u)) = φ
have suffices : f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
Tactic: suffices f ∘ E.restrict X₂ = φ ∘ ρ' by
    rw [← comp_assoc, this, comp_assoc, Homeomorph.self_comp_symm, comp_id]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
A : Type u
inst : TopologicalSpace A
inst_1 : ExtremallyDisconnected A
inst_2 : CompactSpace A
inst_3 : T2Space A
B C : Type u
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : CompactSpace B
inst_7 : T2Space B
inst_8 : CompactSpace C
inst_9 : T2Space C
φ : A → C
f : B → C
φ_cont : Continuous φ
f_cont : Continuous f
f_surj : Surjective f
D : Set (A × B) := {x : A × B | φ x.1 = f x.2}
D_comp : CompactSpace.{u} (↑D : Type u)
X₁ : (↑D : Type u) → A := Prod.fst ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₁_cont : Continuous X₁
X₁_surj : Surjective X₁
E : Set (↑D : Type u)
left : CompactSpace.{u} (↑E : Type u)
E_onto : X₁ '' E = univ
E_min :
  ∀ (E₀ : Set (↑E : Type u)), E₀ ≠ univ → IsClosed E₀ → E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁ '' E₀ ≠ univ
ρ : (↑E : Type u) → A := E.restrict (π := fun (a : (↑D : Type u)) ↦ A) X₁
ρ_cont : Continuous ρ
ρ_surj : Surjective ρ
ρ' : (↑E : Type u) ≃ₜ A := ExtremallyDisconnected.homeoCompactToT2 ρ_cont ρ_surj E_min
X₂ : (↑D : Type u) → B := Prod.snd ∘ Subtype.val (p := fun (x : A × B) ↦ x ∈ D)
X₂_cont : Continuous X₂
⊢ f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂ = φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)
have h : ∀ (x : (↑E : Type u)),
  (f ∘ E.restrict (π := fun (a : (↑D : Type u)) ↦ B) X₂) x = (φ ∘ (⇑ρ' : (a : (↑E : Type u)) → A)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
⊢ ExtremallyDisconnected ((i : ι) × X i)
have open_closure : ∀ (U : Set ((i : ι) × X i)), IsOpen U → IsOpen (closure U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : IsOpen s
⊢ IsOpen (closure s)
have open_closure : ∀ (hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)) (i : ι),
  IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)
Tactic: rw [isOpen_sigma_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (hypothesis)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀ : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)
have h₁ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
Tactic: rcases h₀ i with ⟨h₀⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
h : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)
have rw : IsOpen (closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s)
have open_closure : Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
Tactic: suffices h : Sigma.mk i ⁻¹' closure s = closure (Sigma.mk i ⁻¹' s) by
    rw [h]
    exact h₀ _ (hs i)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
⊢ Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
have open_closure : IsOpenMap (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)
Tactic: apply IsOpenMap.preimage_closure_eq_closure_preimage
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
open_closure : IsOpenMap (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' closure s = closure (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
have open_closure₁ : Continuous (X := X i) (Sigma.mk (β := fun (i : ι) ↦ X i) i)
Tactic: apply IsOpenMap.preimage_closure_eq_closure_preimage
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
have open_closure : ∀ (i_1 : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i_1 ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
Tactic: rw [isOpen_sigma_iff]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
have pos : ∀ (ij : i = j), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
Tactic: by_cases ij : i = j
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
pos : ∀ (ij : i = j), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
have neg : ∀ (ij : ¬i = j), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
Tactic: by_cases ij : i = j
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : i = j
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
have pos : IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
Tactic: rwa [← ij, sigma_mk_preimage_image_eq_self]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
ι : Type u_1
X : ι → Type u_2
inst_1 : (i : ι) → TopologicalSpace (X i)
h₀_1 : ∀ (i : ι), ExtremallyDisconnected.{u_2} (X i)
s : Set ((i : ι) × X i)
hs : ∀ (i : ι), IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
i : ι
h₀ : ∀ (U : Set (X i)), IsOpen U → IsOpen (closure U)
U : Set (X i)
h : IsOpen U
j : ι
ij : ¬i = j
⊢ IsOpen (Sigma.mk (β := fun (i : ι) ↦ X i) j ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i '' U)
have neg : IsOpen.{u_2} (X := X j) ∅
Tactic: rw [sigma_mk_preimage_image' ij]
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
⊢ IsOpen (closure U)
have pos : ∀ (Un : U = ∅), IsOpen (closure U)
Tactic: by_cases! Un : U = ∅
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
pos : ∀ (Un : U = ∅), IsOpen (closure U)
⊢ IsOpen (closure U)
have neg : ∀ (Un : U.Nonempty), IsOpen (closure U)
Tactic: by_cases! Un : U = ∅
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
⊢ PreirreducibleSpace X
have apply : ∀ (s : Set X) (hs : IsOpen s) (sn : s.Nonempty), Dense s
Tactic: apply (preirreducibleSpace_iff_open_dense X).mpr (fun s hs sn ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
⊢ Dense s
have apply : closure s = univ
Tactic: apply dense_iff_closure_eq.mpr
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
⊢ closure s = univ
have inl : closure s = ∅ → closure s = univ
Tactic: cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩
-- Lean 4 proof step from Mathlib.Topology.ExtremallyDisconnected (goal)
Goal:
X : Type u
inst : TopologicalSpace X
h : ExtremallyDisconnected X
h' : PreconnectedSpace X
s : Set X
hs : IsOpen s
sn : s.Nonempty
inl : closure s = ∅ → closure s = univ
⊢ closure s = univ
have inr : closure s = univ → closure s = univ
Tactic: cases preconnectedSpace_iff_clopen.mp h' (closure s) ⟨isClosed_closure, h.open_closure s hs⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
E : B → Type u_5
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : (b : B) → TopologicalSpace (E b)
inst_4 : FiberBundle F E
inst_5 : T1Space B
x : B
⊢ IsClosed[inst_2] (range (TotalSpace.mk (E := E) x))
have rw : IsClosed[inst_2] (TotalSpace.proj (E := E) ⁻¹' {x})
Tactic: rw [TotalSpace.range_mk]