[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
⊢ x * (y + z) = x * y + x * z
[PROOFSTEP]
have := A.mul.map_add (x ⊗ₜ y) (x ⊗ₜ z)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] y + x ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] y) + ↑A.mul (x ⊗ₜ[R] z)
⊢ x * (y + z) = x * y + x * z
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] y + x ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] y) + ↑A.mul (x ⊗ₜ[R] z)
⊢ x * (y + z) = ↑A.mul (x ⊗ₜ[R] y + x ⊗ₜ[R] z)
[PROOFSTEP]
rw [← TensorProduct.tmul_add]
[GOAL]
case h.e'_2
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] y + x ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] y) + ↑A.mul (x ⊗ₜ[R] z)
⊢ x * (y + z) = ↑A.mul (x ⊗ₜ[R] (y + z))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
⊢ (x + y) * z = x * z + y * z
[PROOFSTEP]
have := A.mul.map_add (x ⊗ₜ z) (y ⊗ₜ z)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] z + y ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] z) + ↑A.mul (y ⊗ₜ[R] z)
⊢ (x + y) * z = x * z + y * z
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] z + y ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] z) + ↑A.mul (y ⊗ₜ[R] z)
⊢ (x + y) * z = ↑A.mul (x ⊗ₜ[R] z + y ⊗ₜ[R] z)
[PROOFSTEP]
rw [← TensorProduct.add_tmul]
[GOAL]
case h.e'_2
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this : ↑A.mul (x ⊗ₜ[R] z + y ⊗ₜ[R] z) = ↑A.mul (x ⊗ₜ[R] z) + ↑A.mul (y ⊗ₜ[R] z)
⊢ (x + y) * z = ↑A.mul ((x + y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
⊢ ↑A.mul (0 ⊗ₜ[R] x) = 0
[PROOFSTEP]
rw [TensorProduct.zero_tmul, map_zero]
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
⊢ ↑A.mul (x ⊗ₜ[R] 0) = 0
[PROOFSTEP]
rw [TensorProduct.tmul_zero, map_zero]
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
have := LinearMap.congr_fun A.mul_assoc (x ⊗ₜ y ⊗ₜ z)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x y z : ↑A.X
this :
  ↑(CategoryTheory.MonoidalCategory.tensorHom A.mul (𝟙 A.X) ≫ A.mul) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑((CategoryTheory.MonoidalCategory.associator A.X A.X A.X).hom ≫
          CategoryTheory.MonoidalCategory.tensorHom (𝟙 A.X) A.mul ≫ A.mul)
      ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
⊢ x * y * z = x * (y * z)
[PROOFSTEP]
convert this
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
⊢ 1 * x = x
[PROOFSTEP]
have := LinearMap.congr_fun A.one_mul ((1 : R) ⊗ₜ x)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
this :
  ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (1 ⊗ₜ[R] x) =
    ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (1 ⊗ₜ[R] x)
⊢ 1 * x = x
[PROOFSTEP]
convert this
[GOAL]
case h.e'_3
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
this :
  ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (1 ⊗ₜ[R] x) =
    ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (1 ⊗ₜ[R] x)
⊢ x = ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (1 ⊗ₜ[R] x)
[PROOFSTEP]
rw [MonoidalCategory.leftUnitor_hom_apply, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
⊢ x * 1 = x
[PROOFSTEP]
have := LinearMap.congr_fun A.mul_one (x ⊗ₜ (1 : R))
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
this :
  ↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 A.X) A.one ≫ A.mul) (x ⊗ₜ[R] 1) =
    ↑(CategoryTheory.MonoidalCategory.rightUnitor A.X).hom (x ⊗ₜ[R] 1)
⊢ x * 1 = x
[PROOFSTEP]
convert this
[GOAL]
case h.e'_3
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : AddCommGroup ↑A.X := inferInstance
x : ↑A.X
this :
  ↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 A.X) A.one ≫ A.mul) (x ⊗ₜ[R] 1) =
    ↑(CategoryTheory.MonoidalCategory.rightUnitor A.X).hom (x ⊗ₜ[R] 1)
⊢ x = ↑(CategoryTheory.MonoidalCategory.rightUnitor A.X).hom (x ⊗ₜ[R] 1)
[PROOFSTEP]
erw [MonoidalCategory.leftUnitor_hom_apply, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
x y : R
⊢ OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) }
      (x * y) =
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) }
        x *
      OneHom.toFun
        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) } y
