mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left) (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      pushout.desc
          ((α_ X₁.right X₂.right X₃.left).hom ≫
            X₁.right ◁
                pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
          (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
            pushout.desc
              (X₁.right ◁
                  pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              ⋯)
          ⋯ ≫
        pushout.desc
          (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
            pushout.desc
              (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯)
          ((α_ X₁.left X₂.right X₃.right).inv ≫
            pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
          ⋯ =
    pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ (φ x hd (min x hd).castSucc).1 < (φ x hd (min x hd).succ).1

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ (φ x hd (min x hd).castSucc).2 ≤ (φ x hd (min x hd).succ).2

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
⊢ φ x hd (min x hd).castSucc < φ x hd (min x hd).succ

pp: case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ φ x hd i.castSucc < φ x hd i.succ

Tactic:
· exact Prod.lt_of_lt_of_le (by simp) (by simp)

Goal state after:
case inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin (d + 1)
hi : min x hd < i
⊢ φ x hd i.castSucc < φ x hd i.succ
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_3.h₀
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
        pushout.desc
            ((α_ X₁.right X₂.right X₃.left).hom ≫
              X₁.right ◁
                  pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
              pushout.desc
                (X₁.right ◁
                    pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                ⋯)
            ⋯ ≫
          pushout.desc
            (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
              pushout.desc
                (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯)
            ((α_ X₁.left X₂.right X₃.right).inv ≫
              pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯ =
    (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
        𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_3.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
        pushout.desc
            ((α_ X₁.right X₂.right X₃.left).hom ≫
              X₁.right ◁
                  pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
              pushout.desc
                (X₁.right ◁
                    pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                ⋯)
            ⋯ ≫
          pushout.desc
            (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
              pushout.desc
                (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯)
            ((α_ X₁.left X₂.right X₃.right).inv ≫
              pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯ =
    (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
          (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
        𝟙 ((X₁ □ X₂) □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left) (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
      pushout.desc
          (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
            pushout.desc
              (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯)
          ((α_ X₁.left X₂.right X₃.right).inv ≫
            pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                X₃.right ≫
              pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
          ⋯ ≫
        pushout.desc
          ((α_ X₁.right X₂.right X₃.left).hom ≫
            X₁.right ◁
                pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
              pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
          (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
            pushout.desc
              (X₁.right ◁
                  pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              ⋯)
          ⋯ =
    pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
        (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
      𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_4.h₀
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorLeft X₁.right).map
        (pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
          (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
        pushout.desc
            (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
              pushout.desc
                (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯)
            ((α_ X₁.left X₂.right X₃.right).inv ≫
              pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯ ≫
          pushout.desc
            ((α_ X₁.right X₂.right X₃.left).hom ≫
              X₁.right ◁
                  pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
              pushout.desc
                (X₁.right ◁
                    pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                ⋯)
            ⋯ =
    (tensorLeft X₁.right).map
        (pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
          (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
        𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_4.h₁
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ (tensorLeft X₁.right).map
        (pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
          (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
        pushout.desc
            (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
              pushout.desc
                (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯)
            ((α_ X₁.left X₂.right X₃.right).inv ≫
              pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                  X₃.right ≫
                pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                  (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
            ⋯ ≫
          pushout.desc
            ((α_ X₁.right X₂.right X₃.left).hom ≫
              X₁.right ◁
                  pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                    (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
            (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
              pushout.desc
                (X₁.right ◁
                    pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                  (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                ⋯)
            ⋯ =
    (tensorLeft X₁.right).map
        (pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left) (((curriedTensor C).obj X₂.left).map X₃.hom)) ≫
      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
          (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom) ≫
        𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero.zero.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ x✝ : zero ⟶ zero
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      zero (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        zero x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        zero x✝

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso

Goal state before:
pp: case zero.zero.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : zero ⟶ zero
x✝ : zero ⟶ one
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      zero (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        zero x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        zero x✝

Tactic:
simp

Goal state after: