awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
obj :
  ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
⊢ Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m))
      (Subfunctor.obj
        (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)) m)
      (x₁, x₂) ↔
    Membership.mem (γ := Set ((tensorObj (𝒞 := Functor.category) X₁ X₂).obj m)) (Subfunctor.obj ⊤ m) (x₁, x₂)

Tactic:
simp only [Subfunctor.iSup_obj, Subcomplex.prod_obj, Set.mem_iUnion, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]

Premises used: Set.mem_iUnion, iff_true, SSet.Subcomplex.prod_obj, Set.top_eq_univ, Set.mem_univ, CategoryTheory.Subfunctor.top_obj, CategoryTheory.Subfunctor.iSup_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁

Tactic:
have hx₁ : x₁ ∈ (⊤ : X₁.Subcomplex).obj _ := by simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
⊢ Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
⊢ Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂

Tactic:
have hx₂ : x₂ ∈ (⊤ : X₂.Subcomplex).obj _ := by simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
hx₂ : Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂
⊢ ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m

Tactic:
simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂

Premises used: Set.mem_iUnion, CategoryTheory.Subfunctor.iSup_obj, SSet.N.iSup_subcomplex_eq_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : Membership.mem (γ := Set (X₁.obj m)) (Subfunctor.obj ⊤ m) x₁
hx₂ : Membership.mem (γ := Set (X₂.obj m)) (Subfunctor.obj ⊤ m) x₂
hx₃ : ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m
⊢ ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m

Tactic:
simp only [← N.iSup_subcomplex_eq_top, Subfunctor.iSup_obj, Set.mem_iUnion] at hx₁ hx₂

Premises used: Set.mem_iUnion, CategoryTheory.Subfunctor.iSup_obj, SSet.N.iSup_subcomplex_eq_top
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₁ : ∃ (i : X₁.N), x₁ ∈ i.subcomplex.obj m
hx₂ : ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m
obj :
  ∀ (s₁ : X₁.N) (hs₁ : x₁ ∈ s₁.subcomplex.obj m),
    ∃ (i : X₁.N) (i_1 : X₂.N),
      (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)

Tactic:
obtain ⟨s₁, hs₁⟩ := hx₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
hx₂ : ∃ (i : X₂.N), x₂ ∈ i.subcomplex.obj m
s₁ : X₁.N
hs₁ : x₁ ∈ s₁.subcomplex.obj m
obj :
  ∀ (s₂ : X₂.N) (hs₂ : x₂ ∈ s₂.subcomplex.obj m),
    ∃ (i : X₁.N) (i_1 : X₂.N),
      (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)

Tactic:
obtain ⟨s₂, hs₂⟩ := hx₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
s₁ : X₁.N
hs₁ : x₁ ∈ s₁.subcomplex.obj m
s₂ : X₂.N
hs₂ : x₂ ∈ s₂.subcomplex.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)

Tactic:
⟨s₁, s₂, hs₁, hs₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
s₁ : X₁.N
hs₁ : x₁ ∈ s₁.subcomplex.obj m
s₂ : X₂.N
hs₂ : x₂ ∈ s₂.subcomplex.obj m
⊢ ∃ (i : X₁.N) (i_1 : X₂.N),
    (x₁, x₂) ∈ ((Subcomplex.ofSimplex i.simplex).obj m).prod ((Subcomplex.ofSimplex i_1.simplex).obj m)

Tactic:
exact ⟨s₁, s₂, hs₁, hs₂⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
p q : ℕ
x₁ : X₁ _⦋p⦌
x₂ : X₂ _⦋q⦌
⊢ (ofSimplex x₁).prod (ofSimplex x₂) =
    range (X := tensorObj (𝒞 := Functor.category) Δ[p] Δ[q])
      ((Equiv.symm yonedaEquiv : (a : X₁ _⦋p⦌) → Δ[p] ⟶ X₁) x₁ ⊗ₘ
        (Equiv.symm yonedaEquiv : (a : X₂ _⦋q⦌) → Δ[q] ⟶ X₂) x₂)