[PROOFSTEP]
have h := LinearMap.congr_fun A.one_mul.symm (x ⊗ₜ A.one y)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
x y : R
h :
  ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (x ⊗ₜ[R] ↑A.one y) =
    ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (x ⊗ₜ[R] ↑A.one y)
⊢ OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) }
      (x * y) =
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) }
        x *
      OneHom.toFun
        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) } y
[PROOFSTEP]
rwa [MonoidalCategory.leftUnitor_hom_apply, ← A.one.map_smul] at h
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
r : R
a : (fun x => ↑A.X) r
⊢ ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := src✝.toFun,
                    map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : R),
                      ↑A.one (x • y) =
                        ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (x ⊗ₜ[R] ↑A.one y)) },
            map_zero' := (_ : ↑A.one 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : ↑(MonoidalCategory.tensorUnit (ModuleCat R))),
                  AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }
        r *
      a =
    a *
      ↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := src✝.toFun,
                    map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = AddHom.toFun src✝.toAddHom 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : R),
                      ↑A.one (x • y) =
                        ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (x ⊗ₜ[R] ↑A.one y)) },
            map_zero' := (_ : ↑A.one 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : ↑(MonoidalCategory.tensorUnit (ModuleCat R))),
                  AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }
        r
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
r : R
a : (fun x => ↑A.X) r
⊢ AddHom.toFun A.one.toAddHom r * a = a * AddHom.toFun A.one.toAddHom r
[PROOFSTEP]
have h₁ := LinearMap.congr_fun A.one_mul (r ⊗ₜ a)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
r : R
a : (fun x => ↑A.X) r
h₁ :
  ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (r ⊗ₜ[R] a) =
    ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (r ⊗ₜ[R] a)
⊢ AddHom.toFun A.one.toAddHom r * a = a * AddHom.toFun A.one.toAddHom r
[PROOFSTEP]
have h₂ := LinearMap.congr_fun A.mul_one (a ⊗ₜ r)
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
src✝ : MonoidalCategory.tensorUnit (ModuleCat R) ⟶ A.X := A.one
r : R
a : (fun x => ↑A.X) r
h₁ :
  ↑(CategoryTheory.MonoidalCategory.tensorHom A.one (𝟙 A.X) ≫ A.mul) (r ⊗ₜ[R] a) =
    ↑(CategoryTheory.MonoidalCategory.leftUnitor A.X).hom (r ⊗ₜ[R] a)
h₂ :
  ↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 A.X) A.one ≫ A.mul) (a ⊗ₜ[R] r) =
    ↑(CategoryTheory.MonoidalCategory.rightUnitor A.X).hom (a ⊗ₜ[R] r)
