awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K K' : SSet
f : K ⟶ K'
L : SSet
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) K L).obj Δ
⊢ Eq (α := tensorObj (𝒞 := types) (K'.obj Δ) (L.obj Δ))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ ▷ L.obj Δ) : (a : K.obj Δ ⊗ L.obj Δ) → K'.obj Δ ⊗ L.obj Δ) x :
      tensorObj (𝒞 := types) (K'.obj Δ) (L.obj Δ))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) : (a : K.obj Δ) → K'.obj Δ) x.1, x.2) : K'.obj Δ × L.obj Δ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K L M : SSet
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) K L) M).obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (α_ (K.obj Δ) (L.obj Δ) (M.obj Δ))) :
        (a : (K.obj Δ ⊗ L.obj Δ) ⊗ M.obj Δ) → K.obj Δ ⊗ L.obj Δ ⊗ M.obj Δ)
      x =
    (x.1.1, x.1.2, x.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K L M : SSet
Δ : SimplexCategoryᵒᵖ
x : (tensorObj (𝒞 := Functor.category) K (tensorObj (𝒞 := Functor.category) L M)).obj Δ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (α_ (K.obj Δ) (L.obj Δ) (M.obj Δ))) :
        (a : K.obj Δ ⊗ L.obj Δ ⊗ M.obj Δ) → (K.obj Δ ⊗ L.obj Δ) ⊗ M.obj Δ)
      x =
    ((x.1, x.2.1), x.2.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
h :
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
          ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
              x))
      PUnit.unit =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
              x) ≫
          K.map f))
      PUnit.unit
⊢ ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
      ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
          x) =
    (↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
          x) ≫
      K.map f

Tactic:
ext ⟨⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
h :
  Eq (α := K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map f) : (a : K.obj Δ) → K.obj Δ')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : K _⦋0⦌) → K.obj Δ)
            x :
          K.obj Δ) :
      K.obj Δ')
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((𝟙_ SSet) (𝒞 := Functor.category).map f ≫
          ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ') ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ'))))
              x))
      PUnit.unit =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) → (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
              x) ≫
          K.map f))
      PUnit.unit

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
h :
  Eq (α := K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0) ≫ f)) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
⊢ Eq (α := K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map f) : (a : K.obj Δ) → K.obj Δ')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : K _⦋0⦌) → K.obj Δ)
            x :
          K.obj Δ) :
      K.obj Δ')

Tactic:
rw [← Functor.map_comp_apply]

Premises used: CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ Eq (α := K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ').const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0) ≫ f)) :
          (a : K _⦋0⦌) → K.obj Δ')
        x :
      K.obj Δ')

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
w :
  ∀ (Δ : SimplexCategoryᵒᵖ),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : K _⦋0⦌) ↦
                ({
                    app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                      ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                        (ConcreteCategory.hom (FC := TypeCat.Fun)
                              (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                            (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                              (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                          x,
                    naturality := ⋯ } :
                  NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
              ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                        (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
                      PUnit.unit :
                    (fun (X : Type u) ↦ X) (K _⦋0⦌)))
                φ))
            Δ))
        PUnit.unit =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ)).toFun PUnit.unit
⊢ (fun (x : K _⦋0⦌) ↦
        ({
            app := fun (Δ : SimplexCategoryᵒᵖ) ↦
              ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                    (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                      (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                  x,
            naturality := ⋯ } :
          NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
      ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
              PUnit.unit :
            (fun (X : Type u) ↦ X) (K _⦋0⦌)))
        φ) =
    φ

Tactic:
ext Δ ⟨⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
Δ : SimplexCategoryᵒᵖ
w :
  Eq (α := K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) : (a : 𝟙_ SSet _⦋0⦌) → K _⦋0⦌) PUnit.unit :
          K _⦋0⦌) :
      K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : K _⦋0⦌) ↦
              ({
                  app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                    ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun)
                            (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                          (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                            (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                        x,
                  naturality := ⋯ } :
                NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
            ((fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
                      (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
                    PUnit.unit :
                  (fun (X : Type u) ↦ X) (K _⦋0⦌)))
              φ))
          Δ))
      PUnit.unit =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ)).toFun PUnit.unit

Tactic:
dsimp [-Monoidal.tensorUnit_obj]

Premises used: CategoryTheory.Monoidal.tensorUnit_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
Δ : SimplexCategoryᵒᵖ
w :
  Eq (α := K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((𝟙_ SSet) (𝒞 := Functor.category).map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : 𝟙_ SSet _⦋0⦌) → (𝟙_ SSet).obj Δ)
            PUnit.unit :
          (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) :
      K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)
