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
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
⊢ (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)
have 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)
Tactic: tauto
-- 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
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)
⊢ (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)
have 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)
Tactic: tauto
-- 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), 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)
have snoc : ∀ (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
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
Cleared hypotheses: p, x, hp, hx
-- 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), 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
⊢ ∃ (γ : 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)
have 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)
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
Cleared hypotheses: p, x, hp, hx
-- 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))) (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
have 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
Tactic: rcases h.exists_path_through_family p hp with ⟨γ, hγ⟩
-- 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 : 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)
⊢ ∃ (γ : 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
have h₁ : range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X) ⊆ s
Tactic: rcases hγ with ⟨h₁, h₂⟩
Cleared hypotheses: hγ
-- 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 : 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
⊢ ∃ (γ : 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
have h₂ : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
Tactic: rcases hγ with ⟨h₁, h₂⟩
Cleared hypotheses: hγ
-- 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 : 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
⊢ ∃ (γ : 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
have h₃ : ∀ (y : (↑I : Type)), Membership.mem (α := X) s ((γ : (a : (↑I : Type)) → X) y : X)
Tactic: rw [range_subset_iff] at h₁
Cleared hypotheses: h₁, h₂
-- 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))
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
⊢ ∃ (γ : 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
have 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
Tactic: choose! t ht using h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)
have mp : PathConnectedSpace X → Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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)
⊢ PathConnectedSpace X ↔ Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X)
have mpr : Nonempty.{u_1 + 1} (ZerothHomotopy X) ∧ Subsingleton.{u_1 + 1} (ZerothHomotopy X) → PathConnectedSpace X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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)
have mp : ∀ (a b : ZerothHomotopy X), a = b
Tactic: refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)
have rw : IsPathConnected F ↔ IsPathConnected.{u_1} (X := (↑F : Type u_1)) univ
Tactic: rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
rw : IsPathConnected F ↔ IsPathConnected.{u_1} (X := (↑F : Type u_1)) univ
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)
have rw₁ : IsPathConnected F ↔
  IsPathConnected.{u_1} (X := X) (image (α := { x : X // x ∈ F }) (Subtype.val (p := fun (x : X) ↦ x ∈ F)) univ)
Tactic: rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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)
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)
have rw₂ : IsPathConnected F ↔
  IsPathConnected.{u_1} (X := X) (range (ι := { x : X // x ∈ F }) (Subtype.val (p := fun (x : X) ↦ x ∈ F)))
Tactic: rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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)))
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)
have rw₃ : IsPathConnected F ↔ IsPathConnected.{u_1} (X := X) {x : X | x ∈ F}
Tactic: rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
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}
⊢ IsPathConnected F ↔ PathConnectedSpace.{u_1} (↑F : Type u_1)
have rw₄ : IsPathConnected F ↔ IsPathConnected F
Tactic: rw [pathConnectedSpace_iff_univ, IsInducing.subtypeVal.isPathConnected_iff, image_univ,
    Subtype.range_val_subtype, setOf_mem_eq]
-- 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
inst_2 : PathConnectedSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsPathConnected (range f)
have rw : IsPathConnected (f '' univ)
Tactic: rw [← image_univ]
-- 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
inst_2 : PathConnectedSpace X
f : X → Y
hf : Surjective f
hf' : Continuous[inst, inst_1] f
⊢ PathConnectedSpace Y
have rw : IsPathConnected (range f)
Tactic: rw [pathConnectedSpace_iff_univ, ← hf.range_eq]
-- 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
x y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
⊢ ConnectedSpace X
have rw : ∃ (x : X), connectedComponent x = univ
Tactic: rw [connectedSpace_iff_connectedComponent]
-- 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
x y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
⊢ ∃ (x : X), connectedComponent x = univ
have rcases : ∀ (x : X) (_x_in : Membership.mem (γ := Set X) univ x) (hx : pathComponentIn univ x = univ),
  ∃ (x : X), connectedComponent x = univ
