awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Continuous[_, inst] (piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x))

Tactic:
isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h

Premises used: continuous_const, IsClosed.continuous_piecewise_of_specializes, isClosed_singleton
-- 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
⊢ Continuous[_, inst] (piecewise (β := fun (a : (↑I : Type)) ↦ X) {1} (const (↑I : Type) y) (const (↑I : Type) x))

Tactic:
exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h

Premises used: continuous_const, IsClosed.continuous_piecewise_of_specializes, isClosed_singleton
-- 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
t : (↑I : Type)
refine_2 : (if Membership.mem (γ := Set (↑I : Type)) {1} t then const (↑I : Type) y t else const (↑I : Type) x t) ∈ F
⊢ 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)

Tactic:
simp only [Path.coe_mk_mk, piecewise]

Premises used: Path.coe_mk_mk, Set.piecewise
-- 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
t : (↑I : Type)
pos : Membership.mem (γ := Set (↑I : Type)) {1} t → const (↑I : Type) y t ∈ F
neg : t ∉ {1} → const (↑I : Type) x t ∈ F
⊢ (if Membership.mem (γ := Set (↑I : Type)) {1} t then const (↑I : Type) y t else const (↑I : Type) x t) ∈ F

Tactic:
split_ifs
-- 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
t : (↑I : Type)
h_1 : Membership.mem (γ := Set (↑I : Type)) {1} t
⊢ const (↑I : Type) y t ∈ F

Tactic:
assumption
-- 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
t : (↑I : Type)
h_1 : t ∉ {1}
⊢ const (↑I : Type) x t ∈ F

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : Inseparable x y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x y

Tactic:
h.specializes.joinedIn hx hy

Premises used: Inseparable.specializes, Specializes.joinedIn
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
h : JoinedIn F x y
f : X → Y
hf : ContinuousOn f F
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
let ⟨γ, hγ⟩ := h
  ⟨γ.map' <| hf.mono (range_subset_iff.mpr hγ), fun t ↦ mem_image_of_mem _ (hγ t)⟩

Premises used: Iff.mpr, JoinedIn, _private.0.JoinedIn.map_continuousOn.match_1, Set.mem_image_of_mem, Exists.intro, ContinuousOn.mono, Set.image, Set.range_subset_iff, Path.map'
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
F : Set X
h : JoinedIn F x y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
h.map_continuousOn hf.continuousOn

Premises used: Continuous.continuousOn, JoinedIn.map_continuousOn
-- Module: Mathlib.Topology.Connected.PathConnected
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

Tactic:
⟨?_, (.map · hf.continuous)⟩

Premises used: JoinedIn.map, Iff.intro, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Connected.PathConnected
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
refine : JoinedIn (f '' F) (f x) (f y) → JoinedIn F x y
⊢ JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y

Tactic:
refine ⟨?_, (.map · hf.continuous)⟩
-- Module: Mathlib.Topology.Connected.PathConnected
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)
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
⊢ JoinedIn F x y

Tactic:
choose γ' hγ'F hγ' using hγ
-- Module: Mathlib.Topology.Connected.PathConnected
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
rw₂ rw₃ : f x ⤳ f x
⊢ x ⤳ γ' 0

Tactic:
rw [← hf.specializes_iff, hγ', γ.source]

Premises used: Topology.IsInducing.specializes_iff, Path.source
-- Module: Mathlib.Topology.Connected.PathConnected
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

Tactic:
have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
-- Module: Mathlib.Topology.Connected.PathConnected
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
rw₂ rw₃ : f y ⤳ f y
⊢ γ' 1 ⤳ y

Tactic:
rw [← hf.specializes_iff, hγ', γ.target]

Premises used: Topology.IsInducing.specializes_iff, Path.target
-- Module: Mathlib.Topology.Connected.PathConnected
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

Tactic:
have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
-- Module: Mathlib.Topology.Connected.PathConnected
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)

Tactic:
⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩

Premises used: JoinedIn, ContinuousMap.mk, Path.mk, Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
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
refine : Continuous[_, inst] γ'
⊢ JoinedIn F (γ' 0) (γ' 1)

Tactic:
refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
-- Module: Mathlib.Topology.Connected.PathConnected
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
⊢ Continuous[_, inst] γ'

Tactic:
simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ

Premises used: Topology.IsInducing.continuous_iff, Function.comp_def, ContinuousMapClass.map_continuous
-- Module: Mathlib.Topology.Connected.PathConnected
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)

