awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M N K : ModuleCat R
⊢ Hom.hom (Iso.inv (α_ M N K)) =
    (↑(LinearEquiv.symm (TensorProduct.assoc R (↑M : Type u) (↑N : Type u) (↑K : Type u))) :
      TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)) →ₗ[R]
        TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
K L M N : ModuleCat R
f : K ⟶ L
g : M ⟶ N
k : (↑K : Type u)
m : (↑M : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) K M) (f ⊗ₘ g) :
          (a : (↑(K ⊗ M) : Type u)) → (↑(L ⊗ N) : Type u))
        (k ⊗ₜ[R] m) :
      (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑K : Type u)) → (↑L : Type u))
          k ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              g :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
      TensorProduct R (↑L : 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.Basic
Goal:
R : Type u
inst : CommRing R
L M N : ModuleCat R
f : M ⟶ N
l : (↑L : Type u)
m : (↑M : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) L M) (L ◁ f) :
          (a : (↑(L ⊗ M) : Type u)) → (↑(L ⊗ N) : Type u))
        (l ⊗ₜ[R] m) :
      (↑(tensorObj (𝒞 := moduleCategory R) L N) : Type u))
    (l ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑M : Type u)) → (↑N : Type u))
          m :
      TensorProduct R (↑L : 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.Basic
Goal:
R : Type u
inst : CommRing R
L M : ModuleCat R
f : L ⟶ M
N : ModuleCat R
l : (↑L : 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) L N) (f ▷ N) :
          (a : (↑(L ⊗ N) : Type u)) → (↑(M ⊗ N) : Type u))
        (l ⊗ₜ[R] n) :
      (↑(tensorObj (𝒞 := moduleCategory R) M N) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑L : Type u)) → (↑M : Type u))
          l ⊗ₜ[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.Basic
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
r : R
m : (↑M : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
          tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M) (Iso.hom (λ_ M)) :
        (a : (↑(𝟙_ (ModuleCat R) ⊗ M) : Type u)) → (↑M : Type u))
      (r ⊗ₜ[R] m) =
    r • m

Tactic:
TensorProduct.lid_tmul m r

Premises used: TensorProduct.lid_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
m : (↑M : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M) (Iso.inv (λ_ M)) :
          (a : (↑M : Type u)) → (↑(𝟙_ (ModuleCat R) ⊗ M) : Type u))
        m :
      (↑(tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M) : Type u))
    (1 ⊗ₜ[R] m : TensorProduct R (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u) (↑M : Type u))

Tactic:
TensorProduct.lid_symm_apply m

Premises used: TensorProduct.lid_symm_apply, Quotient, TensorProduct, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
m : (↑M : Type u)
r : R
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
          tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) (Iso.hom (ρ_ M)) :
        (a : (↑(M ⊗ 𝟙_ (ModuleCat R)) : Type u)) → (↑M : Type u))
      (m ⊗ₜ[R] r) =
    r • m

Tactic:
TensorProduct.rid_tmul m r

Premises used: TensorProduct.rid_tmul
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M : ModuleCat R
m : (↑M : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (Y :=
            tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) (Iso.inv (ρ_ M)) :
          (a : (↑M : Type u)) → (↑(M ⊗ 𝟙_ (ModuleCat R)) : Type u))
        m :
      (↑(tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))) : Type u))
    (m ⊗ₜ[R] 1 : TensorProduct R (↑M : Type u) (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u))

Tactic:
TensorProduct.rid_symm_apply m

