awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
ι : Type v
inst_2 : DecidableEq ι
inst_3 : Preorder ι
G : ι → Type v
inst_4 : (i : ι) → AddCommGroup (G i)
inst_5 : (i : ι) → Module.{u, v} R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst_6 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f i j h) : (a : G i) → G j)
s : Cocone (directLimitDiagram G f)
m : Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f) ⟶ s.pt
h : ∀ (j : ι), NatTrans.app (Cocone.ι (directLimitCocone G f)) j ≫ m = s.ι.app j
this : s.ι.app = fun (i : ι) ↦ ↟(DirectLimit.of R ι (fun (i : ι) ↦ G i) (fun (i j : ι) (H : i ≤ j) ↦ f i j H) i) ≫ m
x : (↑(Cocone.pt (F := directLimitDiagram G f) (directLimitCocone G f)) : Type v)
⊢ Eq (α := (↑s.pt : Type v))
    ((Hom.hom m : (a : (↑(directLimitCocone G f).pt : Type v)) → (↑s.pt : Type v)) x : (↑s.pt : Type v))
    ((Hom.hom (↟(Module.DirectLimit.lift R ι G f (fun (i : ι) ↦ Hom.hom (s.ι.app i)) ⋯)) :
          (a : (↑(directLimitCocone G f).pt : Type v)) → (↑s.pt : Type v))
        x :
      (↑s.pt : Type v))

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submonoid R
⊢ Small.{v, max v u} (LocalizedModule S M)