⊢ AddHom.toFun A.one.toAddHom r * a = a * AddHom.toFun A.one.toAddHom r
[PROOFSTEP]
exact h₁.trans h₂.symm
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
⊢ CategoryTheory.MonoidalCategory.tensorHom (Algebra.linearMap R ↑A) (𝟙 (of R ↑A)) ≫ mul' R ↑A =
    (CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom
[PROOFSTEP]
refine TensorProduct.ext <| LinearMap.ext_ring <| LinearMap.ext fun x => ?_
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ ↑(↑(compr₂ (TensorProduct.mk R ↑(MonoidalCategory.tensorUnit (ModuleCat R)) ↑(of R ↑A))
              (CategoryTheory.MonoidalCategory.tensorHom (Algebra.linearMap R ↑A) (𝟙 (of R ↑A)) ≫ mul' R ↑A))
          1)
      x =
    ↑(↑(compr₂ (TensorProduct.mk R ↑(MonoidalCategory.tensorUnit (ModuleCat R)) ↑(of R ↑A))
              (CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom)
          1)
      x
[PROOFSTEP]
rw [compr₂_apply, compr₂_apply, CategoryTheory.comp_apply]
  -- Porting note : this `dsimp` does nothing
      -- dsimp [AlgebraCat.id_apply, TensorProduct.mk_apply, Algebra.linearMap_apply,
      --   LinearMap.compr₂_apply, Function.comp_apply, RingHom.map_one,
      --   ModuleCat.MonoidalCategory.hom_apply, AlgebraCat.coe_comp,
      --   ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
      -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw`
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (Algebra.linearMap R ↑A) (𝟙 (of R ↑A)))
        (↑(↑(TensorProduct.mk R ↑(MonoidalCategory.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)) =
    ↑(CategoryTheory.MonoidalCategory.leftUnitor (of R ↑A)).hom
      (↑(↑(TensorProduct.mk R ↑(MonoidalCategory.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)
[PROOFSTEP]
erw [LinearMap.mul'_apply, MonoidalCategory.leftUnitor_hom_apply, ← Algebra.smul_def]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ (1, x).fst • ↑(𝟙 (of R ↑A)) (1, x).snd = 1 • x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
⊢ CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (Algebra.linearMap R ↑A) ≫ mul' R ↑A =
    (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom
[PROOFSTEP]
refine
  TensorProduct.ext <|
    LinearMap.ext fun x =>
      LinearMap.ext_ring
        ?_
          -- Porting note : this `dsimp` does nothing
              -- dsimp only [AlgebraCat.id_apply, TensorProduct.mk_apply, Algebra.linearMap_apply,
              --   LinearMap.compr₂_apply, Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply,
              --   AlgebraCat.coe_comp]
              -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw`
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ ↑(↑(compr₂ (TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R)))
              (CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (Algebra.linearMap R ↑A) ≫ mul' R ↑A))
          x)
      1 =
    ↑(↑(compr₂ (TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R)))
              (CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom)
          x)
      1
[PROOFSTEP]
erw [compr₂_apply, compr₂_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ ↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (Algebra.linearMap R ↑A) ≫ mul' R ↑A)
      (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R))) x) 1) =
    ↑(CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom
      (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R))) x) 1)
[PROOFSTEP]
rw [CategoryTheory.comp_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (Algebra.linearMap R ↑A))
        (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R))) x) 1)) =
    ↑(CategoryTheory.MonoidalCategory.rightUnitor (of R ↑A)).hom
      (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(MonoidalCategory.tensorUnit (ModuleCat R))) x) 1)
