awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
mp : IsPathConnected F → ∃ x ∈ F, pathComponentIn F x = F
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F
have mpr : (∃ x ∈ F, pathComponentIn F x = F) → IsPathConnected F
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ ∃ x ∈ F, pathComponentIn F x = F
have right : pathComponentIn F x = F
Tactic: use x, x_in
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ IsPathConnected F
have right : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
Tactic: use x, x_in
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ pathComponentIn F x = F
have right : ∀ (y : X), y ∈ pathComponentIn F x ↔ y ∈ F
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ JoinedIn F x y
have right : ∀ (y_in : y ∈ pathComponentIn F x), JoinedIn F x y
Tactic: rwa [← h] at y_in
Cleared hypotheses: y_in
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
hF : IsPathConnected F
f : X → Y
hf : ContinuousOn f F
⊢ IsPathConnected (f '' F)
have rcases : ∀ (x : X) (x_in : x ∈ F) (hx : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y), IsPathConnected (f '' F)
Tactic: rcases hF with ⟨x, x_in, hx⟩
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
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
⊢ IsPathConnected (f '' F)
have right : ∀ ⦃y : Y⦄, y ∈ f '' F → JoinedIn (f '' F) (f x) y
Tactic: use f x, mem_image_of_mem f x_in
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
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)
have right : ContinuousOn f (range (ι := (↑I : Type)) (⇑(sorry.somePath (F := F)) : (a : (↑I : Type)) → X))
Tactic: refine ⟨(hx y_in).somePath.map' ?_, fun t ↦ ⟨_, (hx y_in).somePath_mem t, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
⊢ IsPathConnected F ↔ IsPathConnected (f '' F)
have 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)
Tactic: simp only [IsPathConnected, forall_mem_image, exists_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
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)
have refine : ∀ (x : X) (hx : x ∈ F) (y : X) (hy : y ∈ F), JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)
Tactic: refine exists_congr fun x ↦ and_congr_right fun hx ↦ forall₂_congr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
F : Set X
f : X → Y
hf : IsInducing f
x : X
hx : x ∈ F
y : X
hy : y ∈ F
⊢ JoinedIn F x y ↔ JoinedIn (f '' F) (f x) (f y)
have rw : JoinedIn F x y ↔ JoinedIn F x y
Tactic: rw [hf.joinedIn_image hx hy]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPathConnected.{u_1} (X := X) ((⇑h : (a : X) → Y) ⁻¹' s) ↔ IsPathConnected s
have rw : IsPathConnected.{u_1} (X := X) ((⇑h.symm : (a : Y) → X) '' s) ↔ IsPathConnected s
Tactic: rw [← Homeomorph.image_symm]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPathConnected (X := X) {x}
have refine : ∀ ⦃y : X⦄, Membership.mem (γ := Set X) {x} y → JoinedIn {x} x y
Tactic: refine ⟨x, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
have refine : ∀ (t t' : (↑I : Type)), Membership.mem (α := X) F (((γ.truncateOfLE sorry).cast sorry sorry : (a : (↑I : Type)) → X) t' : X)
Tactic: refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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 (((γ.truncateOfLE ⋯).cast ⋯ ⋯ : (a : (↑I : Type)) → X) t' : X)
have dsimp : Membership.mem (α := X) F ((γ.extend : (a : ℝ) → X) (min (max (↑t' : ℝ) 0) (↑t : ℝ)) : X)
Tactic: dsimp [Path.truncateOfLE, Path.truncate]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponent x)
have rw : IsPathConnected (pathComponentIn univ x)
Tactic: rw [← pathComponentIn_univ]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
⊢ IsPathConnected (U ∪ V)
have rcases : ∀ (x : X) (xU : x ∈ U) (xV : x ∈ V), IsPathConnected (U ∪ V)
Tactic: rcases hUV with ⟨x, xU, xV⟩
Cleared hypotheses: hUV
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ IsPathConnected (U ∪ V)
have right : ∀ ⦃y : X⦄, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
Tactic: use x, Or.inl xU
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U W : Set X
hW : IsPathConnected W
hWU : W ⊆ U
⊢ IsPathConnected (X := { x : X // x ∈ U }) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' W)
have 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))
Tactic: rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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))
⊢ IsPathConnected (X := { x : X // x ∈ U }) (Subtype.val (p := fun (x : X) ↦ x ∈ U) ⁻¹' W)
have rwa₁ : IsPathConnected (U ∩ W)
Tactic: rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ ∃ (γ : 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)
have snoc : ∀ (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: cases p using snocCases with | _ p x => ?_
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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)
have snoc : ∀ (hp : (∀ (i : Fin n), p i ∈ s) ∧ 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)
Tactic: simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe,
    Path.target_mem_range, and_true] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
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
⊢ ∃ (γ : 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)
have hp₁ : ∀ (i : Fin n), p i ∈ s
Tactic: obtain ⟨hp, hx⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
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
⊢ ∃ (γ : 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)
have hx : x ∈ s
Tactic: obtain ⟨hp, hx⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ ∃ (γ : Path (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
have 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
Tactic: simp only [snoc_zero]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
⊢ ∃ (γ : 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
have 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
Tactic: use Path.refl x
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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
hp : ∀ (i : Fin (n + 1)), Membership.mem (α := X) s (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y i : X)
hx : x ∈ s
⊢ ∃ (γ : Path (snoc (α := fun (a : Fin (n + 1 + 1)) ↦ X) (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))
          (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y i : X)
have snoc : ∀ (hp : (∀ (i : Fin n), p i ∈ s) ∧ y ∈ s),
  ∃ (γ : Path (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
Tactic: simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
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
⊢ ∃ (γ : Path (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
have hp₁ : ∀ (i : Fin n), p i ∈ s
Tactic: obtain ⟨hp, hy⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
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
⊢ ∃ (γ : Path (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
have hy : y ∈ s
Tactic: obtain ⟨hp, hy⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
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
hy : y ∈ s
⊢ ∃ (γ : Path (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
have hp₃ : ∃ (γ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y),
  range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s ∧
    ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
Tactic: specialize hp₂ y hp hy
Cleared hypotheses: hp₂
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
hp₂ :
  ∃ (γ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y),
    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 (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
have snoc : ∀ (γ₀ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y)
  (hγ₀s : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s)
  (hγ₀p : ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X)) (p i)),
  ∃ (γ : Path (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
Tactic: obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
Cleared hypotheses: hp₂
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y
hγ₀s : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s
hγ₀p : ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X)) (p i)
⊢ ∃ (γ : Path (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
have snoc : ∀ (γ₁ : Path y x) (hγ₁ : ∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ₁ : (a : (↑I : Type)) → X) t : X)),
  ∃ (γ : Path (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
Tactic: obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y
hγ₀s : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s
hγ₀p : ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X)) (p i)
γ₁ : Path y x
hγ₁ : ∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ₁ : (a : (↑I : Type)) → X) t : X)
⊢ ∃ (γ : Path (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
have hγ₂ : range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ⊆ s
Tactic: rw [← range_subset_iff] at hγ₁
Cleared hypotheses: hγ₁
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y
hγ₀s : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s
hγ₀p : ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X)) (p i)
γ₁ : Path y x
hγ₁ : range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ⊆ s
⊢ ∃ (γ : Path (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
have h₁ : range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X) ⊆ s ∧
  (∀ (i : Fin n),
      Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X)) (p i)) ∧
    Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X)) y
Tactic: use γ₀.trans γ₁
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
n_1 : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc (α := fun (a : Fin (n + 1)) ↦ X) p y 0) y
hγ₀s : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s
hγ₀p : ∀ (i : Fin n), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X)) (p i)
γ₁ : Path y x
hγ₁ : range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ⊆ s
⊢ range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X) ⊆ s ∧
    (∀ (i : Fin n),
        Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X)) (p i)) ∧
      Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑(γ₀.trans γ₁) : (a : (↑I : Type)) → X)) y
have h₁ : (range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s ∧
    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)) (p i)
Tactic: simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]