awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ F.Nonempty ∧ ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y

Tactic:
⟨fun h =>
    ⟨let ⟨b, b_in, _hb⟩ := h; ⟨b, b_in⟩, h.joinedIn⟩,
    fun ⟨⟨b, b_in⟩, h⟩ => ⟨b, b_in, h _ b_in⟩⟩

Premises used: IsPathConnected, _private.0.IsPathConnected.joinedIn.match_1, IsPathConnected.joinedIn, Set.Nonempty, And.intro, Iff.intro, Exists.intro, _private.0.isPathConnected_iff.match_1
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
h : IsPathConnected F
⊢ F.Nonempty

Tactic:
isPathConnected_iff.mp h |>.1

Premises used: isPathConnected_iff, And.left, Iff.mp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
hF : IsPathConnected F
f : X → Y
hf : ContinuousOn f F
rcases : ∀ (x : X) (x_in : x ∈ F) (hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y), IsPathConnected (f '' F)
⊢ IsPathConnected (f '' F)

Tactic:
rcases hF with ⟨x, x_in, hx⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
right : ∀ ⦃y : Y⦄, y ∈ f '' F → JoinedIn (f '' F) (f x) y
⊢ IsPathConnected (f '' F)

Tactic:
use f x, mem_image_of_mem f x_in

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩

Premises used: JoinedIn, JoinedIn.somePath, And.intro, JoinedIn.somePath_mem, Exists.intro, DFunLike.coe, Path.map', rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
right : ContinuousOn f (range (ι := (↑I : Type)) (⇑(⋯.somePath (F := F)) : (a : (↑I : Type)) → X))
⊢ JoinedIn (f '' F) (f x) (f y)

Tactic:
refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ ContinuousOn f (range (ι := (↑I : Type)) (⇑(⋯.somePath (F := F)) : (a : (↑I : Type)) → X))

Tactic:
hf.mono (range_subset_iff.2 (hx y_in).somePath_mem)

Premises used: Iff.mpr, JoinedIn.somePath_mem, ContinuousOn.mono, Set.range_subset_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : ContinuousOn f F
x : X
x_in : x ∈ F
hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
y : X
y_in : y ∈ F
⊢ ContinuousOn f (range (ι := (↑I : Type)) (⇑(⋯.somePath (F := F)) : (a : (↑I : Type)) → X))

Tactic:
exact hf.mono (range_subset_iff.2 (hx y_in).somePath_mem)

Premises used: Iff.mpr, JoinedIn.somePath_mem, ContinuousOn.mono, Set.range_subset_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
hF : IsPathConnected F
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsPathConnected (f '' F)

Tactic:
hF.image' hf.continuousOn

Premises used: Continuous.continuousOn, IsPathConnected.image'
-- 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
hs : IsPathConnected s
ht : IsPathConnected t
⊢ IsPathConnected (s * t)

Tactic:
let ⟨a, ha_mem, ha⟩ := hs; let ⟨b, hb_mem, hb⟩ := ht
  ⟨a * b, mul_mem_mul ha_mem hb_mem, Set.forall_mem_image2.2 fun _x hx _y hy ↦ (ha hx).mul (hb hy)⟩

Premises used: Iff.mpr, IsPathConnected, _private.0.IsPathConnected.joinedIn.match_1, HMul.hMul, Set.forall_mem_image2, JoinedIn.mul, And.intro, 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
hs : IsPathConnected s
a : G
ha_mem : a ∈ s
ha : ∀ ⦃y : G⦄, y ∈ s → JoinedIn s a y
x : G
hx : x ∈ s⁻¹
⊢ JoinedIn s⁻¹ a⁻¹ x

Tactic:
simpa using ha (mem_inv.mp hx) |>.map continuous_inv

Premises used: JoinedIn.map, Iff.mp, ContinuousInv.continuous_inv, Set.mem_inv
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
simp : (∃ x ∈ F, ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y) ↔ ∃ x ∈ F, ∀ ⦃x_1 : X⦄, x_1 ∈ F → JoinedIn (f '' F) (f x) (f x_1)
⊢ IsPathConnected F ↔ IsPathConnected (f '' F)

Tactic:
simp only [IsPathConnected, forall_mem_image, exists_mem_image]