Tactic:
have h : JoinedIn F (γ' 0) (γ' 1) := by
    refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
    simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
-- Module: Mathlib.Topology.Connected.PathConnected
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
h : JoinedIn F (γ' 0) (γ' 1)
⊢ JoinedIn F x y

Tactic:
(h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy

Premises used: Specializes.joinedIn, JoinedIn.trans
-- Module: Mathlib.Topology.Connected.PathConnected
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
h : JoinedIn F (γ' 0) (γ' 1)
⊢ JoinedIn F x y

Tactic:
exact (h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy

Premises used: Specializes.joinedIn, JoinedIn.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
M : Type u_4
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
s t : Set M
a b c d : M
hs : JoinedIn s a b
ht : JoinedIn t c d
⊢ JoinedIn (s * t) (a * c) (b * d)

Tactic:
⟨hs.somePath.mul ht.somePath, fun t ↦ Set.mul_mem_mul (hs.somePath_mem t) (ht.somePath_mem t)⟩

Premises used: JoinedIn, JoinedIn.somePath, Path.mul, JoinedIn.somePath_mem, Exists.intro, Set.mul_mem_mul
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
G : Type u_4
inst : InvolutiveInv G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
s : Set G
a b : G
hs : JoinedIn s a b
⊢ JoinedIn s⁻¹ a⁻¹ b⁻¹

Tactic:
⟨hs.somePath.inv, fun t ↦ Set.inv_mem_inv.mpr (hs.somePath_mem t)⟩

Premises used: Iff.mpr, Path.inv, JoinedIn, Set.inv_mem_inv, JoinedIn.somePath, JoinedIn.somePath_mem, Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ∈ pathComponent y ↔ Joined y x

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ∈ pathComponent x

Tactic:
Joined.refl x

Premises used: Joined.refl, Set.Mem, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ (pathComponent x).Nonempty

Tactic:
⟨x, mem_pathComponent_self x⟩

Premises used: Set.Nonempty, mem_pathComponent_self, Exists.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
⊢ y ∈ pathComponent x

Tactic:
Joined.symm h

Premises used: Set.Mem, Joined.symm, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ∈ pathComponent y ↔ y ∈ pathComponent x

Tactic:
⟨fun h => mem_pathComponent_of_mem h, fun h => mem_pathComponent_of_mem h⟩

Premises used: Iff.intro, mem_pathComponent_of_mem
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
h₁ : ∀ (z : X), z ∈ pathComponent x ↔ z ∈ pathComponent y
⊢ pathComponent x = pathComponent y

Tactic:
ext z
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h₁ : z ∈ pathComponent x → z ∈ pathComponent y
h₂ : z ∈ pathComponent y → z ∈ pathComponent x
⊢ z ∈ pathComponent x ↔ z ∈ pathComponent y

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
h₁ : y ∈ pathComponent z
⊢ z ∈ pathComponent y

Tactic:
rw [pathComponent_symm]

Premises used: pathComponent_symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z

Tactic:
(h.trans h').symm

Premises used: Set.Mem, Joined.symm, Joined.trans, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent x
⊢ y ∈ pathComponent z

Tactic:
exact (h.trans h').symm

Premises used: Joined.symm, Joined.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : z ∈ pathComponent y
h₁ : ∀ (h' : y ∈ pathComponent z), x ∈ pathComponent z
⊢ z ∈ pathComponent x

Tactic:
rw [pathComponent_symm] at h' ⊢

Premises used: pathComponent_symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z

Tactic:
h'.trans h

Premises used: Set.Mem, Joined.trans, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z

Tactic:
exact h'.trans h

Premises used: Joined.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h : (a : (↑I : Type)) → X) 0 = x

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : y ∈ pathComponent x
⊢ (Joined.somePath h : (a : (↑I : Type)) → X) 1 = y

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
simp : ∀ (x_1 : X), (∃ (i : X) (_ : i ∈ connectedComponent x), x_1 ∈ pathComponent i) ↔ x_1 ∈ connectedComponent x
⊢ ⋃ y ∈ connectedComponent x, pathComponent y = connectedComponent x

Tactic:
simp only [Set.ext_iff, mem_iUnion₂]

Premises used: Set.mem_iUnion₂, Set.ext_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ∀ (x_1 : X), (∃ (i : X) (_ : i ∈ connectedComponent x), x_1 ∈ pathComponent i) ↔ x_1 ∈ connectedComponent x

Tactic:
fun z ↦ ⟨fun ⟨y, hy, hz⟩ ↦ connectedComponent_eq hy ▸ pathComponent_subset_component _ hz,
    (⟨z, ·, mem_pathComponent_self z⟩)⟩

Premises used: Membership.mem, Eq.rec, connectedComponent, _private.0.biUnion_connectedComponent_pathComponent_eq.match_2, connectedComponent_eq, mem_pathComponent_self, Iff.intro, pathComponent_subset_component, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ ∀ (x_1 : X), (∃ (i : X) (_ : i ∈ connectedComponent x), x_1 ∈ pathComponent i) ↔ x_1 ∈ connectedComponent x

Tactic:
exact fun z ↦ ⟨fun ⟨y, hy, hz⟩ ↦ connectedComponent_eq hy ▸ pathComponent_subset_component _ hz,
    (⟨z, ·, mem_pathComponent_self z⟩)⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ toConnectedComponents (mk x) = ⟦x⟧

Tactic:
rfl

Premises used: Quotient.map, ZerothHomotopy.toConnectedComponents, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := ZerothHomotopy X) toConnectedComponents

Tactic:
Quotient.map_surjective _ surjective_id

Premises used: ZerothHomotopy, Quotient.map_surjective, ZerothHomotopy.toConnectedComponents, Function.surjective_id, ConnectedComponents
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ pathComponentIn univ x = pathComponent x

Tactic:
simp [pathComponentIn, pathComponent, JoinedIn, Joined, exists_true_iff_nonempty]

Premises used: JoinedIn, exists_true_iff_nonempty, pathComponent, pathComponentIn, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
hyz : Joined y z
hxy : y ∈ pathComponent x
⊢ z ∈ pathComponent x

Tactic:
hxy.trans hyz

Premises used: Set.Mem, Joined.trans, setOf, pathComponent, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
⊢ x ∈ pathComponentIn F x

Tactic:
JoinedIn.refl h

Premises used: JoinedIn, Set.Mem, setOf, pathComponentIn, JoinedIn.refl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
⊢ pathComponentIn F x ⊆ F

Tactic:
fun _ hy ↦ hy.target_mem

Premises used: Set.Subset, JoinedIn.target_mem
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
⊢ (pathComponentIn F x).Nonempty ↔ x ∈ F

Tactic:
⟨fun ⟨_, ⟨γ, hγ⟩⟩ ↦ γ.source ▸ hγ 0, fun hx ↦ ⟨x, mem_pathComponentIn_self hx⟩⟩

Premises used: Membership.mem, Eq.rec, mem_pathComponentIn_self, _private.0.pathComponentIn_nonempty_iff.match_1, Iff.intro, Exists.intro, Path.source, OfNat.ofNat
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
h₁ : ∀ (x_1 : X), x_1 ∈ pathComponentIn F x ↔ x_1 ∈ pathComponentIn F y
⊢ pathComponentIn F x = pathComponentIn F y

Tactic:
ext
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x_1 : X
⊢ x_1 ∈ pathComponentIn F x ↔ x_1 ∈ pathComponentIn F y

Tactic:
⟨h.trans, h.symm.trans⟩

Premises used: JoinedIn.symm, Iff.intro, JoinedIn.trans
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn F y
x_1 : X
⊢ x_1 ∈ pathComponentIn F x ↔ x_1 ∈ pathComponentIn F y

Tactic:
exact ⟨h.trans, h.symm.trans⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F G : Set X
h : F ⊆ G
⊢ pathComponentIn F x ⊆ pathComponentIn G x

Tactic:
fun _ ⟨γ, hγ⟩ ↦ ⟨γ, fun t ↦ h (hγ t)⟩

Premises used: Membership.mem, Set.Subset, pathComponentIn, Exists.intro, _private.0.pathComponentIn_mono.match_1
-- 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
F : Set X
M : Type u_4
inst_2 : Monoid M
inst_3 : TopologicalSpace M
inst_4 : ContinuousMul M
m₁ m₂ : M
hm₁ : Membership.mem (γ := Set M) (pathComponent 1) m₁
hm₂ : Membership.mem (γ := Set M) (pathComponent 1) m₂
⊢ Membership.mem (γ := Set M) (pathComponent 1) (m₁ * m₂)

Tactic:
simpa using hm₁.mul hm₂

Premises used: Joined.mul
-- 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
F : Set X
G : Type u_4
inst_2 : Group G
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
g : G
hg : g ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Submonoid.pathComponentOne G))
⊢ g⁻¹ ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Submonoid.pathComponentOne G))

