awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
⊢ Epi.{u, u + 1} (C := SSet) (X := ∐ fun (s : X.N) ↦ Δ[s.dim]) (Y := X)
    (Sigma.desc fun (s : X.N) ↦ (Equiv.symm yonedaEquiv : (a : X _⦋s.dim⦌) → Δ[s.dim] ⟶ X) s.simplex)

Tactic:
simp only [← Subcomplex.range_eq_top_iff, range_eq_iSup_sigma_ι,
        colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, ← N.iSup_subcomplex_eq_top,
        Subcomplex.range_eq_ofSimplex, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, SSet.Subcomplex.range_eq_ofSimplex, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, SSet.range_eq_iSup_sigma_ι, CategoryTheory.Limits.colimit.ι_desc, SSet.Subcomplex.range_eq_top_iff, SSet.N.iSup_subcomplex_eq_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
obtain : ∀ (Y : SSet.{u}), Y.Finite → IsFinitelyPresentable Y → ∀ (p : Y ⟶ X), Epi p → IsFinitelyPresentable X
⊢ IsFinitelyPresentable X

Tactic:
obtain ⟨Y, _, _, p, _⟩ := exists_epi_from_isCardinalPresentable X

Premises used: SSet.Finite.exists_epi_from_isCardinalPresentable
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
obtain :
  ∀ (Z : SSet.{u}), Z.Finite → IsFinitelyPresentable Z → ∀ (q : Z ⟶ pullback p p), Epi q → IsFinitelyPresentable X
⊢ IsFinitelyPresentable X

Tactic:
obtain ⟨Z, _, _, q, _⟩ := exists_epi_from_isCardinalPresentable (pullback p p)

Premises used: CategoryTheory.Limits.pullback, SSet.Finite.exists_epi_from_isCardinalPresentable
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
⊢ Fact Cardinal.aleph0.IsRegular

Tactic:
have := Cardinal.fact_isRegular_aleph0.{u}
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this : Fact Cardinal.aleph0.IsRegular
⊢ IsRegularEpi p

Tactic:
have := IsRegularEpiCategory.regularEpiOfEpi p
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst_1 : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
hK : HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0
inst :
  ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0
⊢ IsFinitelyPresentable X

Tactic:
apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _

Premises used: CategoryTheory.EffectiveEpiStruct.isColimitCoforkOfIsPullback, CategoryTheory.EffectiveEpi.getStruct, CategoryTheory.Limits.isCoequalizerEpiComp, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.isCardinalPresentable_of_isColimit'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ Cardinal.aleph0 ≤ Cardinal.aleph0

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

Tactic:
exact hasCardinalLT_of_finite _ _ (by rfl)

Premises used: hasCardinalLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst_1 : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
inst : IsCardinalPresentable Z Cardinal.aleph0
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.zero)
    Cardinal.aleph0

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst_1 : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
inst : IsCardinalPresentable Y Cardinal.aleph0
⊢ IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj WalkingParallelPair.one)
    Cardinal.aleph0

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Z Cardinal.aleph0

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Presentable
Goal:
X : SSet
inst : X.Finite
Y : SSet
w : Y.Finite
w_1 : IsFinitelyPresentable Y
p : Y ⟶ X
h : Epi p
Z : SSet
w_2 : Z.Finite
w_3 : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h_1 : Epi q
this_1 : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ IsCardinalPresentable Y Cardinal.aleph0

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x_1 : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
x : Δ[p] _⦋n⦌
y : Δ[q] _⦋n⦌
⊢ (fun (f : Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) ↦
        (((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋p⦌) → Δ[p] _⦋n⦌)
              (SimplexCategory.Hom.mk (OrderHom.comp OrderHom.fst f)),
            (Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋q⦌) → Δ[q] _⦋n⦌)
              (SimplexCategory.Hom.mk (OrderHom.comp OrderHom.snd f))) :
          Δ[p] _⦋n⦌ × Δ[q] _⦋n⦌))
      ((fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌) ↦
          (match (motive := tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x with
            | (x, y) =>
              OrderHom.prod
                (SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[p] _⦋n⦌ ≃ (Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋p⦌)) :
                      (a : Δ[p] _⦋n⦌) → Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋p⦌)
                    x))
                (SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[q] _⦋n⦌ ≃ (Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋q⦌)) :
                      (a : Δ[q] _⦋n⦌) → Opposite.unop (Opposite.op ⦋n⦌) ⟶ ⦋q⦌)
                    y)) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)))
        (x, y)) =
    (x, y)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