Premises used: IsPathConnected, Set.exists_mem_image, Set.forall_mem_image
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ (∃ x ∈ F, ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y) ↔ ∃ x ∈ F, ∀ ⦃x_1 : X⦄, x_1 ∈ F → JoinedIn (f '' F) (f x) (f x_1)

Tactic:
exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_

Premises used: and_congr_right, exists_congr, forall₂_congr
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
refine : ∀ (x : X) (hx : x ∈ F) (y : X) (hy : y ∈ F), JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)
⊢ (∃ x ∈ F, ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y) ↔ ∃ x ∈ F, ∀ ⦃x_1 : X⦄, x_1 ∈ F → JoinedIn (f '' F) (f x) (f x_1)

Tactic:
refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_

Premises used: and_congr_right, exists_congr, forall₂_congr
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
x : X
hx : x ∈ F
y : X
hy : y ∈ F
rw rw₁ : JoinedIn F x y ↔ JoinedIn F x y
⊢ JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)

Tactic:
rw [hf.joinedIn_image hx hy]

Premises used: Topology.IsInducing.joinedIn_image
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
⊢ IsPathConnected.{u_2} (X := Y) ((⇑h : (a : X) → Y) '' s) ↔ IsPathConnected s

Tactic:
h.isInducing.isPathConnected_iff.symm

Premises used: Homeomorph.isInducing, Iff.symm, Topology.IsInducing.isPathConnected_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
rw : IsPathConnected.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPathConnected s
⊢ IsPathConnected.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsPathConnected s

Tactic:
rw [← Homeomorph.image_symm]

Premises used: Homeomorph.image_symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPathConnected s

Tactic:
h.symm.isPathConnected_image

Premises used: Homeomorph.isPathConnected_image, Homeomorph.symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPathConnected s

Tactic:
exact h.symm.isPathConnected_image

Premises used: Homeomorph.isPathConnected_image, Homeomorph.symm
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
F : Set X
h : IsPathConnected F
x_in : x ∈ F
y_in : y ∈ F
⊢ y ∈ pathComponent x

Tactic:
(h.joinedIn x x_in y y_in).joined

Premises used: Set.Mem, setOf, JoinedIn.joined, pathComponent, IsPathConnected.joinedIn, Joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : IsPathConnected F
x_in : x ∈ F
⊢ F ⊆ pathComponent x

Tactic:
fun _y y_in => h.mem_pathComponent x_in y_in

Premises used: Set.Subset, IsPathConnected.mem_pathComponent
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F s : Set X
hs : IsPathConnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ s ⊆ pathComponentIn F x

Tactic:
fun y hys ↦ (hs.joinedIn x hxs y hys).mono hsF

Premises used: JoinedIn, Set.Mem, setOf, Set.Subset, pathComponentIn, IsPathConnected.joinedIn, JoinedIn.mono
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPathConnected (X := X) {x}

Tactic:
⟨x, rfl, ?_⟩

Premises used: IsPathConnected, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
refine : ∀ ⦃y : X⦄, Membership.mem (γ := Set X) {x} y → JoinedIn {x} x y
⊢ IsPathConnected (X := X) {x}

Tactic:
refine ⟨x, rfl, ?_⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y

Tactic:
JoinedIn.refl rfl

Premises used: rfl, JoinedIn.refl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y

Tactic:
exact JoinedIn.refl rfl

Premises used: rfl, JoinedIn.refl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x_1 : X
h_1 : x_1 ∈ pathComponentIn F x
γ : Path x x_1
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
⊢ JoinedIn (pathComponentIn F x) x x_1

Tactic:
⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩

Premises used: JoinedIn, Path.cast, And.left, Exists.intro, Path.extend_zero, Path.extend_extends', Eq.symm, Path.truncateOfLE, Subtype.property
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x_1 : X
h_1 : x_1 ∈ pathComponentIn F x
γ : Path x x_1
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
refine :
  ∀ (t t' : (↑I : Type)), Membership.mem (α := X) F (((γ.truncateOfLE ⋯).cast ⋯ ⋯ : (a : (↑I : Type)) → X) t' : X)
⊢ JoinedIn (pathComponentIn F x) x x_1