Tactic:
simpa using hg.inv

Premises used: Joined.inv
-- 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
F : Set X
G : Type u_4
inst_2 : Group G
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
x_1 : G
h : Membership.mem (γ := Subgroup G) (Subgroup.pathComponentOne G) x_1
g : G
γ : Path 1 x_1
⊢ Continuous[_, inst_3] fun (x : (↑I : Type)) ↦ HMul.hMul (β := G) g ((γ : (a : (↑I : Type)) → G) x : G) * g⁻¹

Tactic:
fun_prop
-- 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
F : Set X
G : Type u_4
inst_2 : Group G
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
x_1 : G
h : Membership.mem (γ := Subgroup G) (Subgroup.pathComponentOne G) x_1
g : G
γ : Path 1 x_1
⊢ ContinuousMap.toFun
      { toFun := fun (x : (↑I : Type)) ↦ HMul.hMul (β := G) g ((γ : (a : (↑I : Type)) → G) x : G) * g⁻¹,
        continuous_toFun := ⋯ : C((↑I : Type), G) }
      0 =
    1

Tactic:
simp
-- 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
F : Set X
G : Type u_4
inst_2 : Group G
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
x_1 : G
h : Membership.mem (γ := Subgroup G) (Subgroup.pathComponentOne G) x_1
g : G
γ : Path 1 x_1
⊢ ContinuousMap.toFun
      { toFun := fun (x : (↑I : Type)) ↦ HMul.hMul (β := G) g ((γ : (a : (↑I : Type)) → G) x : G) * g⁻¹,
        continuous_toFun := ⋯ : C((↑I : Type), G) }
      1 =
    g * x_1 * g⁻¹