Premises used: Quotient, TensorProduct.rid_symm_apply, TensorProduct, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M N K : ModuleCat R
m : (↑M : Type u)
n : (↑N : Type u)
k : (↑K : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) M (tensorObj (𝒞 := moduleCategory R) N K)) : 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) M N) K) (Iso.hom (α_ M N K)) :
          (a : (↑((M ⊗ N) ⊗ K) : Type u)) → (↑(M ⊗ N ⊗ K) : Type u))
        (m ⊗ₜ[R] n ⊗ₜ[R] k) :
      (↑(tensorObj (𝒞 := moduleCategory R) M (tensorObj (𝒞 := moduleCategory R) N K)) : Type u))
    (m ⊗ₜ[R] (n ⊗ₜ[R] k) : TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : 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.Basic
Goal:
R : Type u
inst : CommRing R
M N K : ModuleCat R
m : (↑M : Type u)
n : (↑N : Type u)
k : (↑K : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) M N) K) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (X :=
            tensorObj (𝒞 := moduleCategory R) M (tensorObj (𝒞 := moduleCategory R) N K)) (Iso.inv (α_ M N K)) :
          (a : (↑(M ⊗ N ⊗ K) : Type u)) → (↑((M ⊗ N) ⊗ K) : Type u))
        (m ⊗ₜ[R] (n ⊗ₜ[R] k)) :
      (↑(tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) M N) K) : Type u))
    (m ⊗ₜ[R] n ⊗ₜ[R] k : TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : 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.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ : ModuleCat R
f : (↑M₁ : Type u) → (↑M₂ : Type u) → (↑M₃ : Type u)
h₁ : ∀ (m₁ m₂ : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f (m₁ + m₂) n = f m₁ n + f m₂ n
h₂ : ∀ (a : R) (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f (a • m) n = a • f m n
h₃ : ∀ (m : (↑M₁ : Type u)) (n₁ n₂ : (↑M₂ : Type u)), f m (n₁ + n₂) = f m n₁ + f m n₂
h₄ : ∀ (a : R) (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)), f m (a • n) = a • f m n
m : (↑M₁ : Type u)
n : (↑M₂ : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (tensorLift f h₁ h₂ h₃ h₄) :
        (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u))
      (m ⊗ₜ[R] n) =
    f m n

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) M₁ M₂ ⟶ M₃
h :
  ∀ (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u)) ((Hom.hom f : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
      ((Hom.hom g : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
h₁ :
  ∀ (x : (↑M₁ : Type u)) (x_1 : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
                      TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ :=
                      RingHom.id R) (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u))
                      (Hom.hom f) :
                    (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
                  (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
                x :
              (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
            (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
          x_1 :
        (↑M₃ : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
                      TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ :=
                      RingHom.id R) (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u))
                      (Hom.hom g) :
                    (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
                  (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
                x :
              (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
            (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
          x_1 :
        (↑M₃ : Type u))
⊢ Eq (α := (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
    (LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
        TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
        (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) :
      (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
    (LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
        TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
        (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g) :
      (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) M₁ M₂ ⟶ M₃
h :
  ∀ (m : (↑M₁ : Type u)) (n : (↑M₂ : Type u)),
    Eq (α := (↑M₃ : Type u)) ((Hom.hom f : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
      ((Hom.hom g : (a : (↑(M₁ ⊗ M₂) : Type u)) → (↑M₃ : Type u)) (m ⊗ₜ[R] n) : (↑M₃ : Type u))
x : (↑M₁ : Type u)
x_1 : (↑M₂ : Type u)
⊢ Eq (α := (↑M₃ : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
                    TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ :=
                    RingHom.id R) (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) :
                  (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
                (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
              x :
            (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
          (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
        x_1 :
      (↑M₃ : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑M₁ : Type u)) (N := (↑M₂ : Type u)) (P :=
                    TensorProduct R (↑M₁ : Type u) (↑M₂ : Type u)) (Q := (↑M₃ : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ :=
                    RingHom.id R) (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g) :
                  (↑M₁ : Type u) →ₗ[R] (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
                (a : (↑M₁ : Type u)) → (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u))
              x :
            (↑M₂ : Type u) →ₗ[R] (↑M₃ : Type u)) :
          (a : (↑M₂ : Type u)) → (↑M₃ : Type u))
        x_1 :
      (↑M₃ : Type u))

Tactic:
apply h
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) (tensorObj (𝒞 := moduleCategory R) M₁ M₂) M₃ ⟶ M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑((M₁ ⊗ M₂) ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) g :
            (a : (↑((M₁ ⊗ M₂) ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) :
        (↑M₄ : Type u))
⊢ f = g

Tactic:
hom_ext <| TensorProduct.ext_threefold h

Premises used: TensorProduct.ext_threefold, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) M₁ (tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶ M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
rw : Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (α_ _ _ _).hom]

Premises used: CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) M₁ (tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶ M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
⊢ Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g

Tactic:
tensor_ext₃' h

Premises used: ModuleCat.MonoidalCategory.tensor_ext₃'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : tensorObj (𝒞 := moduleCategory R) M₁ (tensorObj (𝒞 := moduleCategory R) M₂ M₃) ⟶ M₄
h :
  ∀ (m₁ : (↑M₁ : Type u)) (m₂ : (↑M₂ : Type u)) (m₃ : (↑M₃ : Type u)),
    Eq (α := (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) g :
            (a : (↑(M₁ ⊗ M₂ ⊗ M₃) : Type u)) → (↑M₄ : Type u))
          (m₁ ⊗ₜ[R] (m₂ ⊗ₜ[R] m₃)) :
        (↑M₄ : Type u))
⊢ Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g

Tactic:
exact tensor_ext₃' h

Premises used: ModuleCat.MonoidalCategory.tensor_ext₃'
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)

Tactic:
⟨?_, ?_, ?_, ?_⟩

Premises used: CategoryTheory.MonoidalPreadditive.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
refine_1 :
  ∀ {X Y Z : ModuleCat R},
    Eq (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ 0) 0
refine_2 :
  ∀ {X Y Z : ModuleCat R},
    Eq (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (0 ▷ X) 0
refine_3 :
  ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z),
    X ◁ (f + g) =
      HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g)
refine_4 :
  ∀ {X Y Z : ModuleCat R} (f g : Y ⟶ Z),
    (f + g) ▷ X =
      HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X)
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
refine_1 :
  Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) X Y) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (Hom.hom (X ◁ 0)) (Hom.hom 0)
⊢ Eq (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ 0) 0

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) X Y) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (Hom.hom (X ◁ 0)) (Hom.hom 0)

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, Quotient, TensorProduct, TensorProduct.ext, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
refine_1 :
  ∀ (x : (↑X : Type u)) (y : (↑Y : Type u)),
    Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom (X ◁ 0)) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
      (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                      TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                      (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom 0) :
                    (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                  (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
                x :
              (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
            (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
          y :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) X Y) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (Hom.hom (X ◁ 0)) (Hom.hom 0)

Tactic:
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

Premises used: LinearMap.ext, TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                    TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom (X ◁ 0)) :
                  (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
              x :
            (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
          (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X : Type u)) (N := (↑Y : Type u)) (P :=
                    TensorProduct R (↑X : Type u) (↑Y : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑X : Type u) (↑Y : Type u)) (Hom.hom 0) :
                  (↑X : Type u) →ₗ[R] (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
                (a : (↑X : Type u)) → (↑Y : Type u) →ₗ[R] (↑(X ⊗ Z) : Type u))
              x :
            (↑Y : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) :
          (a : (↑Y : Type u)) → (↑(X ⊗ Z) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))

Tactic:
simp [ModuleCat.hom_whiskerLeft]

Premises used: ModuleCat.hom_whiskerLeft
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
refine_2 :
  Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) Y X) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (Hom.hom (0 ▷ X)) (Hom.hom 0)
⊢ Eq (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (0 ▷ X) 0

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
⊢ Eq (α :=
    (↑(tensorObj (𝒞 := moduleCategory R) Y X) : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (Hom.hom (0 ▷ X)) (Hom.hom 0)

Tactic:
TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)

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