Tactic: rcases isPathConnected_iff_eq.mp (pathConnectedSpace_iff_univ.mp ‹_›) with ⟨x, _x_in, hx⟩
-- 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
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
⊢ ∃ (x : X), connectedComponent x = univ
have h : connectedComponent x = univ
Tactic: use x
-- 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
x_1 y z : X
ι : Type u_3
F : Set X
inst_2 : PathConnectedSpace X
x : X
_x_in : Membership.mem (γ := Set X) univ x
hx : pathComponentIn univ x = univ
⊢ connectedComponent x = univ
have h : univ ⊆ connectedComponent x
Tactic: rw [← univ_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ IsConnected F
have rw : ConnectedSpace.{u_1} (↑F : Type u_1)
Tactic: rw [isConnected_iff_connectedSpace]
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
F : Set X
hF : IsPathConnected F
⊢ ConnectedSpace.{u_1} (↑F : Type u_1)
have hF₁ : PathConnectedSpace.{u_1} (↑F : Type u_1)
Tactic: rw [isPathConnected_iff_pathConnectedSpace] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
have this : IsPathConnected.{u_1} (X := X) univ
Tactic: have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
⊢ ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
have rcases : ∀ (γ : Path (p 0) (p (last n)))
  (h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)),
  ∃ (γ : Path (p 0) (p (last n))),
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set X) (range (ι := (↑I : Type)) (⇑γ : (a : (↑I : Type)) → X)) (p i)
Tactic: rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
have this : IsPathConnected.{u_1} (X := X) univ
Tactic: have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected.{u_1} (X := X) univ
⊢ ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
have rcases : ∀ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type))
  (h : ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i),
  ∃ (γ : Path (p 0) (p (last n))) (t : Fin (n + 1) → (↑I : Type)),
    ∀ (i : Fin (n + 1)), (γ : (a : (↑I : Type)) → X) (t i) = p i
Tactic: rcases this.exists_path_through_family' p fun _i => True.intro with ⟨γ, t, -, h⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ preimage (β := ZerothHomotopy X) mk {mk x} = pathComponent x
have h : ∀ (y : X), Membership.mem (γ := Set X) (preimage (β := ZerothHomotopy X) mk {mk x}) y ↔ y ∈ pathComponent x
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Connected.PathConnected (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Membership.mem (γ := Set X) (preimage (β := ZerothHomotopy X) mk {mk x}) y ↔ y ∈ pathComponent x
have h : Eq (α := ZerothHomotopy X) (mk x) (mk y) ↔ Joined x y
Tactic: rw [mem_preimage, mem_singleton_iff, eq_comm, mem_pathComponent_iff]
-- Lean 4 proof step from Mathlib.Topology.Connected.Separation (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TotallySeparatedSpace X
x y : X
h : x ≠ y
⊢ (fun (x y : X) ↦ ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y
have obtain : ∀ (u v : Set X) (h₁ : IsOpen u) (h₂ : IsOpen v) (h₃ : x ∈ u) (h₄ : y ∈ v),
  Set.univ ⊆ u ∪ v →
    ∀ (h₅ : Disjoint u v), ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: obtain ⟨u, v, h₁, h₂, h₃, h₄, _, h₅⟩ := isTotallySeparated_univ trivial trivial h
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
⊢ TotallyDisconnectedSpace (α ⊕ β)
have refine : ∀ s ⊆ univ, ∀ (hs : IsPreconnected s), s.Subsingleton
Tactic: refine ⟨fun s _ hs => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
s : Set (α ⊕ β)
h : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton
have inl : ∀ (t : Set α) (ht : IsPreconnected t),
  Subset (α := Set (α ⊕ β)) (Sum.inl '' t) univ →
    ∀ (hs : IsPreconnected (α := α ⊕ β) (Sum.inl '' t)), Set.Subsingleton (α := α ⊕ β) (Sum.inl '' t)
Tactic: obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isPreconnected_iff.1 hs
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s_1 t u v : Set α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
s : Set (α ⊕ β)
h : s ⊆ univ
hs : IsPreconnected s
inl :
  ∀ (t : Set α) (ht : IsPreconnected t),
    Subset (α := Set (α ⊕ β)) (Sum.inl '' t) univ →
      ∀ (hs : IsPreconnected (α := α ⊕ β) (Sum.inl '' t)), Set.Subsingleton (α := α ⊕ β) (Sum.inl '' t)
⊢ s.Subsingleton
have inr : ∀ (t : Set β) (ht : IsPreconnected t),
  Subset (α := Set (α ⊕ β)) (Sum.inr '' t) univ →
    ∀ (hs : IsPreconnected (α := α ⊕ β) (Sum.inr '' t)), Set.Subsingleton (α := α ⊕ β) (Sum.inr '' t)
Tactic: obtain ⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩ := Sum.isPreconnected_iff.1 hs
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Topology.Connected.TotallyDisconnected (goal)
Goal:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace.{u_2} (X i)
⊢ TotallyDisconnectedSpace ((i : ι) × X i)
have refine : ∀ s ⊆ univ, ∀ (hs : IsPreconnected s), s.Subsingleton
Tactic: refine ⟨fun s _ hs => ?_⟩