awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
x y : R
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R]
            (@ConcreteCategory.hom _ (moduleCategory R)
                  (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier _ _
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
                (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
              y :
          (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑A : Type u)) :
      (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (x ⊗ₜ[R]
            (@ConcreteCategory.hom _ (moduleCategory R)
                  (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) carrier _ _
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
                (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
              y :
          (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑A : Type u)) :
      (↑A : Type u))

Tactic:
have h := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A).symm) (x ⊗ₜ η[A] y)
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
a : (↑A : Type u)
dsimp :
  HMul.hMul (α := (↑A : Type u))
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))
      a =
    HMul.hMul (β := (↑A : Type u)) a
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))
⊢ HMul.hMul (α := (↑A : Type u))
      ((let __src :
              (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                (↑A : Type u) :=
              Hom.hom η;
            { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
              R →+* (↑A : Type u) } :
            (a : R) → (↑A : Type u))
          r :
        (↑A : Type u))
      a =
    HMul.hMul (β := (↑A : Type u)) a
      ((let __src :
              (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) : Type u) →ₗ[R]
                (↑A : Type u) :=
              Hom.hom η;
            { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R) → (↑A : Type u))
          r :
        (↑A : Type u))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
a : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))

Tactic:
have h₁ := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (one_mul A)) (r ⊗ₜ a)
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
a : (↑A : Type u)
h₁ :
  Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))

Tactic:
have h₂ := LinearMap.congr_fun (ModuleCat.hom_ext_iff.mp (mul_one A)) (a ⊗ₜ r)
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
a : (↑A : Type u)
h₁ :
  Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
h₂ :
  Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))
⊢ HMul.hMul (α := (↑A : Type u))
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))
      a =
    HMul.hMul (β := (↑A : Type u)) a
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))

Tactic:
h₁.trans h₂.symm

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, Eq.symm, AddCon.toQuotient, FreeAddMonoid.sumAux, Eq.trans
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
a : (↑A : Type u)
h₁ :
  Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)) A) : Type u)) →
            (↑A : Type u))
        (r ⊗ₜ[R] a) :
      (↑A : Type u))
h₂ :
  Eq (α := (↑A : Type u))
    ((Hom.hom (MonoidalCategoryStruct.whiskerLeft A η ≫ μ) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))
    ((Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
          (a : (↑(MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (ModuleCat R))) : Type u)) →
            (↑A : Type u))
        (a ⊗ₜ[R] r) :
      (↑A : Type u))
⊢ HMul.hMul (α := (↑A : Type u))
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))
      a =
    HMul.hMul (β := (↑A : Type u)) a
      ((Hom.hom η : (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u)) r :
        (↑A : Type u))

Tactic:
exact h₁.trans h₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : ModuleCat R
inst_1 : MonObj A
r : R
⊢ Eq (α := (↑A : Type u)) ((Algebra.algebraMap R (↑A : Type u) : (a : R) → (↑A : Type u)) r : (↑A : Type u))
    ((@ConcreteCategory.hom _ (moduleCategory R) (fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            carrier _ _ (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) A η :
          (a : (↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) : Type u)) → (↑A : Type u))
        r :
      (↑A : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
hf :
  Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) (of R (↑A : Type u))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R (↑A : Type u))) (of R (↑A : Type u)))
        (↟(mul' R (↑A : Type u)))))
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor (of R (↑A : Type u)))))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
        (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) (of R (↑A : Type u)))
      (of R (↑A : Type u)))
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
      (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R (↑A : Type u))) (of R (↑A : Type u)))
      (↟(mul' R (↑A : Type u))))
    (Iso.hom (MonoidalCategoryStruct.leftUnitor (of R (↑A : Type u))))

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)) (of R (↑A : Type u))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R (↑A : Type u))) (of R (↑A : Type u)))
        (↟(mul' R (↑A : Type u)))))
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.leftUnitor (of R (↑A : Type u)))))

Tactic:
TensorProduct.ext <| LinearMap.ext_ring <| LinearMap.ext fun x => ?_

Premises used: LinearMap.ext, Quotient, LinearMap.ext_ring, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x : (↑(of R (↑A : Type u)) : Type u)
⊢ HSMul.hSMul (α := R) (β := (↑A : Type u)) (1, x).1
      ((LinearMap.id : (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u)) (1, x).2 :
        (↑(of R (↑A : Type u)) : Type u)) =
    HSMul.hSMul (α := R) 1 x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
