awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Localization (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
T : ShortComplex (ModuleCat.{v, u} R)
h : T.Exact
⊢ ShortComplex.Exact (T.map (localizedModuleFunctor S))
have rw : ∀
  (h :
    Function.Exact (M := (↑T.X₁ : Type v)) (N := (↑T.X₂ : Type v)) (P := (↑T.X₃ : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) T.f) :
        (a : (↑T.X₁ : Type v)) → (↑T.X₂ : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) T.g) :
        (a : (↑T.X₂ : Type v)) → (↑T.X₃ : Type v))),
  Function.Exact (M := (↑(ShortComplex.X₁ (T.map (localizedModuleFunctor S))) : Type v)) (N :=
    (↑(ShortComplex.X₂ (T.map (localizedModuleFunctor S))) : Type v)) (P :=
    (↑(ShortComplex.X₃ (T.map (localizedModuleFunctor S))) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (Localization (M := R) S)) ↦
          LinearMap.{u, u, v, v} (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := carrier) (X := ShortComplex.X₁ (T.map (localizedModuleFunctor S)))
          (ShortComplex.f (T.map (localizedModuleFunctor S)))) :
      (a : (↑(T.map (localizedModuleFunctor S)).X₁ : Type v)) → (↑(T.map (localizedModuleFunctor S)).X₂ : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (Localization (M := R) S)) ↦
          LinearMap.{u, u, v, v} (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (↑x1 : Type v)
            (↑x2 : Type v))
          (CC := carrier) (X := ShortComplex.X₂ (T.map (localizedModuleFunctor S)))
          (ShortComplex.g (T.map (localizedModuleFunctor S)))) :
      (a : (↑(T.map (localizedModuleFunctor S)).X₂ : Type v)) → (↑(T.map (localizedModuleFunctor S)).X₃ : Type v))
Tactic: rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Localization (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S)
have this : Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
Tactic: have := ((Functor.exact_tfae _).out 1 3).mp (ModuleCat.localizedModuleFunctor_map_exact S)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Localization (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
have this : Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
Tactic: have := ((Functor.exact_tfae _).out 1 3).mp (ModuleCat.localizedModuleFunctor_map_exact S)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat.{u_1, u} R
N : SemimoduleCat.{u_2, u} R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (TensorProduct.{u, u_1, u_2} R (↑M : Type u_1) (↑N : Type u_2)))
have hf : Hom.hom (tensorHom (𝟙 M) (𝟙 N)) = Hom.hom (𝟙 (of R (TensorProduct.{u, u_1, u_2} R (↑M : Type u_1) (↑N : Type u_2))))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat.{u_1, u} R
N : SemimoduleCat.{u_2, u} R
⊢ Hom.hom (tensorHom (𝟙 M) (𝟙 N)) = Hom.hom (𝟙 (of R (TensorProduct.{u, u_1, u_2} R (↑M : Type u_1) (↑N : Type u_2))))
have hf : LinearMap.compr₂ₛₗ (mk R (↑M : Type u_1) (↑N : Type u_2)) (Hom.hom (tensorHom (𝟙 M) (𝟙 N))) =
  LinearMap.compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R (↑M : Type u_1) (↑N : Type u_2))
    (Hom.hom (𝟙 (of R (TensorProduct.{u, u_1, u_2} R (↑M : Type u_1) (↑N : Type u_2)))))
Tactic: apply TensorProduct.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat.{u_1, u} R
X₂ Y₂ Z₂ : SemimoduleCat.{u_2, u} R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)
have hf : Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂) = Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ Y₁ Z₁ : SemimoduleCat.{u_1, u} R
X₂ Y₂ Z₂ : SemimoduleCat.{u_2, u} R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂) = Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))
have hf : LinearMap.compr₂ₛₗ (mk R (↑X₁ : Type u_1) (↑X₂ : Type u_2)) (Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)) =
  LinearMap.compr₂ₛₗ (mk R (↑X₁ : Type u_1) (↑X₂ : Type u_2)) (Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)))