Tactic:
simp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
mp : IsPathConnected F → ∃ x ∈ F, pathComponentIn F x = F
mpr : (∃ x ∈ F, pathComponentIn F x = F) → IsPathConnected F
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
right : pathComponentIn F x = F
⊢ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
use x, x_in
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
right : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ IsPathConnected F

Tactic:
use x, x_in
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
right : ∀ (y : X), y ∈ pathComponentIn F x ↔ y ∈ F
⊢ pathComponentIn F x = F

Tactic:
ext y
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn F x ↔ y ∈ F

Tactic:
⟨fun hy => hy.mem.2, @h _⟩

Premises used: JoinedIn.mem, And.right, Iff.intro
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
⊢ y ∈ pathComponentIn F x ↔ y ∈ F

Tactic:
exact ⟨fun hy => hy.mem.2, @h _⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
y : X
y_in : y ∈ F
right right₁ right₂ right₃ : ∀ (y_in : y ∈ pathComponentIn F x), JoinedIn F x y
⊢ JoinedIn F x y

Tactic:
rwa [← h] at y_in
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
h : IsPathConnected F
⊢ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y

Tactic:
fun _x x_in _y y_in =>
  let ⟨_b, _b_in, hb⟩ := h
  (hb x_in).symm.trans (hb y_in)

Premises used: _private.0.IsPathConnected.joinedIn.match_1, JoinedIn, JoinedIn.symm, JoinedIn.trans