hf :
  Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
            (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
        (↟(mul' R (↑A : Type u)))))
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u)))))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
        (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
      (of R (↑A : Type u)))
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
      (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
      (↟(mul' R (↑A : Type u))))
    (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u))))

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u))
            (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(Algebra.linearMap R (↑A : Type u))))
        (↟(mul' R (↑A : Type u)))))
    (Hom.hom (Iso.hom (MonoidalCategoryStruct.rightUnitor (of R (↑A : Type u)))))

Tactic:
TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext_ring ?_

Premises used: LinearMap.ext, Quotient, LinearMap.ext_ring, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x : (↑(of R (↑A : Type u)) : Type u)
⊢ HSMul.hSMul (α := R) (β := (↑A : Type u)) (x, 1).2
      ((LinearMap.id : (a : (↑(of R (↑A : Type u)) : Type u)) → (↑(of R (↑A : Type u)) : Type u)) (x, 1).1 :
        (↑(of R (↑A : Type u)) : Type u)) =
    HSMul.hSMul (α := R) 1 x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
hf :
  Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
            (of R (↑A : Type u))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u))) (↟(mul' R (↑A : Type u)))))
    (Hom.hom
      (Iso.hom (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u)) (of R (↑A : Type u))) ≫
        CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
          (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u))))
          (↟(mul' R (↑A : Type u)))))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
        (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (of R (↑A : Type u)))
      (of R (↑A : Type u)))
    (CategoryStruct.comp (Y :=
      MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
      (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u))) (↟(mul' R (↑A : Type u))))
    (Iso.hom (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u)) (of R (↑A : Type u))) ≫
      CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u)))) (↟(mul' R (↑A : Type u))))

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
            (of R (↑A : Type u))) :
        Type u) →ₗ[R]
      (↑(of R (↑A : Type u)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
        (MonoidalCategoryStruct.whiskerRight (↟(mul' R (↑A : Type u))) (of R (↑A : Type u))) (↟(mul' R (↑A : Type u)))))
    (Hom.hom
      (Iso.hom (MonoidalCategoryStruct.associator (of R (↑A : Type u)) (of R (↑A : Type u)) (of R (↑A : Type u))) ≫
        CategoryStruct.comp (Y :=
          MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (of R (↑A : Type u)) (of R (↑A : Type u)))
          (MonoidalCategoryStruct.whiskerLeft (of R (↑A : Type u)) (↟(mul' R (↑A : Type u))))
          (↟(mul' R (↑A : Type u)))))

Tactic:
TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext fun x => LinearMap.ext fun y =>
      LinearMap.ext fun z => ?_

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : AlgCat R
x y z : (↑(of R (↑A : Type u)) : Type u)
⊢ x * y * z = ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 * ((x, y).2 * (x ⊗ₜ[R] y, z).2)

Tactic:
simp only [_root_.mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
hf :
  Eq.{u + 1} (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X
            (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X) :
        Type u) →ₗ[R]
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
    (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }))
    (Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ))
⊢ Eq.{u + 1} (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X
        (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X ⟶
      (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X)
    (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
    (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
        (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
      μ)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
⊢ Eq.{u + 1} (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X
            (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X) :
        Type u) →ₗ[R]
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
    (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }))
    (Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ))

Tactic:
TensorProduct.ext rfl

Premises used: Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
⊢ Eq.{u + 1} (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X
            (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X) :
        Type u) →ₗ[R]
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
    (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }))
    (Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ))

Tactic:
exact TensorProduct.ext rfl

Premises used: TensorProduct.ext, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
hf :
  Eq.{u + 1} (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X
            (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X) :
        Type u) →ₗ[R]
      (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u))
    (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }))
    (Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ))
⊢ Eq.{u + 1} (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
        (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X
        (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X ⟶
      (Functor.obj (𝟭 (Mon (ModuleCat R))) A).X)
    (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
    (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
        (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
      μ)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
⊢ Eq.{u + 1} (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X
            (Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X) :
        Type u) →ₗ[R]
      (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u))
    (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }))
    (Hom.hom
      (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
          (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
        μ))

Tactic:
TensorProduct.ext ?_

Premises used: Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient