awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
mp : LocallyConnectedSpace α → ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
⊢ LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
have mpr : (∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)) → LocallyConnectedSpace α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
⊢ LocallyConnectedSpace α
have mpr : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
Tactic: rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
have mpr : ∀ (x : α) (U : Set α) (hU : U ∈ 𝓝 x), x ∈ interior U
Tactic: refine fun x U hU =>
        ⟨connectedComponentIn (interior U) x,
          (connectedComponentIn_subset _ _).trans interior_subset, h _ isOpen_interior x ?_,
          mem_connectedComponentIn ?_, isConnected_connectedComponentIn_iff.mpr ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
have mp : LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
mp : LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
have mpr : (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
have mp : (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V) →
  ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Tactic: rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
have mp : ∀ (V : Set α) (hVU : V ⊆ U) (hV₁ : IsOpen[inst] V) (hxV : x ∈ V) (hV₂ : IsConnected V),
  ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Tactic: rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) → LocallyConnectedSpace α
have mpr : (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) →
  ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
Tactic: rw [locallyConnectedSpace_iff_connectedComponentIn_open]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) →
    ∀ (F : Set α), IsOpen[inst] F → ∀ x ∈ F, IsOpen[inst] (connectedComponentIn F x)
have mpr : ∀ (h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) (U : Set α) (hU : IsOpen[inst] U),
  ∀ x ∈ U, ∀ (y : α) (hy : y ∈ connectedComponentIn U x), connectedComponentIn U x ∈ 𝓝 y
Tactic: refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
⊢ connectedComponentIn U x ∈ 𝓝 y
have mpr : connectedComponentIn U y ∈ 𝓝 y
Tactic: rw [connectedComponentIn_eq hy]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
U : Set α
hU : IsOpen[inst] U
x : α
h_1 : x ∈ U
y : α
hy : y ∈ connectedComponentIn U x
⊢ connectedComponentIn U y ∈ 𝓝 y
have mpr : ∀ (V : Set α) (hVy : V ∈ 𝓝 y) (hV : IsPreconnected V) (hVU : V ⊆ U), connectedComponentIn U y ∈ 𝓝 y
Tactic: rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
have rw : (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U) ↔
  ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
