awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : inl x ∈ u
⊢ inl '' pathComponentIn (inl ⁻¹' u) x ⊆ pathComponentIn u (inl x)
have inl : IsPathConnected (X := X ⊕ Y) (inl '' pathComponentIn (inl ⁻¹' u) x)
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : Sum.inl x ∈ u
inl : IsPathConnected (X := X ⊕ Y) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x)
⊢ Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ pathComponentIn u (Sum.inl x)
have inl₁ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x) (Sum.inl x)
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
x : X
hxu : Sum.inl x ∈ u
inl : IsPathConnected (X := X ⊕ Y) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x)
inl₁ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x) (Sum.inl x)
⊢ Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ pathComponentIn u (Sum.inl x)
have inl₂ : Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ u
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ ∃ t ⊆ pathComponentIn u (inr y), IsOpen[instTopologicalSpaceSum] t ∧ inr y ∈ t
have inr : inr '' pathComponentIn (inr ⁻¹' u) y ⊆ pathComponentIn u (inr y)
Tactic: refine ⟨Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inr y), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inr y ∈ t
have inr₁ : IsOpen[instTopologicalSpaceSum] (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
Tactic: refine ⟨Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)
inr₁ : IsOpen[instTopologicalSpaceSum] (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inr y), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inr y ∈ t
have inr₂ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y) (Sum.inr y)
Tactic: refine ⟨Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : inr y ∈ u
⊢ inr '' pathComponentIn (inr ⁻¹' u) y ⊆ pathComponentIn u (inr y)
have inr : IsPathConnected (X := X ⊕ Y) (inr '' pathComponentIn (inr ⁻¹' u) y)
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : IsPathConnected (X := X ⊕ Y) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
⊢ Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)
have inr₁ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y) (Sum.inr y)
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : LocPathConnectedSpace Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
y : Y
hxu : Sum.inr y ∈ u
inr : IsPathConnected (X := X ⊕ Y) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y)
inr₁ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y) (Sum.inr y)
⊢ Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ pathComponentIn u (Sum.inr y)
have inr₂ : Sum.inr '' pathComponentIn (Sum.inr ⁻¹' u) y ⊆ u
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
⊢ LocPathConnectedSpace ((i : ι) × X i)
have rw : ∀ (x : (i : ι) × X i) (u : Set ((i : ι) × X i)), IsOpen[instTopologicalSpaceSigma] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Tactic: rw [locPathConnectedSpace_iff_pathComponentIn_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ pathComponentIn u x ∈ 𝓝 x
have rw : ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
have refine_1 : mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
  pathComponentIn u x
Tactic: refine ⟨(Sigma.mk x.1) '' pathComponentIn ((Sigma.mk x.1) ⁻¹' u) x.2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
have refine_2 : IsOpen[instTopologicalSpaceSigma]
  (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
Tactic: refine ⟨(Sigma.mk x.1) '' pathComponentIn ((Sigma.mk x.1) ⁻¹' u) x.2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
refine_2 :
  IsOpen[instTopologicalSpaceSigma]
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSigma] t ∧ x ∈ t
have refine_3 : x ∈
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))
Tactic: refine ⟨(Sigma.mk x.1) '' pathComponentIn ((Sigma.mk x.1) ⁻¹' u) x.2, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
have refine_1 : IsPathConnected
  (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  IsPathConnected
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
have refine_1₁ : x ∈
  mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
x_1 y z : X_1
ι : Type u_3
F : Set X_1
inst_2 : LocPathConnectedSpace X_1
X : ι → Type u_4
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), LocPathConnectedSpace.{u_4} (X i)
x : (i : ι) × X i
u : Set ((i : ι) × X i)
hu : IsOpen[instTopologicalSpaceSigma] u
hxu : x ∈ u
refine_1 :
  IsPathConnected
    (mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)))
refine_1₁ :
  x ∈
    mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i))
⊢ mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
      pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
    pathComponentIn u x
