-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem pentagon (W X Y Z : ModuleCat R) :
    whiskerRight (associator W X Y).hom Z ≫
        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
      (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
w : ↑W
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom
        (whiskerRight (associator W X Y).hom Z ≫
          (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
rfl

Result:
no goals

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ ∀ (w : ↑W) (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom
          (whiskerRight (associator W X Y).hom Z ≫
            (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
intro w x y z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
w : ↑W
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom
        (whiskerRight (associator W X Y).hom Z ≫
          (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ whiskerRight (associator W X Y).hom Z ≫ (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ Hom.hom
      (whiskerRight (associator W X Y).hom Z ≫
        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom) =
    Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)

Proof state:
case hf
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ Hom.hom
      (whiskerRight (associator W X Y).hom Z ≫
        (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom) =
    Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom)

Tactic:
apply TensorProduct.ext_fourfold

Result:
case hf.H
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ ∀ (w : ↑W) (x : ↑X) (y : ↑Y) (z : ↑Z),
    (Hom.hom
          (whiskerRight (associator W X Y).hom Z ≫
            (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)