awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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
have hf : ∀ (x : (↑M : Type u)) (y : (↑N : Type u)),
  Eq (α := (↑P : Type u))
    (((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)) :
            (↑(Functor.obj (MonoidalCategory.tensorLeft M) N) : Type u) →ₗ[R] (↑P : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u))
        (x ⊗ₜ[R] y) :
      (↑P : Type u))
    ((Hom.hom f : (a : TensorProduct R (↑M : Type u) (↑N : Type u)) → (↑P : Type u)) (x ⊗ₜ[R] y) : (↑P : Type u))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M X' X Y : ModuleCat R
f : X' ⟶ X
g : X ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) Y
⊢ Eq (α := Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)
    (((M.monoidalClosedHomEquiv X' Y).symm :
          (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
        (f ≫ g) :
      Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)
    (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
        ((M.monoidalClosedHomEquiv X Y).symm :
            (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
          g :
      Functor.obj (MonoidalCategory.tensorLeft M) X' ⟶ Y)
have hf : Eq (α := (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u))
  (Hom.hom
    (((M.monoidalClosedHomEquiv X' Y).symm :
        (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
      (f ≫ g)))
  (Hom.hom
    (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
      ((M.monoidalClosedHomEquiv X Y).symm :
          (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
        g))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M X' X Y : ModuleCat R
f : X' ⟶ X
g : X ⟶ Functor.obj (Functor.obj (linearCoyoneda R (ModuleCat R)) (op M)) Y
⊢ Eq (α := (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u))
    (Hom.hom
      (((M.monoidalClosedHomEquiv X' Y).symm :
          (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
        (f ≫ g)))
    (Hom.hom
      (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
        ((M.monoidalClosedHomEquiv X Y).symm :
            (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) → (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
          g))
have hf : ∀ (x : (↑M : Type u)) (y : (↑X' : Type u)),
  Eq (α := (↑Y : Type u))
    (((Hom.hom
              (((M.monoidalClosedHomEquiv X' Y).symm :
                  (a : X' ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                    (MonoidalCategory.tensorLeft M).obj X' ⟶ Y)
                (f ≫ g)) :
            (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
        (x ⊗ₜ[R] y) :
      (↑Y : Type u))
    (((Hom.hom
              (CategoryTheory.Functor.map (MonoidalCategory.tensorLeft M) f ≫
                ((M.monoidalClosedHomEquiv X Y).symm :
                    (a : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y) →
                      (MonoidalCategory.tensorLeft M).obj X ⟶ Y)
                  g) :
            (↑(Functor.obj (MonoidalCategory.tensorLeft M) X') : Type u) →ₗ[R] (↑Y : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑X' : Type u)) → (↑Y : Type u))
        (x ⊗ₜ[R] y) :
      (↑Y : Type u))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
⊢ Eq (α := Functor.obj (ihom M ⋙ tensorLeft M) N ⟶ Functor.obj (𝟭 (ModuleCat R)) N) (NatTrans.app (ihom.ev M) N)
    (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id)))
have rw : MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N)) =
  ↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
        (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
          TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
      (LinearMap.lcomp R (↑N : Type u)
          (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
        LinearMap.flip LinearMap.id))
Tactic: rw [← MonoidalClosed.uncurry_id_eq_ev]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id))
have hf : Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) =
  Hom.hom
    (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
          (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
            TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
        (LinearMap.lcomp R (↑N : Type u)
            (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
          LinearMap.flip LinearMap.id)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed (goal)
Goal:
R : Type u
inst : CommRing R
M N : ModuleCat R
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) =
    Hom.hom
      (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u) (↑N : Type u) :
            (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
              TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
          (LinearMap.lcomp R (↑N : Type u)
              (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
            LinearMap.flip LinearMap.id)))
have hf : ∀ (x : (↑M : Type u)) (y : (↑(Functor.obj (ihom M) N) : Type u)),
  Eq (α := (↑N : Type u))
    ((Hom.hom (MonoidalClosed.uncurry (𝟙 (Functor.obj (ihom M) N))) :
          (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
        (x ⊗ₜ[R] y) :
      (↑N : Type u))
    (((Hom.hom
              (↟((TensorProduct.uncurry (RingHom.id R) (↑M : Type u) (↑(Functor.obj (ihom M) N) : Type u)
                      (↑N : Type u) :
                    (a : (↑M : Type u) →ₗ[R] (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u)) →
                      TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u) →ₗ[R] (↑N : Type u))
                  (LinearMap.lcomp R (↑N : Type u)
                      (↑homLinearEquiv : (unop (op M) ⟶ N) →ₗ[R] (↑(unop (op M)) : Type u) →ₗ[R] (↑N : Type u)) ∘ₗ
                    LinearMap.flip LinearMap.id))) :
            (↑(tensorObj (𝒞 := moduleCategory R) M (Functor.obj (ihom M) N)) : Type u) →ₗ[R] (↑N : Type u)) :
          (a : TensorProduct R (↑M : Type u) (↑((ihom M).obj N) : Type u)) → (↑N : Type u))
        (x ⊗ₜ[R] y) :
      (↑N : Type u))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f)
have hf : Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))
have hf : ∀ (x : (↑X₁ : Type u)) (y : (↑X₂ : Type u)),
  Eq (α := (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
    ((Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) :
          (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
        (x ⊗ₜ[R] y) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
    ((Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f)) :
          (a : TensorProduct R (↑X₁ : Type u) (↑X₂ : Type u)) → (↑(Y₂ ⊗ Y₁) : Type u))
        (x ⊗ₜ[R] y) :
      (↑(MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y₂ Y₁) : Type u))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
⊢ Iso.hom (α_ X Y Z) ≫
      Iso.hom (X.braiding (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) Y Z)) ≫ Iso.hom (α_ Y Z X) =
    (X.braiding Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (X.braiding Z).hom
have hf : 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: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
⊢ 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)
have 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))
Tactic: apply TensorProduct.ext_threefold
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
⊢ 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
have 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
Tactic: apply (cancel_epi (α_ X Y Z).hom).1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
⊢ 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
have 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)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
X Y Z : SemimoduleCat R
⊢ 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)
have 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))
Tactic: apply TensorProduct.ext_threefold
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
x x_1 : SemimoduleCat R
⊢ (x.braiding x_1).hom ≫ (x_1.braiding x).hom = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1)
have hf : Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) =
  Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric (goal)
Goal:
R : Type u
inst : CommSemiring R
x x_1 : SemimoduleCat R
⊢ Hom.hom ((x.braiding x_1).hom ≫ (x_1.braiding x).hom) =
    Hom.hom (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := moduleCategory R) x x_1))
have 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))
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings (hypothesis)
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)
⊢ HSMul.hSMul (α := (↑(R'.obj Y) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R'.map f) :
            (a : (↑(R'.obj X) : Type u)) → (↑(R'.obj Y) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  RingCat.carrier) (α.app X) :
                (a : (↑(R.obj X) : Type u)) → (↑(R'.obj X) : Type u))
              r :
            (↑(R'.obj X) : 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))
have eq : 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
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings (goal)
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
⊢ (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
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ RingCat.Hom.hom (cR.ι.app X) = (RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))
have a : ∀ (x : (↑(R.obj X) : Type w)),
  Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) :
          (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
⊢ Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) :
          (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
have a : Eq (α := (↑cR.pt : Type w))
  ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
  (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
      x :
    (↑cR.pt : Type w))
Tactic: dsimp