⊢ Eq (α := K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
          (a : K _⦋0⦌) → K.obj Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) : (a : 𝟙_ SSet _⦋0⦌) → K _⦋0⦌) PUnit.unit :
          K _⦋0⦌) :
      K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)

Tactic:
rw [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K
Δ : SimplexCategoryᵒᵖ
⊢ Eq (α := K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((𝟙_ SSet) (𝒞 := Functor.category).map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
              (a : 𝟙_ SSet _⦋0⦌) → (𝟙_ SSet).obj Δ)
            PUnit.unit :
          (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) :
      K.obj Δ)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Δ) : (a : (𝟙_ SSet).obj Δ) → K.obj Δ) PUnit.unit : K.obj Δ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
K : SSet
x : K _⦋0⦌
⊢ (fun (φ : (𝟙_ SSet) (𝒞 := Functor.category) ⟶ K) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app (Opposite.op ⦋0⦌)) :
              (a : (fun (X : Type u) ↦ X) (𝟙_ SSet _⦋0⦌)) → (fun (X : Type u) ↦ X) (K _⦋0⦌))
            PUnit.unit :
          (fun (X : Type u) ↦ X) (K _⦋0⦌)))
      ((fun (x : K _⦋0⦌) ↦
          ({
              app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                ↾fun (x_1 : (𝟙_ SSet) (𝒞 := Functor.category).obj Δ) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (K.map (Quiver.Hom.op ((Opposite.unop Δ).const ⦋0⦌ 0))) :
                      (a : (fun (X : Type u) ↦ X) (K _⦋0⦌)) →
                        (fun (X : Type u) ↦ X) (K.obj (Opposite.op (Opposite.unop Δ))))
                    x,
              naturality := ⋯ } :
            NatTrans ((𝟙_ SSet) (𝒞 := Functor.category)) K))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
w :
  ∀ (n : SimplexCategory) (x_2 : x.obj (Opposite.op n)),
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
              x)
            (Opposite.op n)))
        x_2
⊢ x_1 = (fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0])) x

Tactic:
ext ⟨n⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
n : SimplexCategory
x_2 : x.obj (Opposite.op n)
a :
  ∀ (x_3 : Fin ((Opposite.unop (Opposite.op n)).len + 1)),
    (↑((SimplexCategory.Hom.toOrderHom
                (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                    (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                  (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2)) :
              (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
            x_3) :
        ℕ) =
      (↑((SimplexCategory.Hom.toOrderHom
                (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                    (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                  (TypeCat.Fun.toFun
                    (ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app
                        ((fun (x : SSet.{u}) ↦
                            (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
                          x)
                        (Opposite.op n)))
                    x_2)) :
              (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
            x_3) :
        ℕ)
⊢ Eq (α := Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
    (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
          (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
        (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2) :
      Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
    (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
          (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
                x)
              (Opposite.op n)))
          x_2) :
      Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
n : SimplexCategory
x_2 : x.obj (Opposite.op n)
x_3 : Fin ((Opposite.unop (Opposite.op n)).len + 1)
⊢ (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                  (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2)) :
            (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
          x_3) :
      ℕ) =
    (↑((SimplexCategory.Hom.toOrderHom
              (((objEquiv : Δ[0].obj (Opposite.op n) ≃ (Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)) :
                  (a : Δ[0].obj (Opposite.op n)) → Opposite.unop (Opposite.op n) ⟶ ⦋0⦌)
                (TypeCat.Fun.toFun
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      ((fun (x : SSet.{u}) ↦
                          (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0]))
                        x)
                      (Opposite.op n)))
                  x_2)) :
            (a : Fin ((Opposite.unop (Opposite.op n)).len + 1)) → Fin (⦋0⦌.len + 1))
          x_3) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
x : SSet
x_1 : x ⟶ Δ[0]
n : SimplexCategory
x_2 : x.obj (Opposite.op n)
⊢ TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.app (Opposite.op n))) x_2 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : SSet.{u}) ↦ (SSet.const ((Equiv.symm obj₀Equiv : (a : Fin (0 + 1)) → Δ[0] _⦋0⦌) 0) : x ⟶ Δ[0])) x)
          (Opposite.op n)))
      x_2

Tactic:
exact objEquiv.injective (by ext; simp)

Premises used: Equiv.injective, SSet.stdSimplex.objEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X : SSet
f g : X ⟶ Δ[0]
⊢ f = g

Tactic:
isTerminalObj₀.hom_ext _ _

Premises used: SSet.stdSimplex.isTerminalObj₀, CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
n : SimplexCategoryᵒᵖ
inst : Finite.{u + 1} (X.obj n)
inst_1 : Finite.{u + 1} (Y.obj n)
⊢ Finite.{u + 1} ((tensorObj (𝒞 := Functor.category) X Y).obj n)

Tactic:
inferInstanceAs (Finite (X.obj n × Y.obj n))

Premises used: _private.0.SSet.instFiniteObjOppositeSimplexCategoryTensorObj._proof_1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
⊢ SSet.Finite.{u} ((𝟙_ SSet) (𝒞 := Functor.category))

Tactic:
finite_of_iso (stdSimplex.isTerminalObj₀.{u}.uniqueUpToIso
    CartesianMonoidalCategory.isTerminalTensorUnit)

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, SSet.stdSimplex.isTerminalObj₀, SSet.finite_of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
⊢ HasDimensionLE.{u} ((𝟙_ SSet) (𝒞 := Functor.category)) 0

Tactic:
(hasDimensionLT_iff_of_iso (stdSimplex.isTerminalObj₀.{u}.uniqueUpToIso
    CartesianMonoidalCategory.isTerminalTensorUnit) _).1 inferInstance

Premises used: CategoryTheory.Limits.IsTerminal.uniqueUpToIso, inferInstance, CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit, SSet.stdSimplex.isTerminalObj₀, Iff.mp, SSet.hasDimensionLT_iff_of_iso
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A₁ A₂ : X.Subcomplex
hX : A₁ ≤ A₂
B₁ B₂ : Y.Subcomplex
hY : B₁ ≤ B₂
⊢ A₁.prod B₁ ≤ A₂.prod B₂

Tactic:
fun _ _ hx => ⟨hX _ hx.1, hY _ hx.2⟩

Premises used: Set.Mem, setOf, Set.prod, Set.Subset, And.right, And.left, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ B ≤ B

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ A ≤ A

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
obj :
  ∀ (m : SimplexCategoryᵒᵖ) (y₁ : Y₁.obj m) (y₂ : Y₂.obj m),
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
        (y₁, y₂) ↔
      (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
⊢ range (f₁ ⊗ₘ f₂) = (range f₁).prod (range f₂)

Tactic:
ext m ⟨y₁, y₂⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
obj :
  Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) →
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m
obj₁ :
  (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m →
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂)
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
      (y₁, y₂) ↔
    (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
x₁ : X₁.obj m
x₂ : X₂.obj m
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
        (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
      (x₁, x₂) =
    (y₁, y₂)
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).1 =
      (y₁, y₂).1 ∧
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).2 =
      (y₁, y₂).2

Tactic:
rw [Prod.eq_iff_fst_eq_snd_eq] at h

Premises used: Prod.eq_iff_fst_eq_snd_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
x₁ : X₁.obj m
x₂ : X₂.obj m
h :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).1 =
      (y₁, y₂).1 ∧
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).2 =
      (y₁, y₂).2
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
x₁ : X₁.obj m
x₂ : X₂.obj m
h :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).1 =
      (y₁, y₂).1 ∧
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f₁ ⊗ₘ f₂) m) :
            (a : (fun (X : Type u) ↦ X) ((X₁ ⊗ X₂).obj m)) → (fun (X : Type u) ↦ X) ((Y₁ ⊗ Y₂).obj m))
          (x₁, x₂)).2 =
      (y₁, y₂).2
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
exact ⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
Goal:
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ Membership.mem (α := (tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m) (γ :=
    Set ((tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj m)) (Subfunctor.obj (range (f₁ ⊗ₘ f₂)) m)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (f₁.app m) :
            (a : (fun (X : Type u) ↦ X) (X₁.obj m)) → (fun (X : Type u) ↦ X) (Y₁.obj m))
          x₁,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f₂.app m) :
            (a : (fun (X : Type u) ↦ X) (X₂.obj m)) → (fun (X : Type u) ↦ X) (Y₂.obj m))
          x₂) :
      Y₁.obj m × Y₂.obj m)

Tactic:
⟨⟨x₁, x₂⟩, rfl⟩

Premises used: Set.Mem, setOf, Prod.mk, Exists.intro, Set.range, rfl