Tactic:
small_of_surjective (IsLocalizedModule.mk'_surjective S (LocalizedModule.mkLinearMap S M))

Premises used: small_of_surjective, IsLocalizedModule.mk'_surjective, LocalizedModule.mkLinearMap
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
S : Submonoid R
⊢ IsScalarTower.{u, u, v} R (Localization (M := R) S) (↑(M.localizedModule S) : Type v)

Tactic:
(equivShrink (LocalizedModule S M)).symm.isScalarTower R (Localization S)

Premises used: LocalizedModule, Set.Mem, Localization, Equiv.isScalarTower, ModuleCat.carrier, Equiv.symm, equivShrink
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
S : Submonoid R
⊢ IsLocalizedModule.{u, v, v} (M := (↑M : Type v)) (M' := (↑(M.localizedModule S) : Type v)) S
    ((↑(LinearEquiv.symm (Shrink.linearEquiv R (LocalizedModule.{u, v} S (↑M : Type v)))) :
        LocalizedModule S (↑M : Type v) →ₗ[R] Shrink.{v, max u v} (LocalizedModule S (↑M : Type v))) ∘ₗ
      LocalizedModule.mkLinearMap S (↑M : Type v))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat.{v, u} R
f : X ⟶ Y
g : Y ⟶ Z
hf :
  ∀ (x : (↑(X.localizedModule S) : Type v)),
    Eq (α := (↑(Z.localizedModule S) : Type v))
      ((Hom.hom (localizedModuleMap S (f ≫ g)) :
            (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
          x :
        (↑(Z.localizedModule S) : Type v))
      ((Hom.hom (localizedModuleMap S f ≫ localizedModuleMap S g) :
            (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
          x :
        (↑(Z.localizedModule S) : Type v))
⊢ Eq (α := X.localizedModule S ⟶ Z.localizedModule S) (localizedModuleMap S (f ≫ g))
    (localizedModuleMap S f ≫ localizedModuleMap S g)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X Y Z : ModuleCat.{v, u} R
f : X ⟶ Y
g : Y ⟶ Z
x : (↑(X.localizedModule S) : Type v)
⊢ Eq (α := (↑(Z.localizedModule S) : Type v))
    ((Hom.hom (localizedModuleMap S (f ≫ g)) :
          (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
        x :
      (↑(Z.localizedModule S) : Type v))
    ((Hom.hom (localizedModuleMap S f ≫ localizedModuleMap S g) :
          (a : (↑(X.localizedModule S) : Type v)) → (↑(Z.localizedModule S) : Type v))
        x :
      (↑(Z.localizedModule S) : Type v))

Tactic:
simp [IsLocalizedModule.map_comp' S _ (Y.localizedModuleMkLinearMap S)]

Premises used: IsLocalizedModule.map_comp', ModuleCat.localizedModuleMkLinearMap
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
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
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))
⊢ ShortComplex.Exact (T.map (localizedModuleFunctor S))

Tactic:
rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] at h ⊢

Premises used: CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
T : ShortComplex (ModuleCat.{v, u} R)
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:
IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
    (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ h

Premises used: CategoryTheory.ShortComplex.X₁, LocalizedModule.liftOn, ModuleCat.localizedModuleMkLinearMap, IsLocalizedModule.map_exact, LocalizedModule.lift', CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
T : ShortComplex (ModuleCat.{v, u} R)
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:
exact IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
    (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ h

Premises used: CategoryTheory.ShortComplex.X₁, ModuleCat.localizedModuleMkLinearMap, IsLocalizedModule.map_exact, CategoryTheory.ShortComplex.X₃, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)

Tactic:
have := ((Functor.exact_tfae _).out 1 3).mp (ModuleCat.localizedModuleFunctor_map_exact S)
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this :
  Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S)

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this :
  Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
⊢ Limits.PreservesFiniteLimits (localizedModuleFunctor S)

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this :
  Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
⊢ Limits.PreservesFiniteColimits (localizedModuleFunctor S)

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.Algebra.Category.ModuleCat.Localization
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this :
  Limits.PreservesFiniteLimits (localizedModuleFunctor S) ∧ Limits.PreservesFiniteColimits (localizedModuleFunctor S)
⊢ Limits.PreservesFiniteColimits (localizedModuleFunctor S)

Tactic:
exact this.2

Premises used: And.right
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat R
m : (↑M : Type u)
⊢ Eq (α :=
    (↑((extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type u) →ₗ[S] (↑x2 : Type u)) (CC := carrier) (Y :=
            (extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M))
            ((extendScalars f).map (Iso.inv (λ_ M))) :
          (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj (𝟙_ (ModuleCat R) ⊗ M)) : Type u))
        (1 ⊗ₜ[R] m) :
      (↑((extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) M)) :
        Type u))
    (1 ⊗ₜ[R] (1 ⊗ₜ[R] m) : S ⊗[R] ((↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u) ⊗[R] (↑M : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : ModuleCat R
m : (↑M : Type u)
⊢ Eq (α :=
    (↑((extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type u) →ₗ[S] (↑x2 : Type u)) (CC := carrier) (Y :=
            (extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R))))
            ((extendScalars f).map (Iso.inv (ρ_ M))) :
          (a : (↑((extendScalars f).obj M) : Type u)) → (↑((extendScalars f).obj (M ⊗ 𝟙_ (ModuleCat R))) : Type u))
        (1 ⊗ₜ[R] m) :
      (↑((extendScalars f).obj (tensorObj (𝒞 := moduleCategory R) M ((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)))) :
        Type u))
    (1 ⊗ₜ[R] (m ⊗ₜ[R] 1) : S ⊗[R] ((↑M : Type u) ⊗[R] (↑((𝟙_ (ModuleCat R)) (𝒞 := moduleCategory R)) : Type u)))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := Quiver.Hom (V := ModuleCat S) (of S S) (of S (S ⊗[R] R)))
    (sorry () : Quiver.Hom (V := ModuleCat S) (of S S) (of S (S ⊗[R] R)))
    (↟(↑(LinearEquiv.symm (AlgebraTensorModule.rid R S S)) : S →ₗ[S] S ⊗[R] R) :
      Quiver.Hom (V := ModuleCat S) (of S S) (of S (S ⊗[R] R)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := Quiver.Hom (V := ModuleCat S) (of S (S ⊗[R] R)) (of S S))
    (sorry () : Quiver.Hom (V := ModuleCat S) (of S (S ⊗[R] R)) (of S S))
    (↟(↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : Quiver.Hom (V := ModuleCat S) (of S (S ⊗[R] R)) (of S S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat R
m₁ : (↑M₁ : Type u)
m₂ : (↑M₂ : Type u)
⊢ Eq (α := S ⊗[R] (↑M₁ : Type u) ⊗[S] (S ⊗[R] (↑M₂ : Type u))) (sorry ()) (1 ⊗ₜ[R] m₁ ⊗ₜ[S] (1 ⊗ₜ[R] m₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat.{u_1, u} R
N : SemimoduleCat.{u_2, u} R
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))))
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (TensorProduct.{u, u_1, u_2} R (↑M : Type u_1) (↑N : Type u_2)))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat.{u_1, u} R
N : SemimoduleCat.{u_2, u} R
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)))))
⊢ 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:
apply TensorProduct.ext

Premises used: TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
Goal:
R : Type u
inst : CommSemiring R
M : SemimoduleCat.{u_1, u} R
N : SemimoduleCat.{u_2, u} R
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₂
hf : Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂) = Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))
⊢ tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₂
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₂)))
⊢ Hom.hom (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂) = Hom.hom (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂))

Tactic:
apply TensorProduct.ext

Premises used: TensorProduct.ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₂
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₃
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₃))
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₃
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)))
⊢ 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:
apply TensorProduct.ext_threefold

Premises used: TensorProduct.ext_threefold
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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₃
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:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
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
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)))
⊢ 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))

Tactic:
ext : 1