awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (toTop.map (stdSimplex.δ 1) ≫
                    (TopCat.isoOfHomeo
                        (Homeomorph.trans ⦋1⦌.toTopHomeo
                          (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
                (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
              default :
            (↑TopCat.I : Type u))) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have e_y : Eq (α := (↑TopCat.I : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (toTop.map (stdSimplex.δ 1) ≫
            (TopCat.isoOfHomeo
                (Homeomorph.trans ⦋1⦌.toTopHomeo
                  (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
        (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
      default :
    (↑TopCat.I : Type u))
  (0 : (↑TopCat.I : Type u))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
            (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
          ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1)) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
            default)) :
      (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
          (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) ⋯) :
      (↑unitInterval : Type))
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin 2)) : Type))
  (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
        (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
      ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1)) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
        default) :
    (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
      (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) sorry :
    { x : Fin 2 → ℝ // Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x })
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin 2)) : Type))
    (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
        ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1)) :
            (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
          default) :
      (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
    (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
        (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) ⋯ :
      { x : Fin 2 → ℝ // Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x })
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (stdSimplex.map (X := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌)
    (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 1)) :
      (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    (((⦋0⦌.toTopHomeo : (↑(toTop.obj Δ[0]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type)) :
        (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type))
      default))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
    (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) sorry)
Tactic: refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
    (stdSimplex.map (X := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌)
      (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 1)) :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (((⦋0⦌.toTopHomeo : (↑(toTop.obj Δ[0]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type))
        default))
    (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
      (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) ⋯)
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (stdSimplex.vertex
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 1) :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      0))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
    (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 0 1) sorry)
Tactic: rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (hypothesis)
Goal:
⊢ Eq (α := (↑TopCat.I : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (toTop.map (stdSimplex.δ 1) ≫
              (TopCat.isoOfHomeo
                  (Homeomorph.trans ⦋1⦌.toTopHomeo
                    (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
        default :
      (↑TopCat.I : Type u))
    (0 : (↑TopCat.I : Type u))
have this : Eq (α := (↑unitInterval : Type))
  ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
      (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
        ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 1)) :
            (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
          default)) :
    (↑unitInterval : Type))
  (0 : (↑unitInterval : Type))
Tactic: have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 1)).hom) default)) = 0 := by
    rw [← stdSimplexHomeomorphUnitInterval_zero]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (stdSimplex.δ 0 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I : (a : toTop.obj Δ[1] ⟶ TopCat.I) → Δ[1] ⟶ TopCat.toSSet.obj TopCat.I)
        (TopCat.isoOfHomeo
            (Homeomorph.trans ⦋1⦌.toTopHomeo
              (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom)
    (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1))
have rw : Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (toTop.map (stdSimplex.δ 0) ≫
                  (TopCat.isoOfHomeo
                      (Homeomorph.trans ⦋1⦌.toTopHomeo
                        (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
            default :
          (↑TopCat.I : Type u))) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
Tactic: rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  (toTop.map (stdSimplex.δ 0) ≫
                    (TopCat.isoOfHomeo
                        (Homeomorph.trans ⦋1⦌.toTopHomeo
                          (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
                (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
              default :
            (↑TopCat.I : Type u))) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have e_y : Eq (α := (↑TopCat.I : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (toTop.map (stdSimplex.δ 0) ≫
            (TopCat.isoOfHomeo
                (Homeomorph.trans ⦋1⦌.toTopHomeo
                  (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
        (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
      default :
    (↑TopCat.I : Type u))
  (1 : (↑TopCat.I : Type u))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
            (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
          ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0)) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
            default)) :
      (↑unitInterval : Type))
    ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
        (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
          (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) ⋯) :
      (↑unitInterval : Type))
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin 2)) : Type))
  (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
        (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
      ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0)) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
        default) :
    (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
      (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) sorry :
    { x : Fin 2 → ℝ // Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x })
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin 2)) : Type))
    (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
        ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0)) :
            (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
          default) :
      (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
    (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
        (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) ⋯ :
      { x : Fin 2 → ℝ // Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x })
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (stdSimplex.map (X := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌)
    (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 0)) :
      (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    (((⦋0⦌.toTopHomeo : (↑(toTop.obj Δ[0]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type)) :
        (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type))
      default))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
    (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) sorry)
Tactic: refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
    (stdSimplex.map (X := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌)
      (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 0)) :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (((⦋0⦌.toTopHomeo : (↑(toTop.obj Δ[0]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋0⦌.len + 1))) : Type))
        default))
    (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
      (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) ⋯)
have h : Eq (α := (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
  (stdSimplex.vertex
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋0⦌) (SimplexCategory.δ 0) :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋0⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      0))
  (Subtype.mk (p := fun (x : Fin 2 → ℝ) ↦ Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x)
    (Pi.single (M := fun (j : Fin 2) ↦ ℝ) 1 1) sorry)
Tactic: rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (hypothesis)
Goal:
⊢ Eq (α := (↑TopCat.I : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (toTop.map (stdSimplex.δ 0) ≫
              (TopCat.isoOfHomeo
                  (Homeomorph.trans ⦋1⦌.toTopHomeo
                    (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
          (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
        default :
      (↑TopCat.I : Type u))
    (1 : (↑TopCat.I : Type u))
have this : Eq (α := (↑unitInterval : Type))
  ((stdSimplexHomeomorphUnitInterval : (a : (↑(_root_.stdSimplex ℝ (Fin 2)) : Type)) → (↑unitInterval : Type))
      (((⦋1⦌.toTopHomeo : (↑(toTop.obj Δ[1]) : Type u) ≃ₜ (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type)) :
          (a : (↑(toTop.obj Δ[1]) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (⦋1⦌.len + 1))) : Type))
        ((TopCat.Hom.hom (toTop.map (stdSimplex.δ 0)) :
            (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
          default)) :
    (↑unitInterval : Type))
  (1 : (↑unitInterval : Type))
Tactic: have : stdSimplexHomeomorphUnitInterval (⦋1⦌.toTopHomeo
      (((toTop.{u}.map (stdSimplex.δ 0)).hom) default)) = 1 := by
    rw [← stdSimplexHomeomorphUnitInterval_one]
    congr 1
    refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_
    rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]
    rfl
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
        (const 1 0 (op ⦋0⦌)) :
      (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
    ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0 :
      TopCat.toSSet.obj TopCat.I _⦋0⦌)
have a : Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
          (const 1 0 (op ⦋0⦌)) :
        (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0 :
        TopCat.toSSet.obj TopCat.I _⦋0⦌) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
Tactic: apply yonedaEquiv.symm.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
            (const 1 0 (op ⦋0⦌)) :
          (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0 :
          TopCat.toSSet.obj TopCat.I _⦋0⦌) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have trans : (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
        (const 1 0 (op ⦋0⦌)) :
      (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) =
  stdSimplex.δ 1 ≫ toSSetObjI
Tactic: trans stdSimplex.δ 1 ≫ toSSetObjI
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
trans :
  (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
          (const 1 0 (op ⦋0⦌)) :
        (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) =
    stdSimplex.δ 1 ≫ toSSetObjI
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
            (const 1 0 (op ⦋0⦌)) :
          (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0 :
          TopCat.toSSet.obj TopCat.I _⦋0⦌) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have trans₁ : stdSimplex.δ 1 ≫ toSSetObjI =
  (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0 :
      TopCat.toSSet.obj TopCat.I _⦋0⦌)
Tactic: trans stdSimplex.δ 1 ≫ toSSetObjI
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
        (const 1 1 (op ⦋0⦌)) :
      (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
    ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1 :
      TopCat.toSSet.obj TopCat.I _⦋0⦌)
have a : Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
          (const 1 1 (op ⦋0⦌)) :
        (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1 :
        TopCat.toSSet.obj TopCat.I _⦋0⦌) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
Tactic: apply yonedaEquiv.symm.injective