[PROOFSTEP]
erw [LinearMap.mul'_apply, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, ← Algebra.commutes, ← Algebra.smul_def]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x : ↑(of R ↑A)
⊢ (x, 1).snd • ↑(𝟙 (of R ↑A)) (x, 1).fst = 1 • x
[PROOFSTEP]
rw [id_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
⊢ CategoryTheory.MonoidalCategory.tensorHom (mul' R ↑A) (𝟙 (of R ↑A)) ≫ mul' R ↑A =
    (CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
      CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (mul' R ↑A) ≫ mul' R ↑A
[PROOFSTEP]
refine
  TensorProduct.ext <|
    TensorProduct.ext <|
      LinearMap.ext fun x =>
        LinearMap.ext fun y =>
          LinearMap.ext fun z =>
            ?_
              -- Porting note : this `dsimp` does nothing
                  -- dsimp only [AlgebraCat.id_apply, TensorProduct.mk_apply, LinearMap.compr₂_apply,
                  --   Function.comp_apply, ModuleCat.MonoidalCategory.hom_apply, AlgebraCat.coe_comp,
                  --   MonoidalCategory.associator_hom_apply]
                  -- Porting note : because `dsimp` is not effective, `rw` needs to be changed to `erw`
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x y z : ↑(of R ↑A)
⊢ ↑(↑(↑(compr₂ (TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A))
                  (compr₂
                    (TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
                    (CategoryTheory.MonoidalCategory.tensorHom (mul' R ↑A) (𝟙 (of R ↑A)) ≫ mul' R ↑A)))
              x)
          y)
      z =
    ↑(↑(↑(compr₂ (TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A))
                  (compr₂
                    (TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
                    ((CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
                      CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (mul' R ↑A) ≫ mul' R ↑A)))
              x)
          y)
      z
[PROOFSTEP]
rw [compr₂_apply, compr₂_apply, compr₂_apply, compr₂_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
  CategoryTheory.comp_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x y z : ↑(of R ↑A)
⊢ ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (mul' R ↑A) (𝟙 (of R ↑A)))
        (↑(↑(TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
              (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)) x) y))
          z)) =
    ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (mul' R ↑A))
        (↑(CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom
          (↑(↑(TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
                (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)) x) y))
            z)))
[PROOFSTEP]
erw [LinearMap.mul'_apply, LinearMap.mul'_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x y z : ↑(of R ↑A)
⊢ x * y * ↑(𝟙 (of R ↑A)) (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)) x) y, z).snd =
    ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (mul' R ↑A))
        (↑(CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom
          (↑(↑(TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
                (↑(↑(TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)) x) y))
            z)))
[PROOFSTEP]
rw [id_apply, TensorProduct.mk_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x y z : ↑(of R ↑A)
⊢ x * y * (x ⊗ₜ[R] y, z).snd =
    ↑(mul' R ↑A)
      (↑(CategoryTheory.MonoidalCategory.tensorHom (𝟙 (of R ↑A)) (mul' R ↑A))
        (↑(CategoryTheory.MonoidalCategory.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom
          (↑(↑(TensorProduct.mk R ↑(CategoryTheory.MonoidalCategory.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A))
                (x ⊗ₜ[R] y))
            z)))
[PROOFSTEP]
erw [TensorProduct.mk_apply, TensorProduct.mk_apply, id_apply, LinearMap.mul'_apply, LinearMap.mul'_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
A : AlgebraCat R
x y z : ↑(of R ↑A)
⊢ x * y * (x ⊗ₜ[R] y, z).snd = ((x, y).fst, (x, y).snd ⊗ₜ[R] (x ⊗ₜ[R] y, z).snd).fst * ((x, y).snd * (x ⊗ₜ[R] y, z).snd)
[PROOFSTEP]
simp only [LinearMap.mul'_apply, mul_assoc]
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ ((𝟭 (Mon_ (ModuleCat R))).obj A).one ≫
      {
        toAddHom :=
          { toFun := _root_.id,
            map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
        map_smul' :=
          (_ :
            ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
              AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a) =
                AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a)) } =
    ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).one
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
x✝ : ↑(MonoidalCategory.tensorUnit (ModuleCat R))
⊢ ↑(((𝟭 (Mon_ (ModuleCat R))).obj A).one ≫
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) })
      x✝ =
    ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).one x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ ((𝟭 (Mon_ (ModuleCat R))).obj A).mul ≫
      {
        toAddHom :=
          { toFun := _root_.id,
            map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
        map_smul' :=
          (_ :
            ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
              AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a) =
                AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a)) } =
    CategoryTheory.MonoidalCategory.tensorHom
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) }
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } ≫
      ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).mul
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ compr₂ (TensorProduct.mk R ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X)
      (((𝟭 (Mon_ (ModuleCat R))).obj A).mul ≫
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) }) =
    compr₂ (TensorProduct.mk R ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X)
      (CategoryTheory.MonoidalCategory.tensorHom
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) }
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) } ≫
        ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).mul)
[PROOFSTEP]
dsimp at *
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ compr₂ (TensorProduct.mk R ↑A.X ↑A.X)
      (A.mul ≫
        { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑A.X), x + y = x + y) },
          map_smul' := (_ : ∀ (r : R) (a : ↑A.X), r • a = r • a) }) =
    compr₂ (TensorProduct.mk R ↑A.X ↑A.X)
      (CategoryTheory.MonoidalCategory.tensorHom
          { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑A.X), x + y = x + y) },
            map_smul' := (_ : ∀ (r : R) (a : ↑A.X), r • a = r • a) }
          { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑A.X), x + y = x + y) },
            map_smul' := (_ : ∀ (r : R) (a : ↑A.X), r • a = r • a) } ≫
        mul' R ↑A.X)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).one ≫
      {
        toAddHom :=
          { toFun := _root_.id,
            map_add' :=
              (_ :
                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                  _root_.id (x + y) = _root_.id (x + y)) },
        map_smul' :=
          (_ :
            ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
              AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a) =
                AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a)) } =
    ((𝟭 (Mon_ (ModuleCat R))).obj A).one
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
x✝ : ↑(MonoidalCategory.tensorUnit (ModuleCat R))
⊢ ↑(((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).one ≫
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ :
                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                      _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) })
      x✝ =
    ↑((𝟭 (Mon_ (ModuleCat R))).obj A).one x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).mul ≫
      {
        toAddHom :=
          { toFun := _root_.id,
            map_add' :=
              (_ :
                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                  _root_.id (x + y) = _root_.id (x + y)) },
        map_smul' :=
          (_ :
            ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
              AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a) =
                AddHom.toFun
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) }
                  (r • a)) } =
    CategoryTheory.MonoidalCategory.tensorHom
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' :=
                (_ :
                  ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                    _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) }
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' :=
                (_ :
                  ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                    _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } ≫
      ((𝟭 (Mon_ (ModuleCat R))).obj A).mul
