awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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))
⊢ 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:
congr 2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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) ⋯ :
      { x : Fin 2 → ℝ // Membership.mem (γ := Set (Fin 2 → ℝ)) (_root_.stdSimplex ℝ (Fin 2)) x })
⊢ 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))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
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 })

Tactic:
(SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_

Premises used: SimplexCategory.toTopHomeo_naturality_apply, CategoryTheory.CosimplicialObject.δ, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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) ⋯)
⊢ 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 })

Tactic:
refine (SimplexCategory.toTopHomeo_naturality_apply _ _).trans ?_

Premises used: SimplexCategory.toTopHomeo_naturality_apply, Eq.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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) ⋯)
⊢ 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) ⋯)

Tactic:
rw [Subsingleton.elim (⦋0⦌.toTopHomeo default) (stdSimplex.vertex 0), stdSimplex.map_vertex]

Premises used: Inhabited.default, stdSimplex.vertex, SimplexCategory.mk, SimplexCategory.toTopHomeo, Subsingleton.elim, OfNat.ofNat, stdSimplex.map_vertex, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ 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) ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
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))
    (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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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))
⊢ 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_arg ULift.up.{u} this

Premises used: congr_arg, ULift.up
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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))
⊢ 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:
exact congr_arg ULift.up.{u} this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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)
⊢ 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⦌)

Tactic:
apply yonedaEquiv.symm.injective

Premises used: SSet.yonedaEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
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
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⦌)
⊢ 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:
trans stdSimplex.δ 1 ≫ toSSetObjI

Premises used: CategoryTheory.CosimplicialObject.δ, SSet.stdSimplex, SSet.stdSimplex.toSSetObjI, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ (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:
simp [← yonedaEquiv_symm_comp, stdSimplex.δ_one_eq_const]

Premises used: SSet.yonedaEquiv_symm_comp, SSet.stdSimplex.δ_one_eq_const
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ 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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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)
⊢ 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⦌)

Tactic:
apply yonedaEquiv.symm.injective

Premises used: SSet.yonedaEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
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 1 (op ⦋0⦌)) :
        (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) =
    stdSimplex.δ 0 ≫ toSSetObjI
trans₁ :
  stdSimplex.δ 0 ≫ 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⦌) 1 :
        TopCat.toSSet.obj TopCat.I _⦋0⦌)
⊢ 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:
trans stdSimplex.δ 0 ≫ toSSetObjI

Premises used: CategoryTheory.CosimplicialObject.δ, SSet.stdSimplex, SSet.stdSimplex.toSSetObjI, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ (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⦌)) =
    stdSimplex.δ 0 ≫ toSSetObjI

Tactic:
simp [← yonedaEquiv_symm_comp, stdSimplex.δ_zero_eq_const]

Premises used: SSet.stdSimplex.δ_zero_eq_const, SSet.yonedaEquiv_symm_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ stdSimplex.δ 0 ≫ 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⦌) 1 :
        TopCat.toSSet.obj TopCat.I _⦋0⦌)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
rw :
  ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₀

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv, CategoryTheory.Functor.Monoidal.μ_δ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
h_fst :
  (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
h_snd :
  (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
⊢ (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
rw :
  ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₁

Tactic:
rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv, CategoryTheory.Functor.Monoidal.μ_δ