Tactic:
simp [Subcomplex.range_tensorHom, Subcomplex.range_eq_ofSimplex]

Premises used: SSet.Subcomplex.range_eq_ofSimplex, SSet.Subcomplex.range_tensorHom
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
rw :
  HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)))
    n
⊢ HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂) n

Tactic:
rw [← hasDimensionLT_subcomplex_top_iff, ← iSup_subcomplexOfSimplex_prod_eq_top]

Premises used: SSet.iSup_subcomplexOfSimplex_prod_eq_top, SSet.hasDimensionLT_subcomplex_top_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
simp :
  ∀ (i : X₁.N) (i_1 : X₂.N),
    HasDimensionLT.{u}
      (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
        (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[i.dim] Δ[i_1.dim])
          ((Equiv.symm yonedaEquiv : (a : X₁ _⦋i.dim⦌) → Δ[i.dim] ⟶ X₁) i.simplex ⊗ₘ
            (Equiv.symm yonedaEquiv : (a : X₂ _⦋i_1.dim⦌) → Δ[i_1.dim] ⟶ X₂) i_1.simplex)))
      n
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (⨆ (x₁ : X₁.N), ⨆ (x₂ : X₂.N), (Subcomplex.ofSimplex x₁.simplex).prod (Subcomplex.ofSimplex x₂.simplex)))
    n

Tactic:
simp only [Subcomplex.ofSimplexProd_eq_range, hasDimensionLT_iSup_iff]

Premises used: SSet.Subcomplex.ofSimplexProd_eq_range, SSet.hasDimensionLT_iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
⊢ x₁.dim < d₁

Tactic:
have := X₁.dim_lt_of_nonDegenerate ⟨_, x₁.nonDegenerate⟩ d₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this : x₁.dim < d₁
⊢ x₂.dim < d₂

Tactic:
have := X₂.dim_lt_of_nonDegenerate ⟨_, x₂.nonDegenerate⟩ d₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this_1 : x₁.dim < d₁
this : x₂.dim < d₂
⊢ HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim]) n

Tactic:
have := (Δ[x₁.dim] ⊗ Δ[x₂.dim]).hasDimensionLT_of_le (x₁.dim + x₂.dim + 1) n
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
x₂ : X₂.N
this_1 : x₁.dim < d₁
this_2 : x₂.dim < d₂
this : HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim]) n
⊢ HasDimensionLT.{u}
    (Subcomplex.toSSet (X := tensorObj (𝒞 := Functor.category) X₁ X₂)
      (Subcomplex.range (X := tensorObj (𝒞 := Functor.category) Δ[x₁.dim] Δ[x₂.dim])
        ((Equiv.symm yonedaEquiv : (a : X₁ _⦋x₁.dim⦌) → Δ[x₁.dim] ⟶ X₁) x₁.simplex ⊗ₘ
          (Equiv.symm yonedaEquiv : (a : X₂ _⦋x₂.dim⦌) → Δ[x₂.dim] ⟶ X₂) x₂.simplex)))
    n

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLE d₁
inst_1 : X₂.HasDimensionLE d₂
n : ℕ
hn : d₁ + d₂ ≤ n
⊢ HasDimensionLE.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂) n

Tactic:
hasDimensionLT_prod X₁ X₂ (d₁ + 1) (d₂ + 1) (n + 1)

Premises used: SSet.hasDimensionLT_prod, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLT d₁
inst_1 : X₂.HasDimensionLT d₂
⊢ HasDimensionLT.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂) (d₁ + d₂)

Tactic:
hasDimensionLT_prod _ _ d₁ d₂ (d₁ + d₂)

Premises used: SSet.hasDimensionLT_prod, HAdd.hAdd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
d₁ d₂ : ℕ
inst : X₁.HasDimensionLE d₁
inst_1 : X₂.HasDimensionLE d₂
⊢ HasDimensionLE.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂) (d₁ + d₂)

Tactic:
hasDimensionLE_prod _ _ d₁ d₂ (d₁ + d₂)