Tactic: apply TensorProduct.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ : SemimoduleCat.{u_1, u} R
X₂ : SemimoduleCat.{u_2, u} R
X₃ : SemimoduleCat.{u_3, u} R
Y₁ : SemimoduleCat.{u_1, u} R
Y₂ : SemimoduleCat.{u_2, u} R
Y₃ : SemimoduleCat.{u_3, u} R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)
have hf : Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
  Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ : SemimoduleCat.{u_1, u} R
X₂ : SemimoduleCat.{u_2, u} R
X₃ : SemimoduleCat.{u_3, u} R
Y₁ : SemimoduleCat.{u_1, u} R
Y₂ : SemimoduleCat.{u_2, u} R
Y₃ : SemimoduleCat.{u_3, u} R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) =
    Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃))
have hf : ∀ (x : (↑X₁ : Type u_1)) (y : (↑X₂ : Type u_2)) (z : (↑X₃ : Type u_3)),
  Eq (α := (↑(tensorObj Y₁ (tensorObj Y₂ Y₃)) : Type (max (max u_1 u_2) u_3)))
    ((Hom.hom (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) :
          (a : (↑X₁ : Type u_1) ⊗[R] (↑X₂ : Type u_2) ⊗[R] (↑X₃ : Type u_3)) →
            (↑(tensorObj Y₁ (tensorObj Y₂ Y₃)) : Type (max (max u_1 u_2) u_3)))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj Y₁ (tensorObj Y₂ Y₃)) : Type (max (max u_1 u_2) u_3)))
    ((Hom.hom ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)) :
          (a : (↑X₁ : Type u_1) ⊗[R] (↑X₂ : Type u_2) ⊗[R] (↑X₃ : Type u_3)) →
            (↑(tensorObj Y₁ (tensorObj Y₂ Y₃)) : Type (max (max u_1 u_2) u_3)))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj Y₁ (tensorObj Y₂ Y₃)) : Type (max (max u_1 u_2) u_3)))
Tactic: apply TensorProduct.ext_threefold
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
W : SemimoduleCat.{u_1, u} R
X : SemimoduleCat.{u_2, u} R
Y : SemimoduleCat.{u_3, u} R
Z : SemimoduleCat.{u_4, u} R
⊢ whiskerRight (associator W X Y).hom Z ≫
      Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z))
have hf : Hom.hom
    (whiskerRight (associator W X Y).hom Z ≫
      Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) =
  Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
W : SemimoduleCat.{u_1, u} R
X : SemimoduleCat.{u_2, u} R
Y : SemimoduleCat.{u_3, u} R
Z : SemimoduleCat.{u_4, u} R
⊢ Hom.hom
      (whiskerRight (associator W X Y).hom Z ≫
        Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) =
    Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z)))
have hf : ∀ (w : (↑W : Type u_1)) (x : (↑X : Type u_2)) (y : (↑Y : Type u_3)) (z : (↑Z : Type u_4)),
  Eq (α := (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
    ((Hom.hom
            (whiskerRight (associator W X Y).hom Z ≫
              Iso.hom (associator W (tensorObj X Y) Z) ≫ whiskerLeft W (associator X Y Z).hom) :
          (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
            (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
    ((Hom.hom ((associator (tensorObj W X) Y Z).hom ≫ Iso.hom (associator W X (tensorObj Y Z))) :
          (a : (↑W : Type u_1) ⊗[R] (↑X : Type u_2) ⊗[R] (↑Y : Type u_3) ⊗[R] (↑Z : Type u_4)) →
            (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
        (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj W (tensorObj X (tensorObj Y Z))) : Type (max (max (max u_1 u_2) u_3) u_4)))
Tactic: apply TensorProduct.ext_fourfold
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f
have hf : Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) = Hom.hom ((leftUnitor M).hom ≫ f)
have hf : LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
  LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f))
Tactic: apply TensorProduct.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
      (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f))
have hf : ∀ (x : (↑M : Type u)),
  Eq (α := (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u))
                  (Hom.hom (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) :
                (↑(of R R) : Type u) →ₗ[R] (↑M : Type u) →ₗ[R] (↑N : Type u)) :
              (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
            1 :
          (a : (↑M : Type u)) → (↑N : Type u))
        x :
      (↑N : Type u))
    (((LinearMap.compr₂ₛₗ (mk R (↑(of R R) : Type u) (↑M : Type u)) (Hom.hom ((leftUnitor M).hom ≫ f)) :
              (a : R) → (↑M : Type u) →ₗ[R] (↑N : Type u))
            1 :
          (a : (↑M : Type u)) → (↑N : Type u))
        x :
      (↑N : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f
have hf : Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) = Hom.hom ((rightUnitor M).hom ≫ f)
have hf : LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
    (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
  LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f))
Tactic: apply TensorProduct.ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
      (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) =
    LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f))
