awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TopologicalSpace.IsTopologicalBasis.{u} (α := α) {s : Set α | IsOpen[inst] s ∧ IsPreconnected s}
x : α
⊢ ∀ (i : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | IsOpen[inst] s ∧ IsPreconnected s} i ∧ x ∈ i ↔
      IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i

Tactic:
grind [IsConnected, Set.Nonempty]

Premises used: IsConnected, Set.Nonempty
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
⊢ LocallyConnectedSpace β

Tactic:
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)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, IsConnected, Membership.mem, HasSubset.Subset, And, And.right, Set.preimage, And.left, IsConnected.isPreconnected, Topology.IsEmbedding.injective, IsOpen, locallyConnectedSpace_of_connected_bases, Set.range, IsPreconnected.preimage_of_isOpenMap
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
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)
⊢ LocallyConnectedSpace β

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)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, IsConnected, Membership.mem, HasSubset.Subset, And, And.right, Set.preimage, And.left, IsConnected.isPreconnected, Topology.IsEmbedding.injective, IsOpen, locallyConnectedSpace_of_connected_bases, Set.range, IsPreconnected.preimage_of_isOpenMap
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
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)
⊢ 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:
rw [h.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ 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:
LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap _

Premises used: Set.mem_range_self, Filter.HasBasis.comap, Topology.IsOpenEmbedding.isOpen_range, Filter.HasBasis.restrict_subset, IsOpen.mem_nhds, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
inst_2 : TopologicalSpace β
f : β → α
h : IsOpenEmbedding f
x : β
⊢ 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:
exact LocallyConnectedSpace.open_connected_basis (f x) |>.restrict_subset
    (h.isOpen_range.mem_nhds <| mem_range_self _) |>.comap _

Premises used: Set.mem_range_self, Filter.HasBasis.comap, Topology.IsOpenEmbedding.isOpen_range, Filter.HasBasis.restrict_subset, IsOpen.mem_nhds, LocallyConnectedSpace.open_connected_basis
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LocallyConnectedSpace α
U : Set α
hU : IsOpen[inst] U
⊢ LocallyConnectedSpace.{u} (↑U : Type u)

Tactic:
hU.isOpenEmbedding_subtypeVal.locallyConnectedSpace

Premises used: IsOpen.isOpenEmbedding_subtypeVal, Topology.IsOpenEmbedding.locallyConnectedSpace
-- Module: Mathlib.Topology.Connected.LocallyConnected
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 α)

Tactic:
discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
refine : ∀ (c : ConnectedComponents α), IsOpen (X := ConnectedComponents α) {c}
⊢ DiscreteTopology.{u} (ConnectedComponents α)

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
c : ConnectedComponents α
obtain : ∀ (x : α), IsOpen (X := ConnectedComponents α) {ConnectedComponents.mk x}
⊢ IsOpen (X := ConnectedComponents α) {c}

Tactic:
obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe c

Premises used: ConnectedComponents.surjective_coe, rfl
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
x : α
⊢ IsOpen (X := ConnectedComponents α) {ConnectedComponents.mk x}

Tactic:
simp [← ConnectedComponents.isQuotientMap_coe.isOpen_preimage,
    connectedComponents_preimage_singleton, isOpen_connectedComponent]

Premises used: connectedComponents_preimage_singleton, Topology.IsCoinducing.isOpen_preimage, isOpen_connectedComponent, Topology.IsQuotientMap.isCoinducing, ConnectedComponents.isQuotientMap_coe
-- Module: Mathlib.Topology.Connected.LocallyConnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : LocallyConnectedSpace α
inst_2 : CompactSpace α
⊢ Finite.{u + 1} (ConnectedComponents α)

Tactic:
finite_of_compact_of_discrete

Premises used: finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Connected.PathComponentOne
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : LocPathConnectedSpace G
⊢ IsClosed (↑(pathComponentOne G) : Set G)

Tactic:
.pathComponent 1

Premises used: setOf, pathComponent, IsClosed.pathComponent, OfNat.ofNat, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Joined x x

Tactic:
⟨Path.refl x⟩

Premises used: Nonempty.intro, Path.refl, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : Joined x y
⊢ Joined y x

Tactic:
⟨h.somePath.symm⟩

Premises used: Path.symm, Joined.somePath, Nonempty.intro, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
hxy : Joined x y
hyz : Joined y z
⊢ Joined x z

Tactic:
⟨hxy.somePath.trans hyz.somePath⟩

Premises used: Path.trans, Joined.somePath, Nonempty.intro, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
M : Type u_4
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
a b c d : M
hs : Joined a b
ht : Joined c d
⊢ Joined (a * c) (b * d)

Tactic:
⟨hs.somePath.mul ht.somePath⟩