Premises used: HAdd.hAdd, SSet.hasDimensionLE_prod
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
obtain : ∀ (d₁ : ℕ), X₁.HasDimensionLT d₁ → SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)

Tactic:
obtain ⟨d₁, _⟩ := X₁.hasDimensionLT_of_finite

Premises used: SSet.hasDimensionLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
d₁ : ℕ
h : X₁.HasDimensionLT d₁
obtain : ∀ (d₂ : ℕ), X₂.HasDimensionLT d₂ → SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)

Tactic:
obtain ⟨d₂, _⟩ := X₂.hasDimensionLT_of_finite

Premises used: SSet.hasDimensionLT_of_finite
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
d₁ : ℕ
h : X₁.HasDimensionLT d₁
d₂ : ℕ
h_1 : X₂.HasDimensionLT d₂
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)

Tactic:
finite_of_hasDimensionLT _ (d₁ + d₂) (fun _ _ ↦ inferInstance)

Premises used: SSet.finite_of_hasDimensionLT, inferInstance, HAdd.hAdd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₁.Finite
inst_1 : X₂.Finite
d₁ : ℕ
h : X₁.HasDimensionLT d₁
d₂ : ℕ
h_1 : X₂.HasDimensionLT d₂
⊢ SSet.Finite.{u} (tensorObj (𝒞 := Functor.category) X₁ X₂)

Tactic:
exact finite_of_hasDimensionLT _ (d₁ + d₂) (fun _ _ ↦ inferInstance)

Premises used: SSet.finite_of_hasDimensionLT, inferInstance, HAdd.hAdd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
inst : X₂.Finite
inst_1 : X₃.Finite
Z : SSet
x x_1 : Z ⟶ X₁
h : x ≫ lift t l = x_1 ≫ lift t l
⊢ x ≫ t = x_1 ≫ t

Tactic:
simpa using h =≫ fst _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
sq : IsPullback t l r b
inst : X₂.Finite
inst_1 : X₃.Finite
Z : SSet
x x_1 : Z ⟶ X₁
h : x ≫ lift t l = x_1 ≫ lift t l
⊢ x ≫ l = x_1 ≫ l

Tactic:
simpa using h =≫ snd _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Goal:
X₁ X₂ X₃ X₄ : SSet
inst : X₂.Finite
inst_1 : X₃.Finite
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
⊢ SSet.Finite.{u} (pullback r b)

Tactic:
finite_of_isPullback (IsPullback.of_hasPullback r b)

Premises used: SSet.finite_of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e : Edge (X := tensorObj (𝒞 := Functor.category) X Y) (x, y) (x', y')
⊢ ∃ (e₁ : Edge x x') (e₂ : Edge y y'), e₁.tensor e₂ = e

Tactic:
⟨e.map (fst _ _), e.map (snd _ _), rfl⟩

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, Exists.intro, CategoryTheory.SemiCartesianMonoidalCategory.fst, rfl, SSet.Truncated.Edge.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
y :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
⊢ (id x).tensor (id y) = id (x, y)

Tactic:
rfl

Premises used: SSet.Truncated.Edge.tensor, rfl, SSet.Truncated.Edge.id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y X' Y' : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
f : X ⟶ X'
g : Y ⟶ Y'
⊢ (e₁.tensor e₂).map (f ⊗ₘ g) = (e₁.map f).tensor (e₂.map g)

Tactic:
rfl

Premises used: SSet.Truncated.Edge.tensor, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y X' : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
f : X ⟶ X'
⊢ (e₁.tensor e₂).map (f ▷ Y) = (e₁.map f).tensor e₂

Tactic:
rfl

Premises used: SSet.Truncated.Edge.tensor, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Y' : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
g : Y ⟶ Y'
⊢ (e₁.tensor e₂).map (X ◁ g) = e₁.tensor (e₂.map g)

Tactic:
rfl

Premises used: SSet.Truncated.Edge.tensor, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y Z : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
z z' :
  Z.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₃ : Edge z z'
⊢ ((e₁.tensor e₂).tensor e₃).map (Iso.hom (α_ X Y Z)) = e₁.tensor (e₂.tensor e₃)