Tactic: rw [locallyConnectedSpace_iff_connected_subsets]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
b : α → ι → Set α
p : α → ι → Prop
hbasis : ∀ (x : α), (𝓝 x).HasBasis (p x) (b x)
hconnected : ∀ (x : α) (i : ι), p x i → IsPreconnected (b x i)
⊢ LocallyConnectedSpace α
have rw : ∀ (x : α), (𝓝 x).HasBasis (fun (s : Set α) ↦ s ∈ 𝓝 x ∧ IsPreconnected s) id
Tactic: rw [locallyConnectedSpace_iff_connected_basis]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
⊢ LocallyConnectedSpace β
have refine : ∀ (x : β),
  Filter.HasBasis.{v, u + 1} (ι := Set α) (𝓝 x)
    ((fun (x : β) (s : Set α) ↦ (IsOpen[inst] s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x)
    ((fun (x : β) (s : Set α) ↦ f ⁻¹' s) x)
Tactic: refine locallyConnectedSpace_of_connected_bases (fun _ s ↦ f ⁻¹' s)
    (fun x s ↦ (IsOpen s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) (fun x ↦ ?_)
    (fun x s hxs ↦ hxs.1.2.2.isPreconnected.preimage_of_isOpenMap h.injective h.isOpenMap hxs.2)
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ Filter.HasBasis.{v, u + 1} (ι := Set α) (𝓝 x)
    ((fun (x : β) (s : Set α) ↦ (IsOpen[inst] s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x)
    ((fun (x : β) (s : Set α) ↦ f ⁻¹' s) x)
have rw : Filter.HasBasis.{v, u + 1} (ι := Set α) (Filter.comap f (𝓝 (f x)))
  ((fun (x : β) (s : Set α) ↦ (IsOpen[inst] s ∧ f x ∈ s ∧ IsConnected s) ∧ s ⊆ range f) x)
  ((fun (x : β) (s : Set α) ↦ f ⁻¹' s) x)
Tactic: rw [h.nhds_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
⊢ DiscreteTopology.{u} (ConnectedComponents α)
have refine : ∀ (c : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {c}
Tactic: refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.LocallyConnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
c : ConnectedComponents α
⊢ IsOpen (X := ConnectedComponents α) {c}
have obtain : ∀ (x : α), IsOpen (X := ConnectedComponents α) {ConnectedComponents.mk x}
Tactic: obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
M : Type u_4
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l l' : List M
h : List.Forall₂ Joined l l'
⊢ Joined l.prod l'.prod
have nil : Joined.{u_4} (X := M) (List.prod []) (List.prod [])
Tactic: induction h with
  | nil => rfl
  | cons h₁ _ h₂ => exact h₁.mul h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
M : Type u_4
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l l' : List M
h : List.Forall₂ Joined l l'
nil : Joined.{u_4} (X := M) (List.prod []) (List.prod [])
⊢ Joined l.prod l'.prod
have cons : ∀ {a b : M} {l₁ l₂ : List M} (h₁ : Joined a b),
  List.Forall₂ Joined l₁ l₂ → ∀ (h₂ : Joined l₁.prod l₂.prod), Joined (a :: l₁).prod (b :: l₂).prod
Tactic: induction h with
  | nil => rfl
  | cons h₁ _ h₂ => exact h₁.mul h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F
have rcases : ∀ (γ : Path x y) (γ_in : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)),
  x ∈ F ∧ y ∈ F
Tactic: rcases h with ⟨γ, γ_in⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
⊢ Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X) ∧
    Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
have left : Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
left : Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X)
⊢ Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X) ∧
    Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
have right : Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
γ : Path x y
γ_in : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
⊢ x ∈ F ∧ y ∈ F
have this : Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X) ∧
  Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
Tactic: have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ JoinedIn F y x
have hx : x ∈ F
Tactic: obtain ⟨hx, hy⟩ := h.mem
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
⊢ JoinedIn F y x
have hy : y ∈ F
Tactic: obtain ⟨hx, hy⟩ := h.mem
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F y x
have simp_all : ∀ (h : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy)) (hx_1 : x ∈ F)
  (hy_1 : y ∈ F), Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx)
Tactic: simp_all only [joinedIn_iff_joined]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z
have hx : x ∈ F
Tactic: obtain ⟨hx, hy⟩ := hxy.mem
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
⊢ JoinedIn F x z
have hy : y ∈ F
Tactic: obtain ⟨hx, hy⟩ := hxy.mem
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy hx₁ : y ∈ F
⊢ JoinedIn F x z
have hy₁ : z ∈ F
Tactic: obtain ⟨hx, hy⟩ := hyz.mem
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx_1 : x ∈ F
hy_1 hx : y ∈ F
hy : z ∈ F
⊢ JoinedIn F x z
have simp_all : ∀ (hxy : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1))
  (hyz : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) z hy))
  (hx : x ∈ F) (hx : y ∈ F) (hy_2 : z ∈ F),
  Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) z hy)
Tactic: simp_all only [joinedIn_iff_joined]
Cleared hypotheses: hxy, hyz, hx
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x y
have refine_1 : Continuous[_, inst] (piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x))
Tactic: refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
refine_1 :
  Continuous[_, inst] (piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x))
⊢ JoinedIn F x y
have refine_2 : ∀ (t : (↑I : Type)),
  Membership.mem (α := X) F
    (({ toFun := piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x),
            continuous_toFun := sorry, source' := sorry, target' := sorry } :
          (a : (↑I : Type)) → X)
        t :
      X)
Tactic: refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : (↑I : Type)
⊢ Membership.mem (α := X) F
    (({ toFun := piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x),
            continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } :
          (a : (↑I : Type)) → X)
        t :
      X)
