awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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))
⊢ f = g
have rw : Iso.hom (α_ M₁ M₂ M₃) ≫ f = Iso.hom (α_ M₁ M₂ M₃) ≫ g
Tactic: rw [← cancel_epi (α_ _ _ _).hom]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)
have refine_1 : ∀ {X Y Z : ModuleCat R},
  Eq (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ 0) 0
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)
have refine_2 : ∀ {X Y Z : ModuleCat R},
  Eq (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (0 ▷ X) 0
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)
have 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)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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)
⊢ MonoidalPreadditive.{u, u + 1} (ModuleCat R)
have 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)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
⊢ Eq (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ 0) 0
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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)
have 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))
Tactic: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
⊢ Eq (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (0 ▷ X) 0
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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)
have refine_2 : ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
  Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom (0 ▷ X)) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom 0) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
Tactic: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
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)
have refine_3 : Hom.hom (X ◁ (f + g)) =
  Hom.hom
    (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
⊢ Hom.hom (X ◁ (f + g)) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) (X ◁ f) (X ◁ g))
have refine_3 : ∀ (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 ◁ (f + g))) :
                  (↑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
                      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z)
                        (X ◁ f) (X ◁ g))) :
                  (↑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: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
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)
have refine_4 : Hom.hom ((f + g) ▷ X) =
  Hom.hom
    (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
f g : Y ⟶ Z
⊢ Hom.hom ((f + g) ▷ X) =
    Hom.hom
      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) (f ▷ X) (g ▷ X))
have refine_4 : ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
  Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom ((f + g) ▷ X)) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u))
                    (Hom.hom
                      (HAdd.hAdd (α := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X)
                        (f ▷ X) (g ▷ X))) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
Tactic: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
⊢ MonoidalLinear R (ModuleCat R)
have refine_1 : ∀ (X : ModuleCat R) {Y Z : ModuleCat R} (r : R) (f : Y ⟶ Z),
  X ◁ (r • f) =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
refine_1 :
  ∀ (X : ModuleCat R) {Y Z : ModuleCat R} (r : R) (f : Y ⟶ Z),
    X ◁ (r • f) =
      HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f)
⊢ MonoidalLinear R (ModuleCat R)
have refine_2 : ∀ (r : R) {Y Z : ModuleCat R} (f : Y ⟶ Z) (X : ModuleCat R),
  (r • f) ▷ X =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f)
have refine_1 : Hom.hom (X ◁ (r • f)) =
  Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
⊢ Hom.hom (X ◁ (r • f)) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z) r (X ◁ f))
have 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 ◁ (r • f))) :
                  (↑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
                      (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) X Y ⟶ tensorObj (𝒞 := moduleCategory R) X Z)
                        r (X ◁ f))) :
                  (↑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: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : ModuleCat R
r : R
f : Y ⟶ Z
x : (↑X : Type u)
y : (↑Y : Type u)
⊢ (Hom.hom (X ◁ (r • f)) : (a : TensorProduct R (↑X : Type u) (↑Y : Type u)) → (↑(X ⊗ Z) : Type u)) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) r
      ((Hom.hom (X ◁ f) : (a : TensorProduct R (↑X : Type u) (↑Y : Type u)) → (↑(X ⊗ Z) : Type u)) (x ⊗ₜ[R] y) :
        (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u))
have refine_1 : x ⊗ₜ[R]
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
          (r • f) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      y =
  HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) X Z) : Type u)) r
    (x ⊗ₜ[R]
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              f :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          y :
      TensorProduct R (↑X : Type u) (↑Z : Type u))
Tactic: erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
Y Z : ModuleCat R
f : Y ⟶ Z
X : ModuleCat R
⊢ (r • f) ▷ X =
    HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X)
have refine_2 : Hom.hom ((r • f) ▷ X) =
  Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
Y Z : ModuleCat R
f : Y ⟶ Z
X : ModuleCat R
⊢ Hom.hom ((r • f) ▷ X) =
    Hom.hom (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X) r (f ▷ X))
have refine_2 : ∀ (x : (↑Y : Type u)) (y : (↑X : Type u)),
  Eq (α := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u)) (Hom.hom ((r • f) ▷ X)) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
    (((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑Y : Type u)) (N := (↑X : Type u)) (P :=
                    TensorProduct R (↑Y : Type u) (↑X : Type u)) (Q :=
                    (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R)
                    (σ₃₄ := RingHom.id R) (TensorProduct.mk R (↑Y : Type u) (↑X : Type u))
                    (Hom.hom
                      (HSMul.hSMul (β := tensorObj (𝒞 := moduleCategory R) Y X ⟶ tensorObj (𝒞 := moduleCategory R) Z X)
                        r (f ▷ X))) :
                  (↑Y : Type u) →ₗ[R] (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
                (a : (↑Y : Type u)) → (↑X : Type u) →ₗ[R] (↑(Z ⊗ X) : Type u))
              x :
            (↑X : Type u) →ₗ[R] (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) :
          (a : (↑X : Type u)) → (↑(Z ⊗ X) : Type u))
        y :
      (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
Tactic: refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
Y Z : ModuleCat R
f : Y ⟶ Z
X : ModuleCat R
x : (↑Y : Type u)
y : (↑X : Type u)
⊢ (Hom.hom ((r • f) ▷ X) : (a : TensorProduct R (↑Y : Type u) (↑X : Type u)) → (↑(Z ⊗ X) : Type u)) (x ⊗ₜ[R] y) =
    HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) r
      ((Hom.hom (f ▷ X) : (a : TensorProduct R (↑Y : Type u) (↑X : Type u)) → (↑(Z ⊗ X) : Type u)) (x ⊗ₜ[R] y) :
        (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u))
have refine_2 : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) (r • f) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      x ⊗ₜ[R]
    y =
  HSMul.hSMul (β := (↑(tensorObj (𝒞 := moduleCategory R) Z X) : Type u)) r
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) f :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          x ⊗ₜ[R]
        y :
      TensorProduct R (↑Z : Type u) (↑X : Type u))
Tactic: erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M N P : ModuleCat R
f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P
⊢ (fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
        Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
      ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
          (ofHom₂ (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u)) (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
            N ⟶ of R (unop (op M) ⟶ P)))
        f) =
    f
have hf : Hom.hom
    ((fun (f : N ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) P) ↦
        Iso.hom (β_ M N) ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
      ((fun (f : Functor.obj (MonoidalCategory.tensorLeft M) N ⟶ P) ↦
          (ofHom₂ (LinearMap.compr₂ (TensorProduct.mk R (↑N : Type u) (↑M : Type u)) (Hom.hom (Iso.hom (β_ N M) ≫ f))) :
            N ⟶ of R (unop (op M) ⟶ P)))
        f)) =
  Hom.hom f
Tactic: ext : 1