awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
⊢ ConnectedSpace.{u_1} (↑U : Type u_1) ↔ PathConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
pathConnectedSpace_iff_connectedSpace.symm

Premises used: pathConnectedSpace_iff_connectedSpace, Iff.symm
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
U_op : IsOpen[inst] U
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
⊢ ConnectedSpace.{u_1} (↑U : Type u_1) ↔ PathConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
exact pathConnectedSpace_iff_connectedSpace.symm

Premises used: pathConnectedSpace_iff_connectedSpace, Iff.symm
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩

Premises used: LocallyConnectedSpace.mk, forall_imp, Filter.HasBasis.mk, isOpen_isPathConnected_basis
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
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
⊢ LocallyConnectedSpace X

Tactic:
refine ⟨forall_imp (fun x h ↦ ⟨fun s ↦ ?_⟩) isOpen_isPathConnected_basis⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
⟨fun hs ↦ ?_, fun ⟨u, ⟨hu, hxu, _⟩, hus⟩ ↦ mem_nhds_iff.mpr ⟨u, hus, hu, hxu⟩⟩

Premises used: Iff.mpr, mem_nhds_iff, Membership.mem, nhds, _private.0.instLocallyConnectedSpace.match_1, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
refine : ∀ (hs : s ∈ 𝓝 x), ∃ (i : Set X), (IsOpen[inst] i ∧ x ∈ i ∧ IsConnected i) ∧ id i ⊆ s
⊢ 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⟩⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
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
⊢ ∃ (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
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
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:
⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩

Premises used: IsPathConnected.isConnected, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
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:
exact ⟨u, ⟨hu, hxu, hu'.isConnected⟩, hus⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
⟨fun hs ↦ ?_, fun ⟨_, ht⟩ ↦ Filter.mem_of_superset ht.1.1 ht.2⟩

Premises used: _private.0.locPathConnectedSpace_iff_isOpen_pathComponentIn.match_1, Membership.mem, nhds, And.right, And.left, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
refine : ∀ (hs : s ∈ 𝓝 x), ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ 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⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
let : ∀ (u : Set X) (hu : u ⊆ s ∧ IsOpen[inst] u ∧ x ∈ u), ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s
⊢ ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
let ⟨u, hu⟩ := mem_nhds_iff.mp hs
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
u : Set X
hu : u ⊆ s ∧ IsOpen[inst] u ∧ x ∈ u
⊢ ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
⟨pathComponentIn u x, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
      isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩

Premises used: HasSubset.Subset.trans, mem_pathComponentIn_self, pathComponentIn, And.right, And.left, isPathConnected_pathComponentIn, And.intro, IsOpen.mem_nhds, Exists.intro, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
u : Set X
hu : u ⊆ s ∧ IsOpen[inst] u ∧ x ∈ u
⊢ ∃ (i : Set X), (i ∈ 𝓝 x ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨pathComponentIn u x, ⟨(h x u hu.2.1).mem_nhds (mem_pathComponentIn_self hu.2.2),
      isPathConnected_pathComponentIn hu.2.2⟩, pathComponentIn_subset.trans hu.1⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_4
inst : TopologicalSpace X
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
⊢ LocPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen[inst] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x

Tactic:
rw [locPathConnectedSpace_iff_isOpen_pathComponentIn]

Premises used: locPathConnectedSpace_iff_isOpen_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_4
inst : TopologicalSpace X
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
⊢ (∀ (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:
simp_rw [forall_comm (β := Set X), ← imp_forall_iff]

Premises used: forall_comm, imp_forall_iff
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_

Premises used: imp_congr_right, forall_congr'
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_4
inst : TopologicalSpace X
refine :
  ∀ (u : Set X), IsOpen[inst] u → ((∀ (x : X), IsOpen[inst] (pathComponentIn u x)) ↔ ∀ x ∈ u, pathComponentIn u x ∈ 𝓝 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

Tactic:
refine forall_congr' fun u ↦ imp_congr_right fun _ ↦ ?_

Premises used: imp_congr_right, forall_congr'
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_4
inst : TopologicalSpace X
u : Set X
h : IsOpen[inst] u
⊢ (∀ (x : X), IsOpen[inst] (pathComponentIn u x)) ↔ ∀ x ∈ u, pathComponentIn u x ∈ 𝓝 x

Tactic:
⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
    fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
      pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩

Premises used: Iff.mpr, mem_pathComponentIn_self, IsOpen.mem_nhds, Iff.intro, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_4
inst : TopologicalSpace X
u : Set X
h : IsOpen[inst] u
⊢ (∀ (x : X), IsOpen[inst] (pathComponentIn u x)) ↔ ∀ x ∈ u, pathComponentIn u x ∈ 𝓝 x

Tactic:
exact ⟨fun h x hxu ↦ (h x).mem_nhds (mem_pathComponentIn_self hxu),
    fun h x ↦ isOpen_iff_mem_nhds.mpr fun y hy ↦
      pathComponentIn_congr hy ▸ h y <| pathComponentIn_subset hy⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ Continuous[inst, x] f

Tactic:
have hf : Continuous f := continuous_coinduced_rng
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
    isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_coinduced, isOpen_iff_mem_nhds, locPathConnectedSpace_iff_isOpen_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
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
⊢ LocPathConnectedSpace Y

Tactic:
refine locPathConnectedSpace_iff_isOpen_pathComponentIn.mpr fun y u hu ↦
    isOpen_coinduced.mpr <| isOpen_iff_mem_nhds.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_coinduced, isOpen_iff_mem_nhds, locPathConnectedSpace_iff_isOpen_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ x ∈ f ⁻¹' u

Tactic:
have hx' := preimage_mono pathComponentIn_subset hx
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
mem_nhds_iff.mpr ⟨pathComponentIn (f ⁻¹' u) x, ?_,
    (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩

Premises used: Iff.mpr, mem_nhds_iff, mem_pathComponentIn_self, IsOpen.pathComponentIn, pathComponentIn, Set.preimage, And.intro, Exists.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
refine : pathComponentIn (f ⁻¹' u) x ⊆ f ⁻¹' pathComponentIn u y
⊢ f ⁻¹' pathComponentIn u y ∈ 𝓝 x

Tactic:
refine mem_nhds_iff.mpr ⟨pathComponentIn (f ⁻¹' u) x, ?_,
    (hu.preimage hf).pathComponentIn _, mem_pathComponentIn_self hx'⟩

Premises used: Iff.mpr, mem_nhds_iff, mem_pathComponentIn_self, IsOpen.pathComponentIn, pathComponentIn, Set.preimage, And.intro, Exists.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
rw : f '' pathComponentIn (f ⁻¹' u) x ⊆ pathComponentIn u (f x)
⊢ pathComponentIn (f ⁻¹' u) x ⊆ f ⁻¹' pathComponentIn u y

Tactic:
rw [← image_subset_iff, ← pathComponentIn_congr hx]

Premises used: Set.image_subset_iff, pathComponentIn_congr
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 (f ⁻¹' u) x ⊆ pathComponentIn u (f x)

Tactic:
((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn
    ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
    (image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f

Premises used: Set.image_mono, HasSubset.Subset.trans, IsPathConnected.image, mem_pathComponentIn_self, IsPathConnected.subset_pathComponentIn, isPathConnected_pathComponentIn, And.intro, Set.image_preimage_subset, Exists.intro, pathComponentIn_subset, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 (f ⁻¹' u) x ⊆ pathComponentIn u (f x)

Tactic:
exact ((isPathConnected_pathComponentIn hx').image hf).subset_pathComponentIn
    ⟨x, mem_pathComponentIn_self hx', rfl⟩ <|
    (image_mono pathComponentIn_subset).trans <| u.image_preimage_subset f

Premises used: Set.image_mono, HasSubset.Subset.trans, IsPathConnected.image, mem_pathComponentIn_self, IsPathConnected.subset_pathComponentIn, isPathConnected_pathComponentIn, And.intro, Set.image_preimage_subset, Exists.intro, pathComponentIn_subset, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocPathConnectedSpace X
f : X → Y
h : IsQuotientMap f
⊢ LocPathConnectedSpace Y

Tactic:
h.isCoinducing.eq_coinduced ▸ LocPathConnectedSpace.coinduced f

Premises used: LocPathConnectedSpace.coinduced, Eq.rec, Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, Eq.symm
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
r : X → X → Prop
⊢ LocPathConnectedSpace.{u_1} (Quot r)

Tactic:
isQuotientMap_quot_mk.locPathConnectedSpace

Premises used: Topology.IsQuotientMap.locPathConnectedSpace, isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
s : Setoid X
⊢ LocPathConnectedSpace.{u_1} (Quotient s)

Tactic:
isQuotientMap_quotient_mk'.locPathConnectedSpace

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.locPathConnectedSpace
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
rw : ∀ (x : X ⊕ Y) (u : Set (X ⊕ Y)), IsOpen[instTopologicalSpaceSum] u → x ∈ u → pathComponentIn u x ∈ 𝓝 x
⊢ LocPathConnectedSpace (X ⊕ Y)

Tactic:
rw [locPathConnectedSpace_iff_pathComponentIn_mem_nhds]

Premises used: locPathConnectedSpace_iff_pathComponentIn_mem_nhds
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
rw : ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t
⊢ pathComponentIn u x ∈ 𝓝 x

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
inr :
  ∀ (y : Y) (hxu : Sum.inr y ∈ u),
    ∃ t ⊆ pathComponentIn u (Sum.inr y), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inr y ∈ t
⊢ ∃ t ⊆ pathComponentIn u x, IsOpen[instTopologicalSpaceSum] t ∧ x ∈ t

Tactic:
obtain x | y := x
-- Module: Mathlib.Topology.Connected.LocPathConnected
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

Tactic:
⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩

Premises used: Sum.inl, pathComponentIn, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Connected.LocPathConnected
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)
inl₂ : Membership.mem (γ := Set (X ⊕ Y)) (Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x) (Sum.inl x)
⊢ ∃ t ⊆ pathComponentIn u (Sum.inl x), IsOpen[instTopologicalSpaceSum] t ∧ Sum.inl x ∈ t

Tactic:
refine ⟨Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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)
inl₂ : Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ u
⊢ Sum.inl '' pathComponentIn (Sum.inl ⁻¹' u) x ⊆ pathComponentIn u (Sum.inl x)

Tactic:
apply IsPathConnected.subset_pathComponentIn

Premises used: IsPathConnected.subset_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ x ∈ inl ⁻¹' u

Tactic:
hxu

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ x ∈ inl ⁻¹' u

Tactic:
exact hxu
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ IsPathConnected (X := X ⊕ Y) (inl '' pathComponentIn (inl ⁻¹' u) x)

Tactic:
exact (isPathConnected_pathComponentIn (by exact hxu)).image continuous_inl

Premises used: continuous_inl, IsPathConnected.image, isPathConnected_pathComponentIn
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ Membership.mem (γ := Set (X ⊕ Y)) (inl '' pathComponentIn (inl ⁻¹' u) x) (inl x)

Tactic:
⟨x, mem_pathComponentIn_self hxu, rfl⟩

Premises used: Set.Mem, setOf, mem_pathComponentIn_self, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.Connected.LocPathConnected
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
⊢ Membership.mem (γ := Set (X ⊕ Y)) (inl '' pathComponentIn (inl ⁻¹' u) x) (inl x)

Tactic:
exact ⟨x, mem_pathComponentIn_self hxu, rfl⟩
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 ⊆ u

Tactic:
(image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset
-- Module: Mathlib.Topology.Connected.LocPathConnected
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 ⊆ u

Tactic:
exact (image_mono pathComponentIn_subset).trans (u.image_preimage_subset _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Set.image_preimage_subset, pathComponentIn_subset