have hf : ∀ (x : (↑M : Type u)),
  Eq (α := (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u))
                  (Hom.hom (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) :
                (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
              x :
            (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
          (a : R) → (↑N : Type u))
        1 :
      (↑N : Type u))
    ((((LinearMap.compr₂ₛₗ (mk R (↑M : Type u) (↑(of R R) : Type u)) (Hom.hom ((rightUnitor M).hom ≫ f)) :
                (a : (↑M : Type u)) → (↑(of R R) : Type u) →ₗ[R] (↑N : Type u))
              x :
            (↑(of R R) : Type u) →ₗ[R] (↑N : Type u)) :
          (a : R) → (↑N : Type u))
        1 :
      (↑N : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
⊢ Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)
have hf : Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
  Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M N : SemimoduleCat R
⊢ Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))
have hf : ∀ (x : (↑M : Type u)) (y : (↑(of R R) : Type u)) (z : (↑N : Type u)),
  Eq (α := (↑(tensorObj M N) : Type u))
    ((Hom.hom (Iso.hom (associator M (of R R) N) ≫ tensorHom (𝟙 M) (leftUnitor N).hom) :
          (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj M N) : Type u))
    ((Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N)) :
          (a : (↑M : Type u) ⊗[R] (↑(of R R) : Type u) ⊗[R] (↑N : Type u)) → (↑(tensorObj M N) : Type u))
        (x ⊗ₜ[R] y ⊗ₜ[R] z) :
      (↑(tensorObj M N) : Type u))
Tactic: apply TensorProduct.ext_threefold
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ : SemimoduleCat R
f g : MonoidalCategoryStruct.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))
⊢ LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) =
    LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g)
have h₁ : ∀ (x : (↑M₁ : Type u)) (x_1 : (↑M₂ : Type u)),
  Eq (α := (↑M₃ : Type u))
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom f) :
                (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₂ₛₗ (TensorProduct.mk R (↑M₁ : Type u) (↑M₂ : Type u)) (Hom.hom g) :
                (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: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M₁ M₂ M₃ M₄ : SemimoduleCat R
f g :
  MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) M₁
      (MonoidalCategoryStruct.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 : SemimoduleCat 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 : SemimoduleCat 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
x : ModuleCat R
⊢ CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.leftUnitor x)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategory.tensorIso
            (Iso.symm
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
            (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
        MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
have hf : SemimoduleCat.Hom.hom
    (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.leftUnitor x))) =
  SemimoduleCat.Hom.hom
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R)))
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
          MonoidalCategory.tensorIso
            (Iso.symm
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))
            (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))) ≪≫
        MonoidalCategoryStruct.leftUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
Goal:
R : Type u
inst : CommRing R
x : ModuleCat R
⊢ CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.rightUnitor x)) =
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
            (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
        MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
have hf : SemimoduleCat.Hom.hom
    (CategoryTheory.Functor.map (Equivalence.functor equivalenceSemimoduleCat)
      (Iso.hom (MonoidalCategoryStruct.rightUnitor x))) =
  SemimoduleCat.Hom.hom
    ((Iso.symm
            (Iso.refl
              (MonoidalCategoryStruct.tensorObj (𝒞 := SemimoduleCat.moduleCategory R)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)
                (Functor.obj (Equivalence.functor equivalenceSemimoduleCat)
                  (MonoidalCategoryStruct.tensorUnit (ModuleCat R) (𝒞 := moduleCategory R))))) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x))
            (Iso.symm
              (Iso.refl
                (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R) (𝒞 := SemimoduleCat.moduleCategory R))))) ≪≫
        MonoidalCategoryStruct.rightUnitor (Functor.obj (Equivalence.functor equivalenceSemimoduleCat) x)).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: ext