[PROOFSTEP]
refine TensorProduct.ext ?_
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ compr₂
      (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
        ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X)
      (((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).mul ≫
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' :=
                (_ :
                  ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                    _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) }) =
    compr₂
      (TensorProduct.mk R ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
        ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X)
      (CategoryTheory.MonoidalCategory.tensorHom
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ :
                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                      _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) }
          {
            toAddHom :=
              { toFun := _root_.id,
                map_add' :=
                  (_ :
                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                      _root_.id (x + y) = _root_.id (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                  AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a) =
                    AddHom.toFun
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) }
                      (r • a)) } ≫
        ((𝟭 (Mon_ (ModuleCat R))).obj A).mul)
[PROOFSTEP]
dsimp at *
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ compr₂ (TensorProduct.mk R ↑(of R ↑A.X) ↑(of R ↑A.X))
      (mul' R ↑A.X ≫
        { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑(of R ↑A.X)), x + y = x + y) },
          map_smul' := (_ : ∀ (r : R) (a : ↑(of R ↑A.X)), r • a = r • a) }) =
    compr₂ (TensorProduct.mk R ↑(of R ↑A.X) ↑(of R ↑A.X))
      (CategoryTheory.MonoidalCategory.tensorHom
          { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑(of R ↑A.X)), x + y = x + y) },
            map_smul' := (_ : ∀ (r : R) (a : ↑(of R ↑A.X)), r • a = r • a) }
          { toAddHom := { toFun := _root_.id, map_add' := (_ : ∀ (x y : ↑(of R ↑A.X)), x + y = x + y) },
            map_smul' := (_ : ∀ (r : R) (a : ↑(of R ↑A.X)), r • a = r • a) } ≫
        A.mul)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ Mon_.Hom.mk
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } ≫
      Mon_.Hom.mk
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' :=
                (_ :
                  ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                    _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } =
    𝟙 ((𝟭 (Mon_ (ModuleCat R))).obj A)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
x✝ : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X
⊢ ↑(Mon_.Hom.mk
              {
                toAddHom :=
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                      AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a) =
                        AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a)) } ≫
            Mon_.Hom.mk
              {
                toAddHom :=
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                      AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                  _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a) =
                        AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                  _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a)) }).hom
      x✝ =
    ↑(𝟙 ((𝟭 (Mon_ (ModuleCat R))).obj A)).hom x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
⊢ Mon_.Hom.mk
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' :=
                (_ :
                  ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                    _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                            _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } ≫
      Mon_.Hom.mk
        {
          toAddHom :=
            { toFun := _root_.id,
              map_add' := (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
          map_smul' :=
            (_ :
              ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a) =
                  AddHom.toFun
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                    (r • a)) } =
    𝟙 ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u
inst✝ : CommRing R
A : Mon_ (ModuleCat R)
x✝ : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X
⊢ ↑(Mon_.Hom.mk
              {
                toAddHom :=
                  { toFun := _root_.id,
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          _root_.id (x + y) = _root_.id (x + y)) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                      AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                  _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a) =
                        AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                  _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a)) } ≫
            Mon_.Hom.mk
              {
                toAddHom :=
                  { toFun := _root_.id,
                    map_add' :=
                      (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                      AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a) =
                        AddHom.toFun
                          { toFun := _root_.id,
                            map_add' :=
                              (_ :
                                ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) }
                          (r • a)) }).hom
      x✝ =
    ↑(𝟙 ((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A)).hom x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y : Mon_ (ModuleCat R)} (f : X ⟶ Y),
    (𝟭 (Mon_ (ModuleCat R))).map f ≫
        ((fun A =>
              Iso.mk
                (Mon_.Hom.mk
                  {
                    toAddHom :=
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                          AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a) =
                            AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a)) })
                (Mon_.Hom.mk
                  {
                    toAddHom :=
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a) =
                            AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a)) }))
            Y).hom =
      ((fun A =>
              Iso.mk
                (Mon_.Hom.mk
                  {
                    toAddHom :=
                      { toFun := _root_.id,
                        map_add' :=
                          (_ : ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X), _root_.id (x + y) = _root_.id (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (a : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                          AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a) =
                            AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (Mon_ (ModuleCat R))).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a)) })
                (Mon_.Hom.mk
                  {
                    toAddHom :=
                      { toFun := _root_.id,
                        map_add' :=
                          (_ :
                            ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                              _root_.id (x + y) = _root_.id (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (a : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                          AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a) =
                            AddHom.toFun
                              { toFun := _root_.id,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((functor ⋙ MonModuleEquivalenceAlgebra.inverse).obj A).X),
                                      _root_.id (x + y) = _root_.id (x + y)) }
                              (r • a)) }))
            X).hom ≫
        (functor ⋙ MonModuleEquivalenceAlgebra.inverse).map f
