awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
have inhabit : ∀ (inhabited_h : Inhabited Y), Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
Tactic: inhabit Y
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
have refine_1 : Homotopic (const Y x₀) (const Y x₁) →
  ∀ (H : Homotopy (const Y x₀) (const Y x₁)),
    ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 0 = x₀
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Path (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₀ x₁ : X
inst_2 : Nonempty Y
inhabited_h : Inhabited Y
refine_1 :
  Homotopic (const Y x₀) (const Y x₁) →
    ∀ (H : Homotopy (const Y x₀) (const Y x₁)),
      ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 0 = x₀
⊢ Homotopic (const Y x₀) (const Y x₁) ↔ Joined x₀ x₁
have refine_2 : Homotopic (const Y x₀) (const Y x₁) →
  ∀ (H : Homotopy (const Y x₀) (const Y x₁)),
    ContinuousMap.toFun (X := (↑I : Type)) (((H.comp prodSwap).curry : (a : Y) → C((↑I : Type), X)) default) 1 = x₁
Tactic: refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩,
    fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst : (i : I) → TopologicalSpace (X i)
inst_1 : TopologicalSpace A
f g : (i : I) → ContinuousMap.{u_2, u_3} A (X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : (↑unitInterval : Type)
x : A
hx : x ∈ S
⊢ Eq (α := (i : I) → X i)
    (({
            toFun := fun (x : A) ↦
              ContinuousMap.toFun
                (Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
                  (Homotopy.pi (Y := X) fun (i : I) ↦
                    (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                      ∀ x ∈ S,
                        Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))))
                (t, x),
            continuous_toFun := ⋯ } :
          (a : A) → (i : I) → X i)
        x :
      (i : I) → X i)
    ((ContinuousMap.pi (X := X) f : (a : A) → (i : I) → X i) x : (i : I) → X i)
have dsimp : Eq (α := (i : I) → X i)
  ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
          (Homotopy.pi (Y := X) fun (i : I) ↦
            (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
              ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
        (a : (↑unitInterval : Type) × A) → (i : I) → X i)
      (t, x) :
    (i : I) → X i)
  fun (i : I) ↦ ((f i : (a : A) → X i) x : X i)
Tactic: dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
I : Type u_1
A : Type u_2
X : I → Type u_3
inst : (i : I) → TopologicalSpace (X i)
inst_1 : TopologicalSpace A
f g : (i : I) → ContinuousMap.{u_2, u_3} A (X i)
S : Set A
homotopies : (i : I) → (f i).HomotopyRel (g i) S
t : (↑unitInterval : Type)
x : A
hx : x ∈ S
⊢ Eq (α := (i : I) → X i)
    ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
            (Homotopy.pi (Y := X) fun (i : I) ↦
              (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
          (a : (↑unitInterval : Type) × A) → (i : I) → X i)
        (t, x) :
      (i : I) → X i)
    fun (i : I) ↦ ((f i : (a : A) → X i) x : X i)
have simp : ∀ (x_1 : I),
  Eq.{u_3 + 1} (α := X x_1)
    ((Homotopy.toContinuousMap (f₀ := ContinuousMap.pi (X := X) f) (f₁ := ContinuousMap.pi (X := X) g)
            (Homotopy.pi (Y := X) fun (i : I) ↦
              (homotopies i).toHomotopy (P := fun (f_1 : ContinuousMap.{u_2, u_3} A (X i)) ↦
                ∀ x ∈ S, Eq.{u_3 + 1} (α := X i) ((f_1 : (a : A) → X i) x : X i) ((f i : (a : A) → X i) x : X i))) :
          (a : (↑unitInterval : Type) × A) → (i : I) → X i)
        (t, x) x_1 :
      X x_1)
    ((f x_1 : (a : A) → X x_1) x : X x_1)
Tactic: simp only [funext_iff]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi (X := X) fun (i : ι) ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi (χ := X) γ)
have simp_rw : (pi (X := X) fun (i : ι) ↦ Quotient.mk' (γ i)) = Quotient.mk' (Path.pi (χ := X) γ)
Tactic: simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
simp_rw : (pi (X := X) fun (i : ι) ↦ Quotient.mk' (γ i)) = Quotient.mk' (Path.pi (χ := X) γ)
⊢ (pi (X := X) fun (i : ι) ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi (χ := X) γ)
have simp_rw₁ : (pi (X := X) fun (i : ι) ↦ ⟦γ i⟧) = ⟦Path.pi (χ := X) γ⟧
Tactic: simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
simp_rw : (pi (X := X) fun (i : ι) ↦ Quotient.mk' (γ i)) = Quotient.mk' (Path.pi (χ := X) γ)
simp_rw₁ : (pi (X := X) fun (i : ι) ↦ ⟦γ i⟧) = ⟦Path.pi (χ := X) γ⟧
⊢ (pi (X := X) fun (i : ι) ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi (χ := X) γ)
have simp_rw₂ : Eq (α := Homotopic.Quotient as bs)
  (_root_.Quotient.map (Path.pi (χ := X)) sorry
    (Quotient.choice (α := fun (i : ι) ↦ Path (as i) (bs i)) fun (i : ι) ↦ ⟦γ i⟧))
  ⟦Path.pi (χ := X) γ⟧
Tactic: simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
simp_rw : (pi (X := X) fun (i : ι) ↦ Quotient.mk' (γ i)) = Quotient.mk' (Path.pi (χ := X) γ)
simp_rw₁ : (pi (X := X) fun (i : ι) ↦ ⟦γ i⟧) = ⟦Path.pi (χ := X) γ⟧
simp_rw₂ :
  Eq (α := Homotopic.Quotient as bs)
    (_root_.Quotient.map (Path.pi (χ := X)) ⋯
      (Quotient.choice (α := fun (i : ι) ↦ Path (as i) (bs i)) fun (i : ι) ↦ ⟦γ i⟧))
    ⟦Path.pi (χ := X) γ⟧
⊢ (pi (X := X) fun (i : ι) ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi (χ := X) γ)
have simp_rw₃ : Eq (α := Homotopic.Quotient as bs) (_root_.Quotient.map (Path.pi (χ := X)) sorry ⟦γ⟧) ⟦Path.pi (χ := X) γ⟧
Tactic: simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
a : (i : ι) → Path (bs i) (cs i)
⊢ Eq (α := Homotopic.Quotient as cs) (pi (X := X) γ₀ ⬝ pi (X := X) fun (i : ι) ↦ ⟦a i⟧)
    (pi (X := X) fun (i : ι) ↦
      γ₀ i ⬝ (fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i)
have h : ∀ (a_1 : (i : ι) → Path (as i) (bs i)),
  Eq (α := Homotopic.Quotient as cs)
    (Quotient.trans (x₁ := bs) (pi (X := X) fun (i : ι) ↦ ⟦a_1 i⟧) (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
    (pi (X := X) fun (i : ι) ↦
      Quotient.trans (x₁ := bs i)
        ((fun (i : ι) ↦ (⟦a_1 i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
        ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i))
Tactic: induction γ₀ using Quotient.induction_on_pi
Cleared hypotheses: γ₀
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a_1 : (i : ι) → Path (as i) (bs i)
⊢ Eq (α := Homotopic.Quotient as cs)
    (Quotient.trans (x₁ := bs) (pi (X := X) fun (i : ι) ↦ ⟦a_1 i⟧) (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
    (pi (X := X) fun (i : ι) ↦
      Quotient.trans (x₁ := bs i)
        ((fun (i : ι) ↦ (⟦a_1 i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
        ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i))
have h : Quotient.mk (Path.pi (χ := X) a_1) ⬝ Quotient.mk (Path.pi (χ := X) a) =
  pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i)
Tactic: simp only [Quotient.mk''_eq_mk, pi_lift]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a_1 : (i : ι) → Path (as i) (bs i)
⊢ Quotient.mk (Path.pi (χ := X) a_1) ⬝ Quotient.mk (Path.pi (χ := X) a) =
    pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i)
have h : Eq (α := Homotopic.Quotient as cs) (pi (X := X) fun (i : ι) ↦ Quotient.mk ((a_1 i).trans (a i)))
  (pi (X := X) fun (i : ι) ↦ Quotient.mk (a_1 i) ⬝ Quotient.mk (a i))
Tactic: rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
γ₀ : (i : ι) → Homotopic.Quotient (as i) (bs i)
γ₁ : (i : ι) → Homotopic.Quotient (bs i) (cs i)
⊢ pi (X := X) γ₀ ⬝ pi (X := X) γ₁ = pi (X := X) fun (i : ι) ↦ γ₀ i ⬝ γ₁ i
have h : ∀ (a : (i : ι) → Path (bs i) (cs i)),
  Eq (α := Homotopic.Quotient as cs) (pi (X := X) γ₀ ⬝ pi (X := X) fun (i : ι) ↦ ⟦a i⟧)
    (pi (X := X) fun (i : ι) ↦
      γ₀ i ⬝ (fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (bs i) (cs i)) (Homotopic.setoid (bs i) (cs i)))) i)
Tactic: induction γ₁ using Quotient.induction_on_pi with | _ a =>
  induction γ₀ using Quotient.induction_on_pi
  simp only [Quotient.mk''_eq_mk, pi_lift]
  rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]
  rfl
Cleared hypotheses: γ₁
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
paths : (i : ι) → Homotopic.Quotient (as i) (bs i)
⊢ proj (X := X) i (pi (X := X) paths) = paths i
have h : ∀ (a : (i : ι) → Path (as i) (bs i)),
  Eq.{u_2 + 1} (α := Homotopic.Quotient (as i) (bs i)) (proj (X := X) i (pi (X := X) fun (i : ι) ↦ ⟦a i⟧))
    ((fun (i : ι) ↦ (⟦a i⟧ : Quotient (α := Path (as i) (bs i)) (Homotopic.setoid (as i) (bs i)))) i)
Tactic: induction paths using Quotient.induction_on_pi
Cleared hypotheses: paths
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a : (i : ι) → Path (as i) (bs i)
⊢ proj (X := X) i (pi (X := X) fun (i : ι) ↦ Quotient.mk (a i)) = Quotient.mk (a i)
have h : (Quotient.mk (Path.pi (χ := X) a)).map
    { toFun := fun (p : (i : ι) → X i) ↦ p i, continuous_toFun := sorry : C((i : ι) → X i, X i) } =
  Quotient.mk (a i)
Tactic: rw [proj, pi_lift]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
p : Homotopic.Quotient as bs
⊢ (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i p) = p
have h : ∀ (a : Path as bs), (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i ⟦a⟧) = ⟦a⟧
Tactic: induction p using Quotient.inductionOn
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
a : Path as bs
⊢ (pi (X := fun (i : ι) ↦ X i) fun (i : ι) ↦ proj (X := X) i ⟦a⟧) = ⟦a⟧
have h : Quotient.mk (Path.pi (χ := fun (i : ι) ↦ X i) fun (i : ι) ↦ a.map sorry) = Quotient.mk a
Tactic: simp only [Quotient.mk''_eq_mk, ← Path.Homotopic.Quotient.mk_map, pi_lift]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)
have mk : ∀ (a : Path a₁ a₂) (b : Path b₁ b₂),
  prod (Quotient.mk a) (Quotient.mk b) ⬝ prod r₁ r₂ = prod (Quotient.mk a ⬝ r₁) (Quotient.mk b ⬝ r₂)
Tactic: induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a : Path a₁ a₂
b : Path b₁ b₂
⊢ prod (Quotient.mk a) (Quotient.mk b) ⬝ prod r₁ r₂ = prod (Quotient.mk a ⬝ r₁) (Quotient.mk b ⬝ r₂)
have mk : ∀ (a_1 : Path a₂ a₃) (b_1 : Path b₂ b₃),
  prod (Quotient.mk a) (Quotient.mk b) ⬝ prod (Quotient.mk a_1) (Quotient.mk b_1) =
    prod (Quotient.mk a ⬝ Quotient.mk a_1) (Quotient.mk b ⬝ Quotient.mk b_1)
Tactic: induction r₁, r₂ using Path.Homotopic.Quotient.ind₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projLeft (prod q₁ q₂) = q₁
have mk : ∀ (a : Path a₁ a₂) (b : Path b₁ b₂), projLeft (prod (Quotient.mk a) (Quotient.mk b)) = Quotient.mk a
Tactic: induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projRight (prod q₁ q₂) = q₂
have mk : ∀ (a : Path a₁ a₂) (b : Path b₁ b₂), projRight (prod (Quotient.mk a) (Quotient.mk b)) = Quotient.mk b
Tactic: induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
p : Homotopic.Quotient (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft p) (projRight p) = p
have mk : ∀ (a : Path (a₁, b₁) (a₂, b₂)), prod (projLeft (Quotient.mk a)) (projRight (Quotient.mk a)) = Quotient.mk a
Tactic: induction p using Path.Homotopic.Quotient.ind
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Homotopy.Product (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a : Path (a₁, b₁) (a₂, b₂)
⊢ prod (projLeft (Quotient.mk a)) (projRight (Quotient.mk a)) = Quotient.mk a
have mk : prod (Quotient.mk (a.map sorry)) (Quotient.mk (a.map sorry)) = Quotient.mk a
Tactic: simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.Basic (goal)
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₀ ≫ F.h = f₀
have w : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₀ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₀ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.Basic (goal)
Goal:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₁ ≫ F.h = f₁
have w : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (ι₁ ≫ F.h) :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.Basic (goal)
Goal:
X Y Z : TopCat
f₀ f₁ : X ⟶ Y
g₀ g₁ : Y ⟶ Z
G : Homotopy g₀ g₁
F : Homotopy f₀ f₁
⊢ (G.comp F).h = X ◁ lift (𝟙 I) (𝟙 I) ≫ Iso.inv (α_ X I I) ≫ F.h ▷ I ≫ G.h
have w : ∀ (x : (↑(tensorObj (𝒞 := instCategory) X I) : Type u)),
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (G.comp F).h :
          (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (X ◁ lift (𝟙 I) (𝟙 I) ≫ Iso.inv (α_ X I I) ≫ F.h ▷ I ≫ G.h) :
          (a : (↑(X ⊗ I) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
x y : toSSet.obj X _⦋0⦌
e : SSet.Edge x y
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) x)
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)
have obtain : ∀ (x : (↑X : Type u)) (e : SSet.Edge ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x) y),
  Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)
Tactic: obtain ⟨x, rfl⟩ := toSSetObj₀Equiv.symm.surjective x
Cleared hypotheses: x, e
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
y : toSSet.obj X _⦋0⦌
x : (↑X : Type u)
e : SSet.Edge ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x) y
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)
have obtain : ∀ (y : (↑X : Type u))
  (e :
    SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)),
  Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y : toSSet.obj X _⦋0⦌))
Tactic: obtain ⟨y, rfl⟩ := toSSetObj₀Equiv.symm.surjective y
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
x : ZerothHomotopy (↑X : Type u)
⊢ SSet.π₀.lift (X := toSSet.obj X) (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
        x) =
    x
have mk : ∀ (x : (↑X : Type u)),
  Eq (α := ZerothHomotopy (↑X : Type u))
    (SSet.π₀.lift (X := toSSet.obj X) (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)))
      sorry
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) sorry
        (ZerothHomotopy.mk x)))
    (ZerothHomotopy.mk x)
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
x : (toSSet.obj X).π₀
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
      (SSet.π₀.lift (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯ x) =
    x
have mk : ∀ (x : toSSet.obj X _⦋0⦌),
  ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) sorry
      (SSet.π₀.lift (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) sorry
        (SSet.π₀.mk x)) =
    SSet.π₀.mk x
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
⊢ Nonempty.{u + 1} (Unique (ZerothHomotopy (↑X : Type u)))
have rw : Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u)) ∧ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
Tactic: rw [unique_iff_subsingleton_and_nonempty]
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
⊢ Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u)) ∧ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
have left : Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
left : Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u))
⊢ Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u)) ∧ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
have right : Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy (goal)
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
this : Unique (ZerothHomotopy (↑X : Type u)) := Nonempty.some ⋯
⊢ SSet.IsConnected.{u} (toSSet.obj X)
have rw : Nonempty.{u + 1} (Unique (toSSet.obj X).π₀)
Tactic: rw [SSet.isConnected_iff_nonempty_unique]
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) ↔ ∀ᶠ (i : ι) in L, p i ↔ q
have mp : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) → ∀ᶠ (i : ι) in L, p i ↔ q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.IndicatorConstPointwise (goal)
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
mp : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) → ∀ᶠ (i : ι) in L, p i ↔ q
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) ↔ ∀ᶠ (i : ι) in L, p i ↔ q
have mpr : (∀ᶠ (i : ι) in L, p i ↔ q) → Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
Tactic: constructor