Premises used: Joined.somePath, Nonempty.intro, Path.mul, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
M : Type u_4
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l l' : List M
⊢ Joined.{u_4} (X := M) (List.prod []) (List.prod [])

Tactic:
rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
M : Type u_4
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l l' : List M
a b : M
l₁ l₂ : List M
h₁ : Joined a b
h : List.Forall₂ Joined l₁ l₂
h₂ : Joined l₁.prod l₂.prod
⊢ Joined (a :: l₁).prod (b :: l₂).prod

Tactic:
h₁.mul h₂

Premises used: Joined.mul, List.foldr, List.prod
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
M : Type u_4
inst : MulOneClass M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l l' : List M
a b : M
l₁ l₂ : List M
h₁ : Joined a b
h : List.Forall₂ Joined l₁ l₂
h₂ : Joined l₁.prod l₂.prod
⊢ Joined (a :: l₁).prod (b :: l₂).prod

Tactic:
exact h₁.mul h₂

Premises used: Joined.mul
-- Module: Mathlib.Topology.Connected.PathConnected
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 [])
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
⊢ Joined l.prod l'.prod

Tactic:
induction h with
  | nil => rfl
  | cons h₁ _ h₂ => exact h₁.mul h₂

Premises used: Fin.cons
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
G : Type u_4
inst : Inv G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
x y : G
h : Joined x y
⊢ Joined x⁻¹ y⁻¹

Tactic:
⟨h.somePath.inv⟩

Premises used: Path.inv, Joined.somePath, Nonempty.intro, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
b : ZerothHomotopy X
x : X
⊢ ∃ (a : X), Eq (α := ZerothHomotopy X) (mk a) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) x)

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
b : ZerothHomotopy X
x : X
⊢ ∃ (a : X), Eq (α := ZerothHomotopy X) (mk a) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) x)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : ZerothHomotopy X
obtain : ∀ (x : X), motive (ZerothHomotopy.mk x)
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Premises used: ZerothHomotopy.mk_surjective, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : X
⊢ motive (ZerothHomotopy.mk x)

Tactic:
mk x
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : X
⊢ motive (ZerothHomotopy.mk x)

Tactic:
exact mk x
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
p : Path x y
⊢ Eq (α := ZerothHomotopy X) (mk x) (mk y)

Tactic:
Quotient.sound ⟨p⟩

Premises used: ZerothHomotopy, Nonempty.intro, Quotient.sound, ZerothHomotopy.mk
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsQuotientMap.{u_1, u_1} (X := X) (Y := ZerothHomotopy X) mk

Tactic:
isQuotientMap_quotient_mk'

Premises used: ZerothHomotopy, isQuotientMap_quotient_mk', Quotient.mk', ZerothHomotopy.mk
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y z : X
ι : Type u_3
inst_2 : Nonempty X
⊢ Nonempty.{u_1 + 1} (ZerothHomotopy X)

Tactic:
⟨.mk (Classical.arbitrary _)⟩

Premises used: Nonempty.intro, Classical.arbitrary, ZerothHomotopy.mk
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
T : Type u_4
f : X → T
hf : ∀ ⦃x y : X⦄ (x_1 : Path x y), f x = f y
x : X
⊢ lift f hf (mk x) = f x

Tactic:
rfl

Premises used: ZerothHomotopy.lift, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
rcases :
  ∀ (γ : Path x y) (γ_in : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)),
    x ∈ F ∧ y ∈ F
⊢ x ∈ F ∧ y ∈ F

Tactic:
rcases h with ⟨γ, γ_in⟩
-- Module: Mathlib.Topology.Connected.PathConnected
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)
right : Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
⊢ Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X) ∧
    Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.PathConnected
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)

Tactic:
apply γ_in
-- Module: Mathlib.Topology.Connected.PathConnected
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) 1 : X)

Tactic:
apply γ_in
-- Module: Mathlib.Topology.Connected.PathConnected
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)

Tactic:
have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
-- Module: Mathlib.Topology.Connected.PathConnected
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)
this :
  Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 0 : X) ∧
    Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) 1 : X)
⊢ x ∈ F ∧ y ∈ F

Tactic:
simpa using this
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F

Tactic:
h.mem.1

Premises used: JoinedIn.mem, And.left
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ y ∈ F

Tactic:
h.mem.2

Premises used: JoinedIn.mem, And.right
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
t : (↑I : Type)
⊢ Membership.mem (α := X) F ((h.somePath (F := F) : (a : (↑I : Type)) → X) t : X)

Tactic:
Classical.choose_spec h t

Premises used: Set.Mem, Classical.choose_spec
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Continuous[_, instTopologicalSpaceSubtype] fun (t : (↑I : Type)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ F) ((h.somePath (F := F) : (a : (↑I : Type)) → X) t) ⋯

