awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
hf :
  ∀ (x : (↑X : Type u)) (y : (↑Y : Type u)) (z : (↑Z : Type u)),
    Eq (α :=
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
        Type u))
      ((Hom.hom
              (Iso.hom (α_ X Y Z) ≫
                Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫
                  Iso.hom (α_ Y Z X)) :
            (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(Y ⊗ Z ⊗ X) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
          Type u))
      ((Hom.hom ((X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom) :
            (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(Y ⊗ Z ⊗ X) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
          Type u))
⊢ Hom.hom
      (Iso.hom (α_ X Y Z) ≫
        Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫ Iso.hom (α_ Y Z X)) =
    Hom.hom ((X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom)

Tactic:
apply TensorProduct.ext_threefold

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
x : (↑X : Type u)
y : (↑Y : Type u)
z : (↑Z : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
      Type u))
    ((Hom.hom
            (Iso.hom (α_ X Y Z) ≫
              Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫
                Iso.hom (α_ Y Z X)) :
          (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(Y ⊗ Z ⊗ X) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
        Type u))
    ((Hom.hom ((X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom) :
          (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑(Y ⊗ Z ⊗ X) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X)) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
apply :
  Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫
        ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y) =
    Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y
⊢ Iso.inv (α_ X Y Z) ≫
      ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y) =
    X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y

Tactic:
apply (cancel_epi (α_ X Y Z).hom).1

Premises used: Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
hf :
  Hom.hom
      (Iso.hom (α_ X Y Z) ≫
        Iso.inv (α_ X Y Z) ≫
          ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y)) =
    Hom.hom (Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y)
⊢ Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫
        ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y) =
    Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
hf :
  ∀ (x : (↑X : Type u)) (y : (↑Y : Type u)) (z : (↑Z : Type u)),
    Eq (α :=
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
        Type u))
      ((Hom.hom
              (Iso.hom (α_ X Y Z) ≫
                Iso.inv (α_ X Y Z) ≫
                  ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫
                    Iso.inv (α_ Z X Y)) :
            (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) →
              (↑((Z ⊗ X) ⊗ Y) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
          Type u))
      ((Hom.hom (Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y) :
            (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) →
              (↑((Z ⊗ X) ⊗ Y) : Type u))
          (x ⊗ₜ[R] y ⊗ₜ[R] z) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
          Type u))
⊢ Hom.hom
      (Iso.hom (α_ X Y Z) ≫
        Iso.inv (α_ X Y Z) ≫
          ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y)) =
    Hom.hom (Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y)

Tactic:
apply TensorProduct.ext_threefold

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
x : (↑X : Type u)
y : (↑Y : Type u)
z : (↑Z : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
      Type u))
    ((Hom.hom
            (Iso.hom (α_ X Y Z) ≫
              Iso.inv (α_ X Y Z) ≫
                ((MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) X Y).braiding Z).hom ≫ Iso.inv (α_ Z X Y)) :
          (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑((Z ⊗ X) ⊗ Y) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
        Type u))
    ((Hom.hom (Iso.hom (α_ X Y Z) ≫ X ◁ (Y.braiding Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (X.braiding Z).hom ▷ Y) :
          (a : TensorProduct R (TensorProduct R (↑X : Type u) (↑Y : Type u)) (↑Z : Type u)) → (↑((Z ⊗ X) ⊗ Y) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Z X) Y) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
x x_1 : SemimoduleCat R
hf :
  Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
⊢ (x.braiding x_1).hom ≫ (x_1.braiding x).hom = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
x x_1 : SemimoduleCat R
hf :
  ∀ (x_2 : (↑x : Type u)) (y : (↑x_1 : Type u)),
    Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1)) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
⊢ Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
x x_1 : SemimoduleCat R
hf hf₁ hf₂ hf₃ :
  ∀ (x_2 : (↑x : Type u)) (y : (↑x_1 : Type u)),
    Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1)) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
