Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

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

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

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

Tactic:
<;>

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

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

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