[PROOFSTEP]
aesop_cat
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y : AlgebraCat R} (f : X ⟶ Y),
    (MonModuleEquivalenceAlgebra.inverse ⋙ functor).map f ≫
        ((fun A =>
              Iso.mk
                {
                  toRingHom :=
                    {
                      toMonoidHom :=
                        { toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                  x * y) },
                      map_zero' :=
                        (_ :
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              0 =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              0),
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) })
                                (x + y) =
                              OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) })
                                (x + y)) },
                  commutes' :=
                    (_ :
                      ∀ (r : R),
                        OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                            ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                (x ⊗ₜ[R] y) =
                                              x * y) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r) =
                          OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                            ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                (x ⊗ₜ[R] y) =
                                              x * y) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r)) }
                {
                  toRingHom :=
                    {
                      toMonoidHom :=
                        { toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                      map_zero' :=
                        (_ :
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              0 =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              0),
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                (x + y) =
                              OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                (x + y)) },
                  commutes' :=
                    (_ :
                      ∀ (r : R),
                        OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                            x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r) =
                          OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                            x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                {
                  toRingHom :=
                    {
                      toMonoidHom :=
                        { toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                  x * y) },
                      map_zero' :=
                        (_ :
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              0 =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              0),
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) })
                                (x + y) =
                              OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) })
                                (x + y)) },
                  commutes' :=
                    (_ :
                      ∀ (r : R),
                        OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                            ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                (x ⊗ₜ[R] y) =
                                              x * y) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r) =
                          OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                            ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                (x ⊗ₜ[R] y) =
                                              x * y) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                          (x ⊗ₜ[R] y) =
                                                        x * y) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r)) }
                {
                  toRingHom :=
                    {
                      toMonoidHom :=
                        { toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                      map_zero' :=
                        (_ :
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              0 =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              0),
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                            OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                (x + y) =
                              OneHom.toFun
                                (↑{
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                (x + y)) },
                  commutes' :=
                    (_ :
                      ∀ (r : R),
                        OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                            x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r) =
                          OneHom.toFun
                            (↑↑{
                                  toMonoidHom :=
                                    {
                                      toOneHom :=
                                        { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                      map_mul' :=
                                        (_ :
                                          ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                            x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                  map_zero' :=
                                    (_ :
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0 =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          0),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y) =
                                          OneHom.toFun
                                            (↑{
                                                toOneHom :=
                                                  { toFun := _root_.id,
                                                    map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                                map_mul' :=
                                                  (_ :
                                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                            (x + y)) })
                            (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r)) })
            X).hom ≫
        (𝟭 (AlgebraCat R)).map f
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
X✝ Y✝ : AlgebraCat R
f✝ : X✝ ⟶ Y✝
⊢ (MonModuleEquivalenceAlgebra.inverse ⋙ functor).map f✝ ≫
      ((fun A =>
            Iso.mk
              {
                toRingHom :=
                  {
                    toMonoidHom :=
                      { toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                              ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) = x * y) },
                    map_zero' :=
                      (_ :
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                        x * y) })
                            0 =
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                        x * y) })
                            0),
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              (x + y) =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              (x + y)) },
                commutes' :=
                  (_ :
                    ∀ (r : R),
                      OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r) =
                        OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r)) }
              {
                toRingHom :=
                  {
                    toMonoidHom :=
                      { toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                              x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                    map_zero' :=
                      (_ :
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                            0 =
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                            0),
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              (x + y) =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              (x + y)) },
                commutes' :=
                  (_ :
                    ∀ (r : R),
                      OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r) =
                        OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r)) })
          Y✝).hom =
    ((fun A =>
            Iso.mk
              {
                toRingHom :=
                  {
                    toMonoidHom :=
                      { toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                              ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) = x * y) },
                    map_zero' :=
                      (_ :
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                        x * y) })
                            0 =
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                        x * y) })
                            0),
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              (x + y) =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                        ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) (x ⊗ₜ[R] y) =
                                          x * y) })
                              (x + y)) },
                commutes' :=
                  (_ :
                    ∀ (r : R),
                      OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r) =
                        OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                          ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                              (x ⊗ₜ[R] y) =
                                            x * y) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                  ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                      (x ⊗ₜ[R] y) =
                                                    x * y) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : ↑(_root_.algebraMap R ↑A) 1 = 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)),
                                                    ↑(mul' R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A))
                                                        (x ⊗ₜ[R] y) =
                                                      x * y) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((MonModuleEquivalenceAlgebra.inverse ⋙ functor).obj A)) r)) }
              {
                toRingHom :=
                  {
                    toMonoidHom :=
                      { toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                              x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                    map_zero' :=
                      (_ :
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                            0 =
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                            0),
                    map_add' :=
                      (_ :
                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                          OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              (x + y) =
                            OneHom.toFun
                              (↑{ toOneHom := { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                  map_mul' :=
                                    (_ :
                                      ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                        x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                              (x + y)) },
                commutes' :=
                  (_ :
                    ∀ (r : R),
                      OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r) =
                        OneHom.toFun
                          (↑↑{
                                toMonoidHom :=
                                  {
                                    toOneHom :=
                                      { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                    map_mul' :=
                                      (_ :
                                        ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                          x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) },
                                map_zero' :=
                                  (_ :
                                    OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0 =
                                      OneHom.toFun
                                        (↑{
                                            toOneHom :=
                                              { toFun := _root_.id, map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                            map_mul' :=
                                              (_ :
                                                ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                  x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                        0),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                      OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y) =
                                        OneHom.toFun
                                          (↑{
                                              toOneHom :=
                                                { toFun := _root_.id,
                                                  map_one' := (_ : 1 = ↑(_root_.algebraMap R ↑A) 1) },
                                              map_mul' :=
                                                (_ :
                                                  ∀ (x y : ↑((𝟭 (AlgebraCat R)).obj A)),
                                                    x * y = ↑(mul' R ↑((𝟭 (AlgebraCat R)).obj A)) (x ⊗ₜ[R] y)) })
                                          (x + y)) })
                          (↑(_root_.algebraMap R ↑((𝟭 (AlgebraCat R)).obj A)) r)) })
          X✝).hom ≫
      (𝟭 (AlgebraCat R)).map f✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ ∀ {X Y : Mon_ (ModuleCat R)} (f : X ⟶ Y),
    (functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).map f ≫
        ((fun A =>
              Iso.mk
                {
                  toAddHom :=
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                            _root_.id (x + y) = _root_.id (x + y)) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (x : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                        AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x) =
                          AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x)) }
                {
                  toAddHom :=
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)), _root_.id (x + y) = _root_.id (x + y)) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (x : ↑((Mon_.forget (ModuleCat R)).obj A)),
                        AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x) =
                          AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x)) })
            Y).hom =
      ((fun A =>
              Iso.mk
                {
                  toAddHom :=
                    { toFun := _root_.id,
                      map_add' :=
                        (_ :
                          ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                            _root_.id (x + y) = _root_.id (x + y)) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (x : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                        AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x) =
                          AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((functor ⋙ forget₂ (AlgebraCat R) (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x)) }
                {
                  toAddHom :=
                    { toFun := _root_.id,
                      map_add' :=
                        (_ : ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)), _root_.id (x + y) = _root_.id (x + y)) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (x : ↑((Mon_.forget (ModuleCat R)).obj A)),
                        AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x) =
                          AddHom.toFun
                            { toFun := _root_.id,
                              map_add' :=
                                (_ :
                                  ∀ (x y : ↑((Mon_.forget (ModuleCat R)).obj A)),
                                    _root_.id (x + y) = _root_.id (x + y)) }
                            (c • x)) })
            X).hom ≫
        (Mon_.forget (ModuleCat R)).map f
[PROOFSTEP]
aesop_cat