Tactic:
fun_prop
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Subtype.mk (p := fun (x : X) ↦ x ∈ F) ((h.somePath (F := F) : (a : (↑I : Type)) → X) 0) ⋯ =
    Subtype.mk (p := fun (x : X) ↦ x ∈ F) x ⋯

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Subtype.mk (p := fun (x : X) ↦ x ∈ F) ((h.somePath (F := F) : (a : (↑I : Type)) → X) 1) ⋯ =
    Subtype.mk (p := fun (x : X) ↦ x ∈ F) y ⋯

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
f : ℝ → X
hf : ContinuousOn f I
h₀ : f 0 = x
h₁ : f 1 = y
hF : f '' I ⊆ F
⊢ JoinedIn F x y

Tactic:
⟨Path.ofLine hf h₀ h₁, fun t => hF <| Path.ofLine_mem hf h₀ h₁ t⟩

Premises used: JoinedIn, Path.ofLine_mem, Path.ofLine, Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ Joined x y

Tactic:
⟨h.somePath⟩

Premises used: JoinedIn.somePath, Nonempty.intro, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
x_in : x ∈ F
y_in : y ∈ F
h : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x x_in) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y y_in)
⊢ ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((h.somePath.map ⋯ : (a : (↑I : Type)) → X) t : X)

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ JoinedIn univ x y ↔ Joined x y

Tactic:
simp [JoinedIn, Joined, exists_true_iff_nonempty]

Premises used: JoinedIn, exists_true_iff_nonempty, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
U V : Set X
h : JoinedIn U x y
hUV : U ⊆ V
⊢ JoinedIn V x y

Tactic:
⟨h.somePath, fun t => hUV (h.somePath_mem t)⟩

Premises used: JoinedIn, JoinedIn.somePath, JoinedIn.somePath_mem, Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
⊢ JoinedIn F x x

Tactic:
⟨Path.refl x, fun _t => h⟩

Premises used: JoinedIn, Exists.intro, Path.refl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F

Tactic:
obtain ⟨hx, hy⟩ := h.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
⊢ y ∈ F

Tactic:
obtain ⟨hx, hy⟩ := h.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
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
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)
⊢ JoinedIn F y x

Tactic:
simp_all only [joinedIn_iff_joined]

Premises used: joinedIn_iff_joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
hx_1 : x ∈ F
hy_1 : y ∈ F
h : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1)
hx : x ∈ F
hy : y ∈ F
⊢ Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1)

Tactic:
h.symm

Premises used: Joined.symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
hx_1 : x ∈ F
hy_1 : y ∈ F
h : Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1)
hx : x ∈ F
hy : y ∈ F
⊢ Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) y hy_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1)

Tactic:
exact h.symm

Premises used: Joined.symm
-- Module: Mathlib.Topology.Connected.PathConnected
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
⊢ x ∈ F

Tactic:
obtain ⟨hx, hy⟩ := hxy.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
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
⊢ y ∈ F

Tactic:
obtain ⟨hx, hy⟩ := hxy.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
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 : y ∈ F
⊢ y ∈ F

Tactic:
obtain ⟨hx, hy⟩ := hyz.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
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
⊢ z ∈ F

Tactic:
obtain ⟨hx, hy⟩ := hyz.mem

Premises used: JoinedIn.mem
-- Module: Mathlib.Topology.Connected.PathConnected
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
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)
⊢ JoinedIn F x z

Tactic:
simp_all only [joinedIn_iff_joined]

Premises used: joinedIn_iff_joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hx_1 : x ∈ F
hy_1 : y ∈ F
hy_2 : z ∈ F
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_2)
hx_2 : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) z hy_2)

Tactic:
hxy.trans hyz

Premises used: Joined.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
F : Set X
hx_1 : x ∈ F
hy_1 : y ∈ F
hy_2 : z ∈ F
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_2)
hx_2 : x ∈ F
hx : y ∈ F
hy : z ∈ F
⊢ Joined (Subtype.mk (p := fun (x : X) ↦ x ∈ F) x hx_1) (Subtype.mk (p := fun (x : X) ↦ x ∈ F) z hy_2)

Tactic:
exact hxy.trans hyz

Premises used: Joined.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ ContinuousMap.toFun (X := (↑I : Type))
      { toFun := piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x),
        continuous_toFun := ⋯ : C((↑I : Type), X) }
      0 =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ ContinuousMap.toFun (X := (↑I : Type))
      { toFun := piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x),
        continuous_toFun := ⋯ : C((↑I : Type), X) }
      1 =
    y

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
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))
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 := ⋯, source' := ⋯, target' := ⋯ } :
            (a : (↑I : Type)) → X)
          t :
        X)
⊢ JoinedIn F x y

Tactic:
refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