Tactic:
refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x_1 : X
h_1 : x_1 ∈ pathComponentIn F x
γ : Path x x_1
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
t t' : (↑I : Type)
dsimp : Membership.mem (α := X) F ((γ.extend : (a : ℝ) → X) (min (max (↑t' : ℝ) 0) (↑t : ℝ)) : X)
⊢ Membership.mem (α := X) F (((γ.truncateOfLE ⋯).cast ⋯ ⋯ : (a : (↑I : Type)) → X) t' : X)

Tactic:
dsimp [Path.truncateOfLE, Path.truncate]

Premises used: Path.truncate, Path.truncateOfLE
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x_1 : X
h_1 : x_1 ∈ pathComponentIn F x
γ : Path x x_1
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
t t' : (↑I : Type)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (min (max (↑t' : ℝ) 0) (↑t : ℝ))

Tactic:
simp [t.2.1, t.2.2]

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x_1 : X
h_1 : x_1 ∈ pathComponentIn F x
γ : Path x x_1
hγ : ∀ (t : (↑I : Type)), Membership.mem (α := X) F ((γ : (a : (↑I : Type)) → X) t : X)
t t' : (↑I : Type)
⊢ Membership.mem (α := X) F ((γ.extend : (a : ℝ) → X) (min (max (↑t' : ℝ) 0) (↑t : ℝ)) : X)

Tactic:
exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
rw : IsPathConnected (pathComponentIn univ x)
⊢ IsPathConnected (pathComponent x)

Tactic:
rw [← pathComponentIn_univ]

Premises used: pathComponentIn_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponentIn univ x)

Tactic:
isPathConnected_pathComponentIn (mem_univ x)

Premises used: isPathConnected_pathComponentIn, Set.mem_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponentIn univ x)

Tactic:
exact isPathConnected_pathComponentIn (mem_univ x)

Premises used: isPathConnected_pathComponentIn, Set.mem_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
rcases : ∀ (x : X) (xU : x ∈ U) (xV : x ∈ V), IsPathConnected (U ∪ V)
⊢ IsPathConnected (U ∪ V)

Tactic:
rcases hUV with ⟨x, xU, xV⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
right : ∀ ⦃y : X⦄, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
⊢ IsPathConnected (U ∪ V)

Tactic:
use x, Or.inl xU

Premises used: Or.inl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

Tactic:
(hU.joinedIn x xU y yU).mono subset_union_left

Premises used: Set.subset_union_left, IsPathConnected.joinedIn, JoinedIn.mono
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

Tactic:
exact (hU.joinedIn x xU y yU).mono subset_union_left

Premises used: Set.subset_union_left, IsPathConnected.joinedIn, JoinedIn.mono
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Tactic:
(hV.joinedIn x xV y yV).mono subset_union_right

Premises used: Set.subset_union_right, IsPathConnected.joinedIn, JoinedIn.mono
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Tactic:
exact (hV.joinedIn x xV y yV).mono subset_union_right

Premises used: Set.subset_union_right, IsPathConnected.joinedIn, JoinedIn.mono
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
rwa :
  IsPathConnected
    (Set.image (α := { x : X // x ∈ U }) (Subtype.val (p := fun (x : X) ↦ x ∈ U))
      (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' W))
rwa₁ : IsPathConnected (U ∩ W)
rwa₂ rwa₃ rwa₄ rwa₅ : IsPathConnected W
⊢ IsPathConnected (X := { x : X // x ∈ U }) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' W)

Tactic:
rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]

Premises used: Iff.mpr, Set.inter_eq_right, Subtype.image_preimage_val, Topology.IsInducing.subtypeVal, Topology.IsInducing.isPathConnected_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : (i : Fin n) → X
x : X
hp : ∀ (i : Fin (n + 1)), Membership.mem (α := X) s (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)
⊢ ∃ (γ :
    Path (X := X) (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0 : X)
      (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x (last n) : X)),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin (n + 1)),
        Membership.mem (α := X) (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
          (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)

Tactic:
?_
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
snoc :
  ∀ (p : (i : Fin n) → X) (x : X)
    (hp : ∀ (i : Fin (n + 1)), Membership.mem (α := X) s (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)),
    ∃ (γ :
      Path (X := X) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0 : X)
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x (last n) : X)),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        ∀ (i : Fin (n + 1)),
          Membership.mem (α := X) (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
            (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)
⊢ ∃ (γ : Path (p 0) (p (last n))),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)

Tactic:
cases p using snocCases with | _ p x => ?_
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : (i : Fin n) → X
x : X
hp : ∀ (i : Fin (n + 1)), Membership.mem (α := X) s (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)
snoc :
  ∀ (hp : (∀ (i : Fin n), p i ∈ s) ∧ x ∈ s),
    ∃ (γ : Path (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0) x),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
⊢ ∃ (γ :
    Path (X := X) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0 : X)
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x (last n) : X)),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin (n + 1)),
        Membership.mem (α := X) (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x i : X)

Tactic:
simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe,
    Path.target_mem_range, and_true] at hp ⊢

Premises used: Fin.snoc_castSucc, and_true, Path.cast_coe, Path.target_mem_range, Fin.snoc_last, Fin.forall_fin_succ'
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : (i : Fin n) → X
x : X
hp : (∀ (i : Fin n), p i ∈ s) ∧ x ∈ s
⊢ ∀ (i : Fin n), p i ∈ s

Tactic:
obtain ⟨hp, hx⟩ := hp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : (i : Fin n) → X
x : X
hp : (∀ (i : Fin n), p i ∈ s) ∧ x ∈ s
hp₁ : ∀ (i : Fin n), p i ∈ s
⊢ x ∈ s

Tactic:
obtain ⟨hp, hx⟩ := hp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
snoc :
  ∃ (γ : Path x x),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin 0), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) i.elim0
⊢ ∃ (γ : Path (Fin.snoc (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ X) elim0 x 0) x),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin 0), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) i.elim0