have refine_2 : (if Membership.mem (γ := Set (↑I : Type)) {1} t then const (↑I : Type) y t else const (↑I : Type) x t) ∈ F
Tactic: simp only [Path.coe_mk_mk, piecewise]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : (↑I : Type)
⊢ (if Membership.mem (γ := Set (↑I : Type)) {1} t then const (↑I : Type) y t else const (↑I : Type) x t) ∈ F
have pos : Membership.mem (γ := Set (↑I : Type)) {1} t → const (↑I : Type) y t ∈ F
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
t : (↑I : Type)
pos : Membership.mem (γ := Set (↑I : Type)) {1} t → const (↑I : Type) y t ∈ F
⊢ (if Membership.mem (γ := Set (↑I : Type)) {1} t then const (↑I : Type) y t else const (↑I : Type) x t) ∈ F
have neg : t ∉ {1} → const (↑I : Type) x t ∈ F
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y
have refine : JoinedIn (f '' F) (f x) (f y) → JoinedIn F x y
Tactic: refine ⟨?_, (.map · hf.continuous)⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := Y) (f '' F) ((γ : (a : (↑I : Type)) → Y) t : Y)
⊢ JoinedIn F x y
have choose : ∀ (γ' : (t : (↑I : Type)) → X) (hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F)
  (hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t), JoinedIn F x y
Tactic: choose γ' hγ'F hγ' using hγ
Cleared hypotheses: hγ
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
⊢ x ⤳ γ' 0
have rw : f x ⤳ f (γ' 0)
Tactic: rw [← hf.specializes_iff, hγ', γ.source]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
rw : f x ⤳ f (γ' 0)
⊢ x ⤳ γ' 0
have rw₁ : f x ⤳ (γ : (a : (↑I : Type)) → Y) 0
Tactic: rw [← hf.specializes_iff, hγ', γ.source]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
rw : f x ⤳ f (γ' 0)
rw₁ : f x ⤳ (γ : (a : (↑I : Type)) → Y) 0
⊢ x ⤳ γ' 0
have rw₂ : f x ⤳ f x
Tactic: rw [← hf.specializes_iff, hγ', γ.source]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
⊢ JoinedIn F x y
have h₀ : x ⤳ γ' 0
Tactic: have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
⊢ γ' 1 ⤳ y
have rw : f (γ' 1) ⤳ f y
Tactic: rw [← hf.specializes_iff, hγ', γ.target]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
rw : f (γ' 1) ⤳ f y
⊢ γ' 1 ⤳ y
have rw₁ : (γ : (a : (↑I : Type)) → Y) 1 ⤳ f y
Tactic: rw [← hf.specializes_iff, hγ', γ.target]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
rw : f (γ' 1) ⤳ f y
rw₁ : (γ : (a : (↑I : Type)) → Y) 1 ⤳ f y
⊢ γ' 1 ⤳ y
have rw₂ : f y ⤳ f y
Tactic: rw [← hf.specializes_iff, hγ', γ.target]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
⊢ JoinedIn F x y
have h₁ : γ' 1 ⤳ y
Tactic: have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
⊢ JoinedIn F (γ' 0) (γ' 1)
have refine : Continuous[_, inst] γ'
Tactic: refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : (t : (↑I : Type)) → X
hγ'F : ∀ (t : (↑I : Type)), γ' t ∈ F
hγ' : ∀ (t : (↑I : Type)), f (γ' t) = (γ : (a : (↑I : Type)) → Y) t
h₀ : x ⤳ γ' 0
h₁ : γ' 1 ⤳ y
⊢ JoinedIn F x y
have h : JoinedIn F (γ' 0) (γ' 1)
Tactic: have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
⊢ pathComponent x = pathComponent y
have h₁ : ∀ (z : X), z ∈ pathComponent x ↔ z ∈ pathComponent y
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y
have h₁ : z ∈ pathComponent x → z ∈ pathComponent y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h₁ : z ∈ pathComponent x → z ∈ pathComponent y
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y
have h₂ : z ∈ pathComponent y → z ∈ pathComponent x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ z ∈ pathComponent y
have h₁ : y ∈ pathComponent z
Tactic: rw [pathComponent_symm]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
⊢ z ∈ pathComponent x
have h₁ : ∀ (h' : y ∈ pathComponent z), x ∈ pathComponent z
Tactic: rw [pathComponent_symm] at h' ⊢
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ⋃ y ∈ connectedComponent x, pathComponent y = connectedComponent x
have simp : ∀ (x_1 : X), (∃ (i : X) (_ : i ∈ connectedComponent x), x_1 ∈ pathComponent i) ↔ x_1 ∈ connectedComponent x
Tactic: simp only [Set.ext_iff, mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
⊢ pathComponentIn F x = pathComponentIn F y
have h₁ : ∀ (x_1 : X), x_1 ∈ pathComponentIn F x ↔ x_1 ∈ pathComponentIn F y
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F
have mp : IsPathConnected F → ∃ x ∈ F, pathComponentIn F x = F
Tactic: constructor