Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: case ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ ((((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
            ↑(assoc R R R ↑S ↑T ↑U).symm).comp
        includeLeft)
      x✝ =
    ((((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
                ↑(assoc R R R ↑S ↑U ↑T).symm).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑S)
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))).comp
        includeLeft)
      x✝

pp: case hb.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ (((AlgHom.restrictScalars R
                (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
            includeRight).comp
        includeLeft)
      x✝ =
    (((AlgHom.restrictScalars R
                (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                          (AlgHom.id R ↑T)).comp
                      ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                  (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                    (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
            includeRight).comp
        includeLeft)
      x✝

pp: case hb.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                        (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                    ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
              includeRight)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                            (AlgHom.id R ↑T)).comp
                        ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                    (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
              includeRight)).comp
        includeRight)
      x✝

Tactic:
<;>

Goal state after:
case ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑S
⊢ ((((↑(assoc R R R ↑U ↑S ↑T).symm).comp (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
            ↑(assoc R R R ↑S ↑T ↑U).symm).comp
        includeLeft)
      x✝ =
    ((((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom) (AlgHom.id R ↑T)).comp
                ↑(assoc R R R ↑S ↑U ↑T).symm).comp
            (Algebra.TensorProduct.map (AlgHom.id R ↑S)
              (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom))).comp
        includeLeft)
      x✝

case hb.ha
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑T
⊢ (((AlgHom.restrictScalars R
                (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                  ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
            includeRight).comp
        includeLeft)
      x✝ =
    (((AlgHom.restrictScalars R
                (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                          (AlgHom.id R ↑T)).comp
                      ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                  (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                    (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
            includeRight).comp
        includeLeft)
      x✝

case hb.hb
R : Type u
inst✝ : CommRing R
A B C D S T U : CommAlgCat R
x✝ : ↑U
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((↑(assoc R R R ↑U ↑S ↑T).symm).comp
                        (Hom.hom (isoMk (Algebra.TensorProduct.comm R (↑S ⊗[R] ↑T) ↑U)).hom)).comp
                    ↑(assoc R R R ↑S ↑T ↑U).symm)).comp
              includeRight)).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars R
                  (((Algebra.TensorProduct.map (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑S ↑U)).hom)
                            (AlgHom.id R ↑T)).comp
                        ↑(assoc R R R ↑S ↑U ↑T).symm).comp
                    (Algebra.TensorProduct.map (AlgHom.id R ↑S)
                      (Hom.hom (isoMk (Algebra.TensorProduct.comm R ↑T ↑U)).hom)))).comp
              includeRight)).comp
        includeRight)
      x✝