i : Fin (n + 1)
⊢ Eq (α := Fin (p + 1))
    ((((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                  (a : Δ[p] _⦋n⦌ ⊗ Δ[q] _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                x :
              Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
            (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
          i).1 :
      Fin (p + 1))
    ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
i : Fin (n + 1)
⊢ Eq (α := Fin (q + 1))
    ((((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                  (a : Δ[p] _⦋n⦌ ⊗ Δ[q] _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                x :
              Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
            (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
          i).2 :
      Fin (q + 1))
    ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i : Fin (q + 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q m n : ℕ
f : ⦋m⦌ ⟶ ⦋n⦌
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ Eq (α := Fin (⦋m⦌.len + 1) →o Fin (p + 1) × Fin (q + 1))
    (OrderHom.comp
      (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
          (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
        z)
      (SimplexCategory.Hom.toOrderHom f))
    (((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋m⦌ ≃ (Fin (m + 1) →o Fin (p + 1) × Fin (q + 1))) :
        (a : (Δ[p] ⊗ Δ[q]) _⦋m⦌) → Fin (m + 1) →o Fin (p + 1) × Fin (q + 1))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).map f.op) :
          (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋m⦌))
        z))

Tactic:
rfl

Premises used: Quiver.Hom.unop, OrderHom.comp, OrderHom.prod, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n m : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
i : Fin (m + 1)
⊢ Eq (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋m⦌ ≃ (Fin (m + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋m⦌) → Fin (m + 1) →o Fin (p + 1) × Fin (q + 1))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).map f.op) :
                  (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) → (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋m⦌))
                x) :
            Fin (m + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (m + 1)) → Fin (p + 1) × Fin (q + 1))
        i :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        ((SimplexCategory.Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1)) i : Fin (⦋n⦌.len + 1)) :
      Fin (p + 1) × Fin (q + 1))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n + 1⦌
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (SimplicialObject.δ (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]) i) :
                  (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌))
                x) :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        j :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv :
                  tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n + 1⦌ ≃
                    (Fin (n + 1 + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n + 1⦌) → Fin (n + 1 + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1 + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1 + 1)) → Fin (p + 1) × Fin (q + 1))
        (i.succAbove j) :
      Fin (p + 1) × Fin (q + 1))

Tactic:
rfl

Premises used: Fin.succAbove, rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
rw :
  Function.Injective (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (ULift.down ∘
        Functor.obj
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
                (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
            z)) ↔
    Function.Injective (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    Function.Injective (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_injective,
    ← Function.Injective.of_comp_iff ULift.down_injective]

Premises used: SSet.nonDegenerate_iff_of_mono, SSet.prodStdSimplex.isoNerve, PartialOrder.mem_nerve_nonDegenerate_iff_injective, ULift.down_injective, CategoryTheory.Iso.hom, Function.Injective.of_comp_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ Function.Injective (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (ULift.down ∘
        Functor.obj
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
              (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
                (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
            z)) ↔
    Function.Injective (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
rw :
  StrictMono.{0, u} (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β :=
      ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))
      (Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
          z)) ↔
    StrictMono (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
⊢ Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[q]).nonDegenerate n) z ↔
    StrictMono (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))

Tactic:
rw [← nonDegenerate_iff_of_mono (isoNerve p q).hom,
    PartialOrder.mem_nerve_nonDegenerate_iff_strictMono]

Premises used: SSet.nonDegenerate_iff_of_mono, SSet.prodStdSimplex.isoNerve, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
⊢ StrictMono.{0, u} (α := Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)) (β :=
      ULift.{u, 0} (Fin (p + 1) × Fin (q + 1)))
      (Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((isoNerve p q).hom.app (Opposite.op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[p] ⊗ Δ[q]) _⦋n⦌)) →
              (fun (X : Type u) ↦ X) (nerve (ULift.{u, 0} (Fin (p + 1) × Fin (q + 1))) _⦋n⦌))
          z)) ↔
    StrictMono (α := Fin (n + 1)) (β := Fin (p + 1) × Fin (q + 1))
      (⇑(((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
        (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i) : ℕ) < m + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
⊢ LE.le (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        j :
      Fin (p + 1) × Fin (q + 1))

Tactic:
have := (objEquiv x).monotone h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this :
  LE.le (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        j :
      Fin (p + 1) × Fin (q + 1))
⊢ LE.le (α := Fin (p + 1)) ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))
    ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j : Fin (p + 1))

Tactic:
have h₁ : x.1 i ≤ x.1 j := this.1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this :
  LE.le (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        j :
      Fin (p + 1) × Fin (q + 1))
h₁ :
  LE.le (α := Fin (p + 1)) ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))
    ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j : Fin (p + 1))
⊢ LE.le (α := Fin (q + 1)) ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i : Fin (q + 1))
    ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j : Fin (q + 1))

Tactic:
have h₂ : x.2 i ≤ x.2 j := this.2
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this :
  LE.le (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        i :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              x :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        j :
      Fin (p + 1) × Fin (q + 1))
h₁ :
  LE.le (α := Fin (p + 1)) ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i : Fin (p + 1))
    ((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j : Fin (p + 1))
h₂ :
  LE.le (α := Fin (q + 1)) ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i : Fin (q + 1))
    ((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j : Fin (q + 1))
⊢ (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) i) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) i) : ℕ) ≤
    (↑((x.1 : (a : Fin (n + 1)) → Fin (p + 1)) j) : ℕ) + (↑((x.2 : (a : Fin (n + 1)) → Fin (q + 1)) j) : ℕ)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
hab : a ≤ b
⊢ a.1 ≤ b.1

Tactic:
obtain ⟨h₁, h₂⟩ := hab
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
hab : a ≤ b
h₁ : a.1 ≤ b.1
⊢ a.2 ≤ b.2

Tactic:
obtain ⟨h₁, h₂⟩ := hab
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
m : ℕ
hm : p + q = m
a b : Fin (p + 1) × Fin (q + 1)
h₁ : a.1 ≤ b.1
h₂ : a.2 ≤ b.2
rw : a.1 < b.1 ∧ a.2 ≤ b.2 ∨ a.1 ≤ b.1 ∧ a.2 < b.2 ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)
⊢ a < b ↔ (↑a.1 : ℕ) + (↑a.2 : ℕ) < (↑b.1 : ℕ) + (↑b.2 : ℕ)

Tactic:
rw [Prod.lt_iff]

Premises used: Prod.lt_iff