awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst] u
v_op : IsOpen[inst] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ False
have this : ContinuousOn u.boolIndicator s
Tactic: have : ContinuousOn u.boolIndicator s := by
    apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
    · rw [preimage_subtype_coe_eq_compl hsuv H]
      exact (v_op.preimage continuous_subtype_val).isClosed_compl
    · exact u_op.preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ PreconnectedSpace α ↔ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have refine : ∀ (h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ), PreconnectedSpace α
Tactic: refine ⟨fun _ _ => isClopen_iff.mp, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ PreconnectedSpace α
have refine : ∀ (f : α → Bool) (hf : Continuous[inst, _] f) (x y : α), f x = f y
Tactic: refine preconnectedSpace_of_forall_constant fun f hf x y ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have rw : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
Tactic: rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
rw : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have rw₁ : f ⁻¹' {false} = f ⁻¹' {!true}
Tactic: rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
rw : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
rw₁ : f ⁻¹' {false} = f ⁻¹' {!true}
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
have rw₂ : f ⁻¹' {false} = f ⁻¹' {false}
Tactic: rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
⊢ f x = f y
have this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
Tactic: have : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ := by
    rw [← Set.preimage_compl, Bool.compl_singleton, Bool.not_true]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
⊢ f x = f y
have inl : ∀ (h : f ⁻¹' {true} = ∅), f x = f y
Tactic: obtain (h | h) := h _ ((isClopen_discrete {true}).preimage hf)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
inl : ∀ (h : f ⁻¹' {true} = ∅), f x = f y
⊢ f x = f y
have inr : ∀ (h : f ⁻¹' {true} = univ), f x = f y
Tactic: obtain (h | h) := h _ ((isClopen_discrete {true}).preimage hf)
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Tactic: rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have rw₁ : Set.Nonempty.{u} (α := α) univ ∧ IsPreconnected.{u} (α := α) univ ↔
  Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Tactic: rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₁ :
  Set.Nonempty.{u} (α := α) univ ∧ IsPreconnected.{u} (α := α) univ ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have rw₂ : Set.Nonempty.{u} (α := α) univ ∧ PreconnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Tactic: rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₁ :
  Set.Nonempty.{u} (α := α) univ ∧ IsPreconnected.{u} (α := α) univ ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₂ : Set.Nonempty.{u} (α := α) univ ∧ PreconnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have rw₃ : (Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
  Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Tactic: rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.Clopen (goal)
Goal:
α : Type u
inst : TopologicalSpace α
rw : IsConnected.{u} (α := α) univ ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₁ :
  Set.Nonempty.{u} (α := α) univ ∧ IsPreconnected.{u} (α := α) univ ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₂ : Set.Nonempty.{u} (α := α) univ ∧ PreconnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
rw₃ :
  (Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
    Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
⊢ ConnectedSpace α ↔ Nonempty α ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
have rw₄ : (Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
  Set.Nonempty.{u} (α := α) univ ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
Tactic: rw [connectedSpace_iff_univ, IsConnected, ← preconnectedSpace_iff_univ,
    preconnectedSpace_iff_clopen, Set.nonempty_iff_univ_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id
have rw : ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
Tactic: rw [hasBasis_self]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)
x : X
t : Set X
ht : t ∈ 𝓝 x
⊢ ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
have rcases : ∀ (i : ι) (hpi : p x i) (hi : s x i ⊆ t), ∃ r ∈ 𝓝 x, IsPathConnected r ∧ r ⊆ t
Tactic: rcases (h x).mem_iff.mp ht with ⟨i, hpi, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x : X
⊢ IsOpen[inst] (pathComponentIn F x)
have rw : ∀ x_1 ∈ pathComponentIn F x, pathComponentIn F x ∈ 𝓝 x_1
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : IsOpen[inst] F
x y : X
hy : y ∈ pathComponentIn F x
⊢ pathComponentIn F x ∈ 𝓝 y
have let : ∀ (s : Set X) (hs : (s ∈ 𝓝 y ∧ IsPathConnected s) ∧ id s ⊆ F), pathComponentIn F x ∈ 𝓝 y
Tactic: let ⟨s, hs⟩ := (path_connected_basis y).mem_iff.mp (hF.mem_nhds (pathComponentIn_subset hy))
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ IsOpen[inst] (pathComponent x)
have rw : IsOpen[inst] (pathComponentIn univ x)
Tactic: rw [← pathComponentIn_univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ IsClosed[inst] (pathComponent x)
have rw : ∀ x_1 ∈ (pathComponent x)ᶜ, (pathComponent x)ᶜ ∈ 𝓝 x_1
Tactic: rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
⊢ (pathComponent x)ᶜ ∈ 𝓝 y
have rcases : ∀ (V : Set X) (hVy : V ∈ 𝓝 y) (hVc : IsPathConnected V), (pathComponent x)ᶜ ∈ 𝓝 y
Tactic: rcases (path_connected_basis y).ex_mem with ⟨V, hVy, hVc⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
hxy : y ∈ (pathComponent x)ᶜ
V : Set X
hVy : V ∈ 𝓝 y
hVc : IsPathConnected V
⊢ (pathComponent x)ᶜ ∈ 𝓝 y
have h : ∀ (z : X) (hz : z ∈ V) (hxz : z ∈ pathComponent x), False
Tactic: filter_upwards [hVy] with z hz hxz
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
inst_1 : LocPathConnectedSpace X
hF : F ∈ 𝓝 x
⊢ pathComponentIn F x ∈ 𝓝 x
have let : ∀ (u : Set X) (huF : u ⊆ F) (hu : IsOpen[inst] u) (hxu : x ∈ u), pathComponentIn F x ∈ 𝓝 x
Tactic: let ⟨u, huF, hu, hxu⟩ := mem_nhds_iff.mp hF
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x y : X
⊢ connectedComponent x = connectedComponent y ↔ Joined x y
have rw : connectedComponent y = connectedComponent x ↔ y ∈ connectedComponent x
Tactic: rw [← mem_pathComponent_iff, pathComponent_eq_connectedComponent, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id
have refine : ∀ (s : Set X) (hs : s ∈ 𝓝 x), ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
Tactic: refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
have have : ∀ (u : Set X) (hus : u ⊆ s) (hu : IsOpen[inst] u) (hxu : x ∈ u),
  ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
Tactic: have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs
-- 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
inst_2 : LocPathConnectedSpace X
e : Y → X
he : IsOpenEmbedding e
this :
  ∀ (y : Y), (𝓝 y).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) fun (x : Set X) ↦ e ⁻¹' x
x : Y
s : Set X
h : s ∈ 𝓝 (e x) ∧ IsPathConnected s ∧ s ⊆ range e
left : s ∈ 𝓝 (e x)
hs : IsPathConnected s
hse : s ⊆ range e
⊢ IsPathConnected (e ⁻¹' s)
have rwa : IsPathConnected (e '' e ⁻¹' s)
Tactic: rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
⊢ IsConnected U ↔ IsPathConnected U
have rw : ConnectedSpace.{u_1} (↑U : Type u_1) ↔ PathConnectedSpace.{u_1} (↑U : Type u_1)
Tactic: rw [isConnected_iff_connectedSpace, isPathConnected_iff_pathConnectedSpace]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
⊢ ConnectedSpace.{u_1} (↑U : Type u_1) ↔ PathConnectedSpace.{u_1} (↑U : Type u_1)
have this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
Tactic: haveI := U_op.locPathConnectedSpace
-- 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
⊢ LocallyConnectedSpace X
have refine : ∀ (x : X) (h : (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id) (s : Set X),
  s ∈ 𝓝 x ↔ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
Tactic: refine ⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩
-- 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
h : (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
have refine : ∀ (hs : s ∈ 𝓝 x), ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
Tactic: refine ⟨fun hs ↦ ?_, fun ⟨u, ⟨hu, hxu, _⟩, hus⟩ ↦ mem_nhds_iff.mpr ⟨u, hus, hu, hxu⟩⟩
-- 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
h : (𝓝 x).HasBasis (fun (s : Set X) ↦ IsOpen[inst] s ∧ x ∈ s ∧ IsPathConnected s) id
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
have let : ∀ (u : Set X) (hu : IsOpen[inst] u) (hxu : x ∈ u) (hu' : IsPathConnected u) (hus : id u ⊆ s),
  ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
Tactic: let ⟨u, ⟨hu, hxu, hu'⟩, hus⟩ := (h.mem_iff' s).mp hs
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen[inst] u → IsOpen[inst] (pathComponentIn u x)
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have refine : ∀ (hs : s ∈ 𝓝 x), ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
Tactic: refine ⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
h : ∀ (x : X) (u : Set X), IsOpen[inst] u → IsOpen[inst] (pathComponentIn u x)
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
have let : ∀ (u : Set X) (hu : u ⊆ s ∧ IsOpen[inst] u ∧ x ∈ u), ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
Tactic: let ⟨u, hu⟩ := mem_nhds_iff.mp hs
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
⊢ LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen[inst] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
have rw : (∀ (x : X) (u : Set X), IsOpen[inst] u → IsOpen[inst] (pathComponentIn u x)) ↔
  ∀ (x : X) (u : Set X), IsOpen[inst] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
Tactic: rw [locPathConnectedSpace_iff_isOpen_pathComponentIn]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
⊢ (∀ (x : X) (u : Set X), IsOpen[inst] u → IsOpen[inst] (pathComponentIn u x)) ↔
    ∀ (x : X) (u : Set X), IsOpen[inst] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
have simp_rw : (∀ (b : Set X), IsOpen[inst] b → ∀ (x : X), IsOpen[inst] (pathComponentIn b x)) ↔
  ∀ (b : Set X), IsOpen[inst] b → ∀ x ∈ b, pathComponentIn b x ∈ 𝓝 x
Tactic: simp_rw [forall_comm (β := Set X), ← imp_forall_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
⊢ (∀ (b : Set X), IsOpen[inst] b → ∀ (x : X), IsOpen[inst] (pathComponentIn b x)) ↔
    ∀ (b : Set X), IsOpen[inst] b → ∀ x ∈ b, pathComponentIn b x ∈ 𝓝 x
have refine : ∀ (u : Set X), IsOpen[inst] u → ((∀ (x : X), IsOpen[inst] (pathComponentIn u x)) ↔ ∀ x ∈ u, pathComponentIn u x ∈ 𝓝 x)
Tactic: refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x : TopologicalSpace Y := TopologicalSpace.coinduced f inst
⊢ LocPathConnectedSpace Y
have hf : Continuous[inst, x] f
Tactic: have hf : Continuous f := continuous_coinduced_rng
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x : TopologicalSpace Y := TopologicalSpace.coinduced f inst
hf : Continuous[inst, x] f
⊢ LocPathConnectedSpace Y
have refine : ∀ (y : Y) (u : Set Y) (hu : IsOpen[TopologicalSpace.coinduced f inst] u) (x : X) (hx : x ∈ f ⁻¹' pathComponentIn u y),
  f ⁻¹' pathComponentIn u y ∈ 𝓝 x
Tactic: refine locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
    isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x_1 : TopologicalSpace Y := TopologicalSpace.coinduced f inst
hf : Continuous[inst, x_1] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
⊢ f ⁻¹' pathComponentIn u y ∈ 𝓝 x
have hx' : x ∈ f ⁻¹' u
Tactic: have hx' := preimage_mono pathComponentIn_subset hx
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x_1 : TopologicalSpace Y := TopologicalSpace.coinduced f inst
hf : Continuous[inst, x_1] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ f ⁻¹' pathComponentIn u y ∈ 𝓝 x
have refine : pathComponentIn (f ⁻¹' u) x ⊆ f ⁻¹' pathComponentIn u y
Tactic: refine mem_nhds_iff.mpr ⟨pathComponentIn (f ⁻¹' u) x, ?_,
    (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocPathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
Y : Type u_4
f : X → Y
x_1 : TopologicalSpace Y := TopologicalSpace.coinduced f inst
hf : Continuous[inst, x_1] f
y : Y
u : Set Y
hu : IsOpen[TopologicalSpace.coinduced f inst] u
x : X
hx : x ∈ f ⁻¹' pathComponentIn u y
hx' : x ∈ f ⁻¹' u
⊢ pathComponentIn (f ⁻¹' u) x ⊆ f ⁻¹' pathComponentIn u y
have rw : f '' pathComponentIn (f ⁻¹' u) x ⊆ pathComponentIn u (f x)
Tactic: rw [← image_subset_iff, ← pathComponentIn_congr hx]
-- 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 : LocPathConnectedSpace Y
⊢ LocPathConnectedSpace (X ⊕ Y)
have rw : ∀ (x : X ⊕ Y) (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] 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 : 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
x : X ⊕ Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
hxu : x ∈ u
⊢ pathComponentIn u x ∈ 𝓝 x
have rw : ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t
Tactic: rw [mem_nhds_iff]
-- 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
x : X ⊕ Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
hxu : x ∈ u
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t
have inl : ∀ (x : X) (hxu : inl x ∈ u), ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t
Tactic: obtain x | y := x
Cleared hypotheses: x, hxu
-- 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
x : X ⊕ Y
u : Set (X ⊕ Y)
hu : IsOpen[instTopologicalSpaceSum] u
hxu : x ∈ u
inl :
  ∀ (x : X) (hxu : Sum.inl x ∈ u),
    ∃ t ⊆ pathComponentIn u (Sum.inl x), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inl x ∈ t
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t
have inr : ∀ (y : Y) (hxu : inr y ∈ u), ∃ t ⊆ pathComponentIn u (inr y), IsOpen[instTopologicalSpaceSum] t ∧ inr y ∈ t
Tactic: obtain x | y := x
Cleared hypotheses: x, hxu
-- 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
⊢ ∃ t ⊆ pathComponentIn u (inl x), IsOpen[instTopologicalSpaceSum] t ∧ inl x ∈ t
have inl : inl '' pathComponentIn (inl ⁻¹' u) x ⊆ pathComponentIn u (inl x)
Tactic: refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩
-- 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 : Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ pathComponentIn u (Sum.inl x)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inl x), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inl x ∈ t
have inl₁ : IsOpen[instTopologicalSpaceSum] (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x)
Tactic: refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩
-- 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 : Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ pathComponentIn u (Sum.inl x)
inl₁ : IsOpen[instTopologicalSpaceSum] (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inl x), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inl x ∈ t
have inl₂ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x) (Sum.inl x)
Tactic: refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