Tactic:
rfl

Premises used: SSet.Truncated.Edge.tensor, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
⊢ (e₁.tensor e₂).map (fst X Y) = e₁

Tactic:
rfl

Premises used: rfl, SSet.Truncated.Edge.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x x' :
  X.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₁ : Edge x x'
y y' :
  Y.obj
    (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ tensor._proof_1))
e₂ : Edge y y'
⊢ (e₁.tensor e₂).map (snd X Y) = e₂

Tactic:
rfl

Premises used: rfl, SSet.Truncated.Edge.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ex : Edge x₀ x₁
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
ey : Edge y₀ y₁
rw : homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) = homMk (ex.tensor ey)
rw₁ rw₂ : homMk (ex.tensor ey) = homMk (ex.tensor ey)
⊢ homMk (ex.tensor (Edge.id y₀)) ≫ homMk ((Edge.id x₁).tensor ey) =
    homMk ((Edge.id x₀).tensor ey) ≫ homMk (ex.tensor (Edge.id y₁))

Tactic:
rw [homMk_comp_homMk ((Edge.CompStruct.idComp ex).tensor (Edge.CompStruct.compId ey)),
    homMk_comp_homMk ((Edge.CompStruct.compId ex).tensor (Edge.CompStruct.idComp ey))]

Premises used: SSet.Truncated.Edge.CompStruct.tensor, SSet.Truncated.Edge.CompStruct.compId, SSet.Truncated.HomotopyCategory.homMk_comp_homMk, SSet.Truncated.Edge.CompStruct.idComp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (functor X Y).obj (mk (x, y)) = (mk x, mk y)

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e : Edge x₀ x₁
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e' : Edge y₀ y₁
⊢ (functor X Y).map (homMk (e.tensor e')) = (homMk e, homMk e')

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Paths, CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, Quiver.Path.comp, SSet.Truncated.HomotopyCategory.mk, rfl, SSet.Truncated.Edge.map
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ ∀
    (x_1 :
      Y.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    Eq.{u + 1} (α :=
      Quiver.Hom (V := (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        ((fun
              (y :
                Y.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (mk (x, y) : (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x_1)
        ((fun
              (y :
                Y.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (mk (x, y) : (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x_1))
      ((fun
            {y₀ y₁ :
              Y.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))}
            (e : Edge y₀ y₁) ↦
          homMk ((Edge.id x).tensor e))
        (Edge.id x_1))
      (𝟙
        ((fun
              (y :
                Y.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))) ↦
            (mk (x, y) : (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
          x_1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (inverse X Y).obj (mk x, mk y) = mk (x, y)

Tactic:
rfl

Premises used: SSet.Truncated.HomotopyCategory.mk, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e : Edge x₀ x₁
y :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
⊢ (inverse X Y).map (Prod.mkHom (homMk e) (𝟙 (mk y))) = homMk (e.tensor (Edge.id y))

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, Quiver.Path.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e : Edge y₀ y₁
⊢ (inverse X Y).map (Prod.mkHom (𝟙 (mk x)) (homMk e)) = homMk ((Edge.id x).tensor e)

Tactic:
rfl

Premises used: CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, Quiver.Path.comp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e : Edge x₀ x₁
y₀ y₁ :
  Y.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge.tensor._proof_1))
e' : Edge y₀ y₁
⊢ (inverse X Y).map (Prod.mkHom (homMk e) (homMk e')) = homMk (e.tensor e')

Tactic:
homMk_comp_homMk ((Edge.CompStruct.compId e).tensor (Edge.CompStruct.idComp e'))

Premises used: SSet.Truncated.Edge.CompStruct.tensor, SSet.Truncated.Edge.CompStruct.compId, CategoryTheory.Cat.FreeRefl.homMk, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, SSet.Truncated.HomotopyCategory.homMk, SSet.Truncated.HomotopyCategory.homMk_comp_homMk, Quiver.Path.comp, SSet.Truncated.Edge.CompStruct.idComp, SSet.Truncated.HomotopyCategory.mk