awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
n : ℕ
x : toSSet.obj X _⦋n⦌
i : Fin (n + 1)
z : (↑(stdSimplex ℝ (Fin (n + 2))) : Type)
⊢ Eq (α := (↑X : Type u))
    ((((X.toSSetObjEquiv (op ⦋n + 1⦌) :
                (a : toSSet.obj X _⦋n + 1⦌) → C((↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type), (↑X : Type u)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (toSSet.obj X) i) :
                  (a : toSSet.obj X _⦋n⦌) → toSSet.obj X _⦋n + 1⦌)
                x) :
            C((↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type)) → (↑X : Type u))
        z :
      (↑X : Type u))
    ((((X.toSSetObjEquiv (op ⦋n⦌) : (a : toSSet.obj X _⦋n⦌) → C((↑(stdSimplex ℝ (Fin (n + 1))) : Type), (↑X : Type u)))
              x :
            C((↑(stdSimplex ℝ (Fin (n + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (n + 1))) : Type)) → (↑X : Type u))
        (stdSimplex.map i.predAbove z) :
      (↑X : Type u))

Tactic:
rfl

Premises used: stdSimplex.map, Set.Mem, Fin.predAbove, dite, ULift.map, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ Eq (α := (↑(SSet.toTop.obj Δ[0]) : Type u))
    ((TopCat.toSSetObj₀Equiv : (a : TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌) → (↑(SSet.toTop.obj Δ[0]) : Type u))
        ((SSet.yonedaEquiv :
              (a : Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) → (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0] _⦋0⦌)
            (sSetTopAdj.unit.app Δ[0]) :
          (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0] _⦋0⦌) :
      (↑(SSet.toTop.obj Δ[0]) : Type u))
    (((TopCat.toSSetObj₀Equiv : TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌ ≃ (↑(SSet.toTop.obj Δ[0]) : Type u)) :
          (a : TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌) → (↑(SSet.toTop.obj Δ[0]) : Type u))
        (((SSet.yonedaEquiv :
                (Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) ≃ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0] _⦋0⦌) :
              (a : Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) → (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0] _⦋0⦌)
            (SSet.const
                ((Equiv.symm TopCat.toSSetObj₀Equiv :
                    (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
                  default) :
              Functor.obj (𝟭 SSet) Δ[0] ⟶ TopCat.toSSet.obj (SSet.toTop.obj Δ[0])) :
          (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0] _⦋0⦌) :
      (↑(SSet.toTop.obj Δ[0]) : Type u))

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ Eq (α := Functor.obj (𝟭 SSet) Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) (sSetTopAdj.unit.app Δ[0])
    (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv :
          (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
        default))

Tactic:
have : sSetTopAdj.unit.app Δ[0] =
      SSet.const (TopCat.toSSetObj₀Equiv.symm default) :=
    SSet.yonedaEquiv.injective (TopCat.toSSetObj₀Equiv.injective (by subsingleton))
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this :
  Eq (α := Functor.obj (𝟭 SSet) Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) (sSetTopAdj.unit.app Δ[0])
    (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv :
          (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
        default))
rw :
  Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
          ((Equiv.symm TopCat.toSSetObj₀Equiv :
              (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
            default) ≫
        TopCat.toSSet.map f :
      Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
        ((Equiv.symm (X.toSSetObjEquiv (op ⦋0⦌)) :
            (a : C((↑(stdSimplex ℝ (Fin (0 + 1))) : Type), (↑X : Type u))) → TopCat.toSSet.obj X _⦋0⦌)
          {
            toFun := fun (x : (↑(stdSimplex ℝ (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type)) ↦
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f :
                  (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
                default,
            continuous_toFun := ⋯ }) :
      Δ[0] ⟶ TopCat.toSSet.obj X)
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
    ((sSetTopAdj.homEquiv Δ[0] X : (a : SSet.toTop.obj Δ[0] ⟶ X) → Δ[0] ⟶ TopCat.toSSet.obj X) f :
      Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑X : Type u)) → TopCat.toSSet.obj X _⦋0⦌)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  f :
                (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
              default :
            (↑X : Type u))) :
      Δ[0] ⟶ TopCat.toSSet.obj X)

Tactic:
rw [Adjunction.homEquiv_unit, TopCat.toSSetObj₀Equiv_symm_apply, this]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, TopCat.toSSetObj₀Equiv_symm_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this :
  Eq (α := Functor.obj (𝟭 SSet) Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) (sSetTopAdj.unit.app Δ[0])
    (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv :
          (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
        default))
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
          ((Equiv.symm TopCat.toSSetObj₀Equiv :
              (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
            default) ≫
        TopCat.toSSet.map f :
      Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
        ((Equiv.symm (X.toSSetObjEquiv (op ⦋0⦌)) :
            (a : C((↑(stdSimplex ℝ (Fin (0 + 1))) : Type), (↑X : Type u))) → TopCat.toSSet.obj X _⦋0⦌)
          {
            toFun := fun (x : (↑(stdSimplex ℝ (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type)) ↦
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f :
                  (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
                default,
            continuous_toFun := ⋯ }) :
      Δ[0] ⟶ TopCat.toSSet.obj X)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ Eq (α := (↑I : Type u))
    ((stdSimplexHomeomorphI : (a : (↑(stdSimplex ℝ (Fin 2)) : Type)) → (↑I : Type u)) (stdSimplex.vertex 0) :
      (↑I : Type u))
    (0 : (↑I : Type u))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ Eq (α := (↑I : Type u))
    ((stdSimplexHomeomorphI : (a : (↑(stdSimplex ℝ (Fin 2)) : Type)) → (↑I : Type u)) (stdSimplex.vertex 1) :
      (↑I : Type u))
    (1 : (↑I : Type u))

Tactic:
rfl

Premises used: Function.update, Set.Mem, Pi.single, dite, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ Eq (α := (↑(stdSimplex ℝ (Fin 2)) : Type))
    ((stdSimplexHomeomorphI.symm : (a : (↑I : Type u)) → (↑(stdSimplex ℝ (Fin 2)) : Type)) 0 :
      (↑(stdSimplex ℝ (Fin 2)) : Type))
    (stdSimplex.vertex 0 : (↑(stdSimplex ℝ (Fin 2)) : Type))

Tactic:
simp [← TopCat.stdSimplexHomeomorphI_vertex_zero]

Premises used: TopCat.stdSimplexHomeomorphI_vertex_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
⊢ Eq (α := (↑(stdSimplex ℝ (Fin 2)) : Type))
    ((stdSimplexHomeomorphI.symm : (a : (↑I : Type u)) → (↑(stdSimplex ℝ (Fin 2)) : Type)) 1 :
      (↑(stdSimplex ℝ (Fin 2)) : Type))
    (stdSimplex.vertex 1 : (↑(stdSimplex ℝ (Fin 2)) : Type))

Tactic:
simp [← TopCat.stdSimplexHomeomorphI_vertex_one]

Premises used: TopCat.stdSimplexHomeomorphI_vertex_one
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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.δ 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)
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (stdSimplex.δ 1 ≫
      (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⦌) 0))

Tactic:
rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]

Premises used: sSetTopAdj_homEquiv_stdSimplex_zero, CategoryTheory.Adjunction.homEquiv_naturality_left
-- 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.δ 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))
⊢ 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)

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.δ 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 })
⊢ 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))

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.δ 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 })

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.δ 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) ⋯)
⊢ 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 })

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.δ 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) ⋯)
⊢ 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) ⋯)

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.δ 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) ⋯)

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.δ 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
-- 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.δ 1)) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
            default)) :
      (↑unitInterval : Type))
    (0 : (↑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.δ 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_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.δ 1)) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑(toTop.obj Δ[0 + 1]) : Type u))
            default)) :
      (↑unitInterval : Type))
    (0 : (↑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.δ 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:
exact congr_arg ULift.up.{u} this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
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)
⊢ 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))

Tactic:
rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]

Premises used: sSetTopAdj_homEquiv_stdSimplex_zero, CategoryTheory.Adjunction.homEquiv_naturality_left