⊢ ∀ (x_2 : (↑x : Type u)) (y : (↑x_1 : Type u)),
    Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))
      ((Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1)) :
            (a : TensorProduct R (↑x : Type u) (↑x_1 : Type u)) → (↑(x ⊗ x_1) : Type u))
          (x_2 ⊗ₜ[R] y) :
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1) : Type u))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
m : (↑M : Type u)
n : (↑N : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N M) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X := MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) (Iso.hom (β_ M N)) :
          (a : (↑(M ⊗ N) : Type u)) → (↑(N ⊗ M) : Type u))
        (m ⊗ₜ[R] n) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N M) : Type u))
    (n ⊗ₜ[R] m : TensorProduct R (↑N : Type u) (↑M : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
m : (↑M : Type u)
n : (↑N : Type u)
⊢ Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X := MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) N M) (Iso.inv (β_ M N)) :
          (a : (↑(N ⊗ M) : Type u)) → (↑(M ⊗ N) : Type u))
        (n ⊗ₜ[R] m) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    (m ⊗ₜ[R] n : TensorProduct R (↑M : Type u) (↑N : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
A B C D : SemimoduleCat R
⊢ tensorμ A B C D =
    ↟(↑(TensorProduct.tensorTensorTensorComm R (↑A : Type u) (↑B : Type u) (↑C : Type u) (↑D : Type u)) :
        TensorProduct R (TensorProduct R (↑A : Type u) (↑B : Type u))
            (TensorProduct R (↑C : Type u) (↑D : Type u)) →ₗ[R]
          TensorProduct R (TensorProduct R (↑A : Type u) (↑C : Type u)) (TensorProduct R (↑B : Type u) (↑D : Type u)))

Tactic:
SemimoduleCat.hom_ext <| TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext₂ fun _ _ =>
    TensorProduct.ext <| LinearMap.ext₂ fun _ _ => rfl

Premises used: SemimoduleCat.hom_ext, LinearMap.ext₂, TensorProduct.ext, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommSemiring R
A B C D : SemimoduleCat R
x : (↑A : Type u)
y : (↑B : Type u)
z : (↑C : Type u)
w : (↑D : Type u)
⊢ Eq (α :=
    (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A C)
          (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) B D)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemimoduleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
            (X :=
            MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A B)
              (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) C D))
            (tensorμ A B C D) :
          (a : (↑((A ⊗ B) ⊗ C ⊗ D) : Type u)) → (↑((A ⊗ C) ⊗ B ⊗ D) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) A C)
            (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) B D)) :
        Type u))
    (x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w) :
      TensorProduct R (TensorProduct R (↑A : Type u) (↑C : Type u)) (TensorProduct R (↑B : Type u) (↑D : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
m : (↑M : Type u)
n : (↑N : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) N M) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) M N) (Iso.hom (β_ M N)) :
          (a : (↑(M ⊗ N) : Type u)) → (↑(N ⊗ M) : Type u))
        (m ⊗ₜ[R] n) :
      (↑(tensorObj (𝒞 := moduleCategory R) N M) : Type u))
    (n ⊗ₜ[R] m : TensorProduct R (↑N : Type u) (↑M : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
m : (↑M : Type u)
n : (↑N : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) N M) (Iso.inv (β_ M N)) :
          (a : (↑(N ⊗ M) : Type u)) → (↑(M ⊗ N) : Type u))
        (n ⊗ₜ[R] m) :
      (↑(tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    (m ⊗ₜ[R] n : TensorProduct R (↑M : Type u) (↑N : Type u))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommRing R
A B C D : ModuleCat R
⊢ tensorμ A B C D =
    ↟(↑(TensorProduct.tensorTensorTensorComm R (↑A : Type u) (↑B : Type u) (↑C : Type u) (↑D : Type u)) :
        TensorProduct R (TensorProduct R (↑A : Type u) (↑B : Type u))
            (TensorProduct R (↑C : Type u) (↑D : Type u)) →ₗ[R]
          TensorProduct R (TensorProduct R (↑A : Type u) (↑C : Type u)) (TensorProduct R (↑B : Type u) (↑D : Type u)))

Tactic:
ModuleCat.hom_ext <| TensorProduct.ext <| TensorProduct.ext <| LinearMap.ext₂ fun _ _ =>
    TensorProduct.ext <| LinearMap.ext₂ fun _ _ => rfl

Premises used: LinearMap.ext₂, ModuleCat.hom_ext, TensorProduct.ext, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
Goal:
R : Type u
inst : CommRing R
A B C D : ModuleCat R
x : (↑A : Type u)
y : (↑B : Type u)
z : (↑C : Type u)
w : (↑D : Type u)
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) A C)
          (tensorObj (𝒞 := moduleCategory R) B D)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) A B)
              (tensorObj (𝒞 := moduleCategory R) C D))
            (tensorμ A B C D) :
          (a : (↑((A ⊗ B) ⊗ C ⊗ D) : Type u)) → (↑((A ⊗ C) ⊗ B ⊗ D) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] (z ⊗ₜ[R] w)) :
      (↑(tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) A C)
            (tensorObj (𝒞 := moduleCategory R) B D)) :
        Type u))
    (x ⊗ₜ[R] z ⊗ₜ[R] (y ⊗ₜ[R] w) :
      TensorProduct R (TensorProduct R (↑A : Type u) (↑C : Type u)) (TensorProduct R (↑B : Type u) (↑D : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
M' : PresheafOfModules.{v, v', u', u} R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : (↑(R.obj X) : Type u)
x : (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X)) : Type v)
⊢ Eq (α := (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (R.map f ≫ α.app Y) : (a : (↑(R.obj X) : Type u)) → (↑(R'.obj Y) : Type u)) r :
      (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (α.app X ≫ R'.map f) : (a : (↑(R.obj X) : Type u)) → (↑(R'.obj Y) : Type u)) r :
      (↑(R'.obj Y) : Type u))

Tactic:
have eq := RingHom.congr_fun (congrArg RingCat.Hom.hom <| α.naturality f) r
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
M' : PresheafOfModules.{v, v', u', u} R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : (↑(R.obj X) : Type u)
x : (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X)) : Type v)
eq :
  Eq (α := (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (α.app Y) : (a : (↑(R.obj Y) : Type u)) → (↑(R'.obj Y) : Type u))
        ((RingCat.Hom.hom (R.map f) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u)) r : (↑(R.obj Y) : Type u)) :
      (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (R'.map f) : (a : (↑(R'.obj X) : Type u)) → (↑(R'.obj Y) : Type u))
        ((RingCat.Hom.hom (α.app X) : (a : (↑(R.obj X) : Type u)) → (↑(R'.obj X) : Type u)) r :
          (↑(R'.obj X) : Type u)) :
      (↑(R'.obj Y) : Type u))
⊢ HSMul.hSMul (α := (↑(R'.obj Y) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
      ((RingCat.Hom.hom (α.app Y) : (a : (↑(R.obj Y) : Type u)) → (↑(R'.obj Y) : Type u))
          ((RingCat.Hom.hom (R.map f) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u)) r :
            (↑(R.obj Y) : Type u)) :
        (↑(R'.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M'.map f) :
            (a : (↑(M'.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v)) =
    HSMul.hSMul (α := (↑(R.obj X) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).obj (M'.obj Y))) :
        Type v))
      ((RingHom.id (↑(R.obj X) : Type u) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj X) : Type u)) r :
        (↑(R.obj X) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M'.map f) :
            (a : (↑(M'.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
X_1 Y_1 : PresheafOfModules.{v, v', u', u} R'
φ' : X_1 ⟶ Y_1
X Y : Cᵒᵖ
f : X ⟶ Y
hf :
  ∀ (x : (↑((X_1.restrictScalarsObj α).obj X) : Type v)),
    Eq (α :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
      ((ModuleCat.Hom.hom
              ((X_1.restrictScalarsObj α).map f ≫
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                  ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).map (φ'.app Y))) :
            (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
                Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
      ((ModuleCat.Hom.hom
              ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).map (φ'.app X) ≫
                (Y_1.restrictScalarsObj α).map f) :
            (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
                Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
⊢ (X_1.restrictScalarsObj α).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).map (φ'.app Y)) =
    (ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).map (φ'.app X) ≫ (Y_1.restrictScalarsObj α).map f

Tactic:
ext x