awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hy : y ∈ s
⊢ ∃ (γ : 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
-- 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 : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
hp₂ :
  ∃ (γ : Path (Fin.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)
snoc :
  ∀ (γ₀ : Path (Fin.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 (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)) ↦ 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₂
-- 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 : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (Fin.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)
snoc :
  ∀ (γ₁ : Path y x) (hγ₁ : ∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ₁ : (a : (↑I : Type)) → X) t : X)),
    ∃ (γ : 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)) ↦ 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

Premises used: IsPathConnected.joinedIn
-- 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 : 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)
⊢ range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ⊆ s

Tactic:
rw [← range_subset_iff] at hγ₁

Premises used: Set.range_subset_iff
-- 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 : 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
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
⊢ ∃ (γ : 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:
use γ₀.trans γ₁

Premises used: Path.trans
-- 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 : 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
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)
⊢ 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:
simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]

Premises used: Set.mem_union, and_true, Set.union_subset_iff, Path.source_mem_range, Path.trans_range, or_true
-- 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 : 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
h₁ : range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) ⊆ s
h₂ : range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X) ⊆ s
h₃ h₄ h₅ :
  ∀ (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)
h₆ h₇ h₈ h₉ h₁₀ h₁₁ :
  ∀ (i : Fin n),
    p i ∉ range (ι := (↑I : Type)) (⇑γ₀ : (a : (↑I : Type)) → X) →
      Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ₁ : (a : (↑I : Type)) → X)) (p i)
⊢ (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:
tauto
-- 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
hx : x ∈ s
snoc :
  ∀ (x : X) (hp : ∀ (i : Fin 0), i.elim0 ∈ s) (hx : x ∈ s),
    ∃ (γ : 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
snoc₁ :
  ∀ {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),
    ∃ (γ : 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)
⊢ ∃ (γ : 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)

Tactic:
induction p using snocInduction generalizing x with
  | elim0 =>
    simp only [snoc_zero]
    use Path.refl x
    simp [hx]
  | @snoc n p y hp₂ =>
    simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
    obtain ⟨hp, hy⟩ := hp
    specialize hp₂ y hp hy
    obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
    obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
    rw [← range_subset_iff] at hγ₁
    use γ₀.trans γ₁
    simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]
    tauto

Premises used: Set.mem_union, Fin.snoc_castSucc, and_true, Set.union_subset_iff, Path.cast_coe, Fin.snoc_apply_zero, Fin.snoc, Fin.snoc_zero, Path.source_mem_range, Path.trans_range, Set.range_subset_iff, Path.refl, or_true, Fin.snoc_last, Fin.elim0, 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 : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
rcases :
  ∀ (γ : Path (p 0) (p (last n)))
    (hγ :
      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)),
    ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
      (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
        ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
      ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩

Premises used: IsPathConnected.exists_path_through_family
-- 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
γ : Path (p 0) (p (last n))
hγ :
  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)
⊢ range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s

Tactic:
rcases hγ with ⟨h₁, h₂⟩
-- 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
γ : Path (p 0) (p (last n))
hγ :
  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)
h₁ : 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:
rcases hγ with ⟨h₁, h₂⟩
-- 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
γ : Path (p 0) (p (last n))
h₁ : range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ (y : (↑I : Type)), (γ : (a : (↑I : Type)) → X) y = p i
⊢ ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)

Tactic:
rw [range_subset_iff] at h₁

Premises used: Set.range_subset_iff
-- 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
γ : Path (p 0) (p (last n))
h₁ : range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s
h₂ : ∀ (i : Fin (n + 1)), ∃ (y : (↑I : Type)), (γ : (a : (↑I : Type)) → X) y = p i
h₃ : ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)
⊢ ∀ (i : Fin (n + 1)), ∃ (y : (↑I : Type)), (γ : (a : (↑I : Type)) → X) y = p i

Tactic:
rw [range_subset_iff] at h₁

Premises used: Set.range_subset_iff
-- 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
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)
h₂ : ∀ (i : Fin (n + 1)), ∃ (y : (↑I : Type)), (γ : (a : (↑I : Type)) → X) y = p i
choose! :
  ∀ (t : (i : Fin (n + 1)) → (↑I : Type)) (ht : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i),
    ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
      (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
        ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
      ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
choose! t ht using h₂
-- 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
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)
t : (i : Fin (n + 1)) → (↑I : Type)
ht : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
      ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
⟨γ, t, h₁, ht⟩

Premises used: And.intro, Exists.intro
-- 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
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)
t : (i : Fin (n + 1)) → (↑I : Type)
ht : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    (∀ (t : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) t : X)) ∧
      ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i

Tactic:
exact ⟨γ, t, h₁, ht⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
mp : PathConnectedSpace X → Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)
mpr : Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X) → PathConnectedSpace X
⊢ PathConnectedSpace X ↔ Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)

Tactic:
⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩

Premises used: Iff.mpr, Subsingleton.intro, And.intro, PathConnectedSpace.nonempty, nonempty_quotient_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
mp : ∀ (a b : ZerothHomotopy X), a = b
⊢ Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)

Tactic:
refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a : ZerothHomotopy X
x : X
b : ZerothHomotopy X
y : X
⊢ Eq (α := ZerothHomotopy X) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) x) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) y)

Tactic:
Quotient.sound (PathConnectedSpace.joined x y)

Premises used: ZerothHomotopy, Quotient.sound, PathConnectedSpace.joined
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a : ZerothHomotopy X
x : X
b : ZerothHomotopy X
y : X
⊢ Eq (α := ZerothHomotopy X) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) x) (Quot.mk (⇑(pathSetoid X) : X → X → Prop) y)

Tactic:
exact Quotient.sound (PathConnectedSpace.joined x y)

Premises used: Quotient.sound
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : Nonempty.{u_1 + 1} (Quotient (pathSetoid X))
h' : Subsingleton.{u_1 + 1} (Quotient (pathSetoid X))
⊢ PathConnectedSpace X

Tactic:
⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩

Premises used: PathConnectedSpace.mk, Quotient.mk, Quotient.exact, Iff.mp, Subsingleton.elim, nonempty_quotient_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
h : Nonempty.{u_1 + 1} (Quotient (pathSetoid X))
h' : Subsingleton.{u_1 + 1} (Quotient (pathSetoid X))
⊢ PathConnectedSpace X

Tactic:
exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩
-- 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
inst_2 inst_3 : PathConnectedSpace X
⊢ Subsingleton.{u_1 + 1} (ZerothHomotopy X)

Tactic:
(pathConnectedSpace_iff_zerothHomotopy.1 inferInstance).2

Premises used: inferInstance, And.right, Iff.mp, pathConnectedSpace_iff_zerothHomotopy
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ PathConnectedSpace X ↔ IsPathConnected.{u_1} (X := X) univ

Tactic:
simp [pathConnectedSpace_iff, isPathConnected_iff, nonempty_iff_univ_nonempty]

Premises used: isPathConnected_iff, pathConnectedSpace_iff, Set.nonempty_iff_univ_nonempty
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
rw : IsPathConnected F ↔ IsPathConnected.{u_1} (X := (↑F : Type u_1)) univ
rw₁ :
  IsPathConnected F ↔
    IsPathConnected.{u_1} (X := X) (image (α := { x : X // x ∈ F }) (Subtype.val (p := fun (x : X) ↦ x ∈ F)) univ)
rw₂ :
  IsPathConnected F ↔
    IsPathConnected.{u_1} (X := X) (range (ι := { x : X // x ∈ F }) (Subtype.val (p := fun (x : X) ↦ x ∈ F)))
rw₃ : IsPathConnected F ↔ IsPathConnected.{u_1} (X := X) {x : X | x ∈ F}
rw₄ rw₅ : IsPathConnected F ↔ IsPathConnected F
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)

Tactic:
rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]

Premises used: Set.image_univ, Set.setOf_mem_eq, Subtype.range_val_subtype, pathConnectedSpace_iff_univ, Topology.IsInducing.subtypeVal, Topology.IsInducing.isPathConnected_iff
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
⊢ IsPathConnected.{u_1} (X := X) univ

Tactic:
pathConnectedSpace_iff_univ.mp inferInstance

Premises used: inferInstance, pathConnectedSpace_iff_univ, Iff.mp
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
rw : IsPathConnected (f '' univ)
⊢ IsPathConnected (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsPathConnected (f '' univ)

Tactic:
isPathConnected_univ.image hf

Premises used: isPathConnected_univ, IsPathConnected.image
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsPathConnected (f '' univ)

Tactic:
exact isPathConnected_univ.image hf

Premises used: isPathConnected_univ, IsPathConnected.image
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst, inst_1] f
rw : IsPathConnected (range f)
⊢ PathConnectedSpace Y

Tactic:
rw [pathConnectedSpace_iff_univ, ← hf.range_eq]

Premises used: Function.Surjective.range_eq, pathConnectedSpace_iff_univ
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst, inst_1] f
⊢ IsPathConnected (range f)

Tactic:
isPathConnected_range hf'

Premises used: isPathConnected_range
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst, inst_1] f
⊢ IsPathConnected (range f)

Tactic:
exact isPathConnected_range hf'

Premises used: isPathConnected_range
-- 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
s : Setoid X
inst_2 : PathConnectedSpace X
⊢ PathConnectedSpace.{u_1} (Quotient s)

Tactic:
Quotient.mk'_surjective.pathConnectedSpace continuous_coinduced_rng

Premises used: Quotient.mk'_surjective, Function.Surjective.pathConnectedSpace, continuous_coinduced_rng
-- Module: Mathlib.Topology.Connected.PathConnected
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x_1 y_1 z : X
ι : Type u_3
F : Set X
x y : ℝ
⊢ Continuous (Y := ℝ) fun (t : (↑I : Type)) ↦ (1 - (↑t : ℝ)) * x + (↑t : ℝ) * y

Tactic:
fun_prop