awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
h :
  ∀ (x : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)),
    Eq (α := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        (⇑m.toTopHomeo :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) →
            (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (SSet.toTop.map (SSet.stdSimplex.map f))) :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        x)
      (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
        (stdSimplex.map
          (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
        (⇑n.toTopHomeo :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
            (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type))
        x)
⊢ Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑m.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      (⇑n.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)))

Tactic:
ext x : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑m.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      x)
    (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      (⇑n.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type))
      x)

Tactic:
ULift.up_injective (ConcreteCategory.congr_hom ((forget TopCat).congr_map
    (toTopSimplex.hom.naturality f)) x)

Premises used: ULift.up_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑m.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      x)
    (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      (⇑n.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type))
      x)

Tactic:
exact ULift.up_injective (ConcreteCategory.congr_hom ((forget TopCat).congr_map
    (toTopSimplex.hom.naturality f)) x)

Premises used: ULift.up_injective, CategoryTheory.NatTrans.naturality, SSet.toTopSimplex, CategoryTheory.forget, CategoryTheory.Functor.congr_map, TopCat, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)
⊢ Eq (α := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    ((m.toTopHomeo :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) →
            (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (SSet.toTop.map (SSet.stdSimplex.map f)) :
            (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
              (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
          x) :
      (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (stdSimplex.map (X := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
        ((n.toTopHomeo :
            (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
              (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type))
          x) :
      (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)) : Type))

Tactic:
congr_fun (toTopHomeo_naturality f) x

Premises used: stdSimplex.map, SimplexCategory.toTopHomeo_naturality, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
h :
  ∀ (x : (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type)),
    Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
        (⇑m.toTopHomeo.symm :
          (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        (stdSimplex.map
          (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
        x)
      (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
        (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        (⇑n.toTopHomeo.symm :
          (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
        x)
⊢ Eq (α :=
    (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type) →
      (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑m.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑n.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)))

Tactic:
ext x : 1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type)
⊢ Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑m.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      x)
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑n.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      x)

Tactic:
ConcreteCategory.congr_hom ((forget _).congr_map
    (toTopSimplex.inv.naturality f)) _

Premises used: stdSimplex.map, Set.Mem, CategoryTheory.NatTrans.naturality, SSet.toTopSimplex, CategoryTheory.forget, CategoryTheory.Functor.congr_map, ULift.map, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type)
⊢ Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑m.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      x)
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑n.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      x)

Tactic:
exact ConcreteCategory.congr_hom ((forget _).congr_map
    (toTopSimplex.inv.naturality f)) _

Premises used: CategoryTheory.NatTrans.naturality, SSet.toTopSimplex, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
n m : SimplexCategory
f : n ⟶ m
x : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)
⊢ Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    ((m.toTopHomeo.symm :
          (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        (stdSimplex.map
          (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)
          x) :
      (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f)) :
          (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
            (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
        ((n.toTopHomeo.symm :
              (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) →
                (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
            x :
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) :
      (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))

Tactic:
congr_fun (toTopHomeo_symm_naturality f) x

Premises used: SimplexCategory.toTopHomeo_symm_naturality, congr_fun
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
x : (↑X : Type u)
⊢ Continuous.{0, u} (Y := (↑X : Type u)) fun (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
x : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))
h :
  ∀ (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)),
    Eq (α := (↑X : Type u))
      (((fun (x : (↑X : Type u)) ↦
                { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                  continuous_toFun := ⋯ : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
              ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
                x) :
            (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
          x_1 :
        (↑X : Type u))
      ((x : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) x_1 : (↑X : Type u))
⊢ (fun (x : (↑X : Type u)) ↦
        { toFun := fun (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x, continuous_toFun := ⋯ :
          C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
      ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default) x) =
    x

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
x_1 : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))
x : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)
h :
  Eq (α := (↑X : Type u))
    (((fun (x : (↑X : Type u)) ↦
              { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                continuous_toFun := ⋯ : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
            ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
              x_1) :
          (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
        default :
      (↑X : Type u))
    ((x_1 : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) default : (↑X : Type u))
⊢ Eq (α := (↑X : Type u))
    (((fun (x : (↑X : Type u)) ↦
              { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                continuous_toFun := ⋯ : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
            ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
              x_1) :
          (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
        x :
      (↑X : Type u))
    ((x_1 : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) x : (↑X : Type u))

Tactic:
obtain rfl := Subsingleton.elim x default

Premises used: Inhabited.default, Subsingleton.elim, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
x : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))
⊢ Eq (α := (↑X : Type u))
    (((fun (x : (↑X : Type u)) ↦
              { toFun := fun (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                continuous_toFun := ⋯ : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
            ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
              x) :
          (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
        default :
      (↑X : Type u))
    ((x : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) default : (↑X : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X Y : TopCat
y : (↑Y : Type u)
⊢ Eq (α := toSSet.obj X ⟶ toSSet.obj Y) (toSSet.map (const y))
    (SSet.const ((Equiv.symm toSSetObj₀Equiv : (a : (↑Y : Type u)) → toSSet.obj Y _⦋0⦌) y))

Tactic:
rfl

Premises used: SSet.const, Set.Mem, ContinuousMap.comp, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerLeft, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
n m : SimplexCategory
f : n ⟶ m
g : C((↑(stdSimplex ℝ (Fin (m.len + 1))) : Type), (↑X : Type u))
⊢ Continuous (X := (↑(stdSimplex ℝ (Fin ((unop (op n)).len + 1))) : Type)) (Y :=
    (↑(stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (stdSimplex.map
      (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))

Tactic:
continuity
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
n m : SimplexCategory
f : n ⟶ m
g : C((↑(stdSimplex ℝ (Fin (m.len + 1))) : Type), (↑X : Type u))
⊢ Eq (α := (fun (X : Type u) ↦ X) ((toSSet.obj X).obj (op n)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toSSet.obj X).map f.op) :
          (a : (fun (X : Type u) ↦ X) ((toSSet.obj X).obj (op m))) → (fun (X : Type u) ↦ X) ((toSSet.obj X).obj (op n)))
        ((Equiv.symm (X.toSSetObjEquiv (op m)) :
              (a : C((↑(stdSimplex ℝ (Fin ((unop (op m)).len + 1))) : Type), (↑X : Type u))) →
                (toSSet.obj X).obj (op m))
            g :
          (toSSet.obj X).obj (op m)) :
      (fun (X : Type u) ↦ X) ((toSSet.obj X).obj (op n)))
    ((Equiv.symm (X.toSSetObjEquiv (op n)) :
          (a : C((↑(stdSimplex ℝ (Fin ((unop (op n)).len + 1))) : Type), (↑X : Type u))) → (toSSet.obj X).obj (op n))
        (g.comp
          {
            toFun :=
              stdSimplex.map
                (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                      fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
                  (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) →
                    (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m),
            continuous_toFun := ⋯ :
            C((↑(stdSimplex ℝ (Fin ((unop (op n)).len + 1))) : Type), (↑(stdSimplex ℝ (Fin (m.len + 1))) : Type)) }) :
      (toSSet.obj X).obj (op n))

Tactic:
rfl

Premises used: stdSimplex.map, Set.Mem, ContinuousMap.comp, Quiver.Hom.unop, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
n m : SimplexCategory
f : n ⟶ m
x : (toSSet.obj X).obj (op m)
z : (↑(stdSimplex ℝ (Fin (n.len + 1))) : Type)
⊢ Eq (α := (↑X : Type u))
    ((((X.toSSetObjEquiv (op n) :
                (a : (toSSet.obj X).obj (op n)) → C((↑(stdSimplex ℝ (Fin (n.len + 1))) : Type), (↑X : Type u)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toSSet.obj X).map f.op) :
                  (a : (toSSet.obj X).obj (op m)) → (toSSet.obj X).obj (op n))
                x) :
            C((↑(stdSimplex ℝ (Fin (n.len + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑X : Type u))
        z :
      (↑X : Type u))
    ((((X.toSSetObjEquiv (op m) :
                (a : (toSSet.obj X).obj (op m)) → C((↑(stdSimplex ℝ (Fin (m.len + 1))) : Type), (↑X : Type u)))
              x :
            C((↑(stdSimplex ℝ (Fin (m.len + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑X : Type u))
        (stdSimplex.map
          (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
            (a : Fin (n.len + 1)) → Fin (m.len + 1))
          z) :
      (↑X : Type u))

Tactic:
rfl

Premises used: stdSimplex.map, Set.Mem, Quiver.Hom.unop, ULift.map, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
n : ℕ
x : toSSet.obj X _⦋n + 1⦌
i : Fin (n + 2)
z : (↑(stdSimplex ℝ (Fin (n + 1))) : Type)
⊢ Eq (α := (↑X : Type u))
    ((((X.toSSetObjEquiv (op ⦋n⦌) : (a : toSSet.obj X _⦋n⦌) → C((↑(stdSimplex ℝ (Fin (n + 1))) : Type), (↑X : Type u)))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (toSSet.obj X) i) :
                  (a : toSSet.obj X _⦋n + 1⦌) → toSSet.obj X _⦋n⦌)
                x) :
            C((↑(stdSimplex ℝ (Fin (n + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (n + 1))) : Type)) → (↑X : Type u))
        z :
      (↑X : Type u))
    ((((X.toSSetObjEquiv (op ⦋n + 1⦌) :
                (a : toSSet.obj X _⦋n + 1⦌) → C((↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type), (↑X : Type u)))
              x :
            C((↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type), (↑X : Type u))) :
          (a : (↑(stdSimplex ℝ (Fin (n + 1 + 1))) : Type)) → (↑X : Type u))
        (stdSimplex.map i.succAbove z) :
      (↑X : Type u))

Tactic:
rfl

Premises used: Fin.succAbove, stdSimplex.map, Set.Mem, ULift.map, rfl, ite