Tactic:
simp only [snoc_zero]

Premises used: Fin.snoc_zero
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
h₁ :
  range (ι := (↑I : Type)) (⇑(Path.refl x) : (a : (↑I : Type)) → X) ⊆ s ∧
    ∀ (i : Fin 0),
      Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(Path.refl x) : (a : (↑I : Type)) → X)) i.elim0
⊢ ∃ (γ : Path x x),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin 0), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) i.elim0

Tactic:
use Path.refl x

Premises used: Path.refl
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
⊢ range (ι := (↑I : Type)) (⇑(Path.refl x) : (a : (↑I : Type)) → X) ⊆ s ∧
    ∀ (i : Fin 0),
      Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(Path.refl x) : (a : (↑I : Type)) → X)) i.elim0

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ :
  ∀ (x : X) (hp : ∀ (i : Fin n), p i ∈ s) (hx : x ∈ s),
    ∃ (γ : Path (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0) x),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
x : X
hp : ∀ (i : Fin (n + 1)), Membership.mem (α := X) s (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p y i : X)
hx : x ∈ s
snoc :
  ∀ (hp : (∀ (i : Fin n), p i ∈ s) ∧ y ∈ s),
    ∃ (γ : Path (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) x),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        (∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)) ∧
          Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) y
⊢ ∃ (γ : Path (Fin.snoc (α := fun (a : Fin (n + 1 + 1)) ↦ X) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p y) x 0) x),
    range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
      ∀ (i : Fin (n + 1)),
        Membership.mem (α := X) (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X))
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ X) p y i : X)

Tactic:
simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢

Premises used: Fin.snoc_castSucc, Path.cast_coe, Fin.snoc_apply_zero, Fin.snoc_last, Fin.forall_fin_succ'
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ :
  ∀ (x : X) (hp : ∀ (i : Fin n), p i ∈ s) (hx : x ∈ s),
    ∃ (γ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0) x),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
x : X
hx : x ∈ s
hp : (∀ (i : Fin n), p i ∈ s) ∧ y ∈ s
⊢ ∀ (i : Fin n), p i ∈ s

Tactic:
obtain ⟨hp, hy⟩ := hp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ :
  ∀ (x : X) (hp : ∀ (i : Fin n), p i ∈ s) (hx : x ∈ s),
    ∃ (γ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p x 0) x),
      range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
        ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
x : X
hx : x ∈ s
hp : (∀ (i : Fin n), p i ∈ s) ∧ y ∈ s
hp₁ : ∀ (i : Fin n), p i ∈ s
⊢ y ∈ s

Tactic:
obtain ⟨hp, hy⟩ := hp