have refine_1₂ : mk (β := fun (i : ι) ↦ X i) (x.fst (β := fun (i : ι) ↦ X i)) ''
    pathComponentIn (mk (β := X) (x.fst (β := fun (i : ι) ↦ X i)) ⁻¹' u) (x.snd (β := fun (i : ι) ↦ X i)) ⊆
  u
Tactic: apply IsPathConnected.subset_pathComponentIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
⊢ LocPathConnectedSpace X
have apply : ∀ (x : X) (i : Unit), True → IsPathConnected (X := X) (nhdsKer {x})
Tactic: apply LocPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
⊢ ∀ (x : X) (i : Unit), True → IsPathConnected (X := X) (nhdsKer {x})
have simp : ∀ (x : X), ∃ (x_1 : X), x_1 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_1 y
Tactic: simp only [forall_const, IsPathConnected, mem_nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x : X
⊢ ∃ (x_2 : X), x_2 ⤳ x ∧ ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x_2 y
have exists : ∀ ⦃y : X⦄, y ⤳ x → JoinedIn (nhdsKer {x}) x y
Tactic: exists x, specializes_rfl
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) x y
have symm : JoinedIn (nhdsKer {x}) y x
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) y x
have hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
Tactic: apply hy.joinedIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
⊢ JoinedIn (nhdsKer {x}) y x
have hy₁ : Membership.mem (γ := Set X) (nhdsKer {x}) x
Tactic: apply hy.joinedIn
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ Membership.mem (γ := Set X) (nhdsKer {x}) x
have hy₁ : x ⤳ x
Tactic: rewrite [mem_nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) y x
have hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
Tactic: apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
⊢ JoinedIn (nhdsKer {x}) y x
have hy₁ : Membership.mem (γ := Set X) (nhdsKer {x}) x
Tactic: apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
inst_3 : AlexandrovDiscrete X
x y : X
hy : y ⤳ x
hx : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₁ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₁ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₂ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₂ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₃ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₃ : Membership.mem (γ := Set X) (nhdsKer {x}) y
hy₄ : Membership.mem (γ := Set X) (nhdsKer {x}) x
hx₄ : y ⤳ x
⊢ JoinedIn (nhdsKer {x}) y x
have hy₅ : x ⤳ x
Tactic: apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
⊢ DiscreteTopology.{u_1} (ZerothHomotopy X)
have refine : ∀ (c : ZerothHomotopy X), IsOpen (X := ZerothHomotopy X) {c}
Tactic: refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
c : ZerothHomotopy X
⊢ IsOpen (X := ZerothHomotopy X) {c}
have obtain : ∀ (x : X), IsOpen (X := ZerothHomotopy X) {ZerothHomotopy.mk x}
Tactic: obtain ⟨x, rfl⟩ := ZerothHomotopy.mk_surjective c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : LocPathConnectedSpace X
x : X
⊢ IsOpen (X := ZerothHomotopy X) {ZerothHomotopy.mk x}
have rw : IsOpen[inst] (preimage (β := ZerothHomotopy X) ZerothHomotopy.mk {ZerothHomotopy.mk x})
Tactic: rw [← ZerothHomotopy.isQuotientMap_mk.isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have simp_rw : (∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id) ↔
  ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
Tactic: simp_rw [locallyConnectedSpace_iff_hasBasis_isOpen_isConnected]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id) ↔
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have refine : ∀ (x : α),
  (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
Tactic: refine forall_congr' fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have mp : (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id →
  ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
mp :
  (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id →
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
⊢ (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id ↔
    ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have mpr : (∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
  (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
x : α
h : (𝓝 x).HasBasis (fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsConnected s) id
U : Set α
hU : U ∈ 𝓝 x
⊢ ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have mp : ∀ (V : Set α) (hV : IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) (hVU : id V ⊆ U),
  ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
Tactic: rcases h.mem_iff.mp hU with ⟨V, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
h : F ∈ 𝓝 x
⊢ connectedComponentIn F x ∈ 𝓝 x
have h₁ : ∃ (i : Set α), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
Tactic: rw [(LocallyConnectedSpace.open_connected_basis x).mem_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
h : ∃ (i : Set α), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ F
⊢ connectedComponentIn F x ∈ 𝓝 x
have rcases : ∀ (s : Set α) (hsF : id s ⊆ F) (h1s : IsOpen[inst] s) (hxs : x ∈ s) (h2s : IsConnected s),
  connectedComponentIn F x ∈ 𝓝 x
Tactic: rcases h with ⟨s, ⟨h1s, hxs, h2s⟩, hsF⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
⊢ IsOpen[inst] (connectedComponentIn F x)
have rw : ∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y
have rw : connectedComponentIn F y ∈ 𝓝 y
Tactic: rw [connectedComponentIn_eq hy]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
x : α
⊢ IsOpen[inst] (connectedComponent x)
have rw : IsOpen[inst] (connectedComponentIn univ x)
Tactic: rw [← connectedComponentIn_univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
have mp : LocallyConnectedSpace α → ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
Tactic: constructor