mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ F.map ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    F.map ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (𝟭 C) ≫ adj.unit.app (𝟙_ C) = ε (F ⋙ G)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
X✝ Y✝ : D
x✝ : X✝ ⟶ Y✝
⊢ ∀ (X' : D), F.map x✝ ▷ F.obj X' ≫ (fData.μIso Y✝ X').hom = (fData.μIso X✝ X').hom ≫ F.map (x✝ ▷ X')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ μ (𝟭 C) X Y ≫ adj.unit.app (X ⊗ Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ (F ⋙ G) X Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
X✝ Y✝ x✝ : D
⊢ ∀ (f : X✝ ⟶ Y✝), F.obj x✝ ◁ F.map f ≫ (fData.μIso x✝ Y✝).hom = (fData.μIso x✝ X✝).hom ≫ F.map (x✝ ◁ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
⊢ ε (G ⋙ F) ≫ adj.counit.app (𝟙_ D) = ε (𝟭 D)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝² x✝¹ x✝ : D
⊢ (fData.μIso x✝² x✝¹).hom ▷ F.obj x✝ ≫ (fData.μIso (x✝² ⊗ x✝¹) x✝).hom ≫ F.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (F.obj x✝²) (F.obj x✝¹) (F.obj x✝)).hom ≫ F.obj x✝² ◁ (fData.μIso x✝¹ x✝).hom ≫ (fData.μIso x✝² (x✝¹ ⊗ x✝)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝ : D
⊢ (λ_ (F.obj x✝)).hom = fData.εIso.hom ▷ F.obj x✝ ≫ (fData.μIso (𝟙_ D) x✝).hom ≫ F.map (λ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
x✝ : D
⊢ (ρ_ (F.obj x✝)).hom = F.obj x✝ ◁ fData.εIso.hom ≫ (fData.μIso x✝ (𝟙_ D)).hom ≫ F.map (ρ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
⊢ F.CoreMonoidal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
    e.inverse.map (X ◁ f) =
      (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₁)).inv ≫
        e.inverse.obj X ◁ e.inverse.map f ≫ (e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y₂)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
    e.inverse.map (f ▷ Y) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj Y)).inv ≫
        e.inverse.map f ▷ e.inverse.obj Y ≫ (e.unitIso.app (e.inverse.obj X₂ ⊗ e.inverse.obj Y)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    e.inverse.map (f ⊗ₘ g) =
      (e.unitIso.app (e.inverse.obj X₁ ⊗ e.inverse.obj X₂)).inv ≫
        (e.inverse.map f ⊗ₘ e.inverse.map g) ≫ (e.unitIso.app (e.inverse.obj Y₁ ⊗ e.inverse.obj Y₂)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ μ (G ⋙ F) X Y ≫ adj.counit.app (X ⊗ Y) = (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) X Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X Y Z : D),
    e.inverse.map (α_ X Y Z).hom =
      (((e.unitIso.app (e.inverse.obj (X ⊗ Y) ⊗ e.inverse.obj Z)).symm ≪≫
            ((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ᵢ Iso.refl (e.inverse.obj Z))) ≪≫
          α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ e.unitIso.app (e.inverse.obj Y ⊗ e.inverse.obj Z)) ≪≫
              e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (Y ⊗ Z))).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit (limitCone F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (λ_ X).hom =
      (((e.unitIso.app (e.inverse.obj (𝟙_ D) ⊗ e.inverse.obj X)).symm ≪≫
            ((e.unitIso.app (𝟙_ C)).symm ⊗ᵢ Iso.refl (e.inverse.obj X))) ≪≫
          λ_ (e.inverse.obj X)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit ((forget₂ SemiRingCat AddCommMonCat).mapCone (limitCone F))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
this : MonoidalCategoryStruct D := transportStruct e
⊢ ∀ (X : D),
    e.inverse.map (ρ_ X).hom =
      (((e.unitIso.app (e.inverse.obj X ⊗ e.inverse.obj (𝟙_ D))).symm ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ (e.unitIso.app (𝟙_ C)).symm)) ≪≫
          ρ_ (e.inverse.obj X)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommSemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommSemiRingCat).sections
x✝¹ : (forget₂ CommSemiRingCat SemiRingCat).ReflectsIsomorphisms :=
  reflectsIsomorphisms_forget₂ CommSemiRingCat SemiRingCat
x✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommSemiRingCat SemiRingCat) ⋙ forget SemiRingCat).sections :=
  instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier._proof_1 F
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget CommSemiRingCat)).pt,
    π :=
      { app := fun j ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCat SemiRingCat) j),
        naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ CommSemiRingCat SemiRingCat)
t : IsLimit c'
⊢ IsLimit c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ (equivalenceTransported e).inverse.Monoidal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ (equivalenceTransported e).symm.IsMonoidal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).map f ≫
      ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝) =
    ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝¹) ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget RingCat)).pt,
    π := { app := fun x ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x), naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ RingCat SemiRingCat)
t : IsLimit c'
⊢ (forget₂ RingCat SemiRingCat).mapCone c ≅ c'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
c : Cone F :=
  { pt := of (Types.Small.limitCone (F ⋙ forget RingCat)).pt,
    π := { app := fun x ↦ ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x), naturality := ⋯ } }
c' : Cone (F ⋙ forget₂ RingCat SemiRingCat)
t : IsLimit c'
⊢ IsLimit ((forget₂ RingCat SemiRingCat).mapCone c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
⊢ Injective toRatLinearMap

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
h : ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)
X Y : C
f : X ⟶ Y
r : R
⊢ r • f = (r • 𝟙 X) ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
⊢ IsLimit ((forget₂ RingCat AddCommGrpCat).mapCone (limitCone F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
α β : F ⟶ G
h : α.hom = β.hom
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
⊢ Linear R F ↔ ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝ : Linear R F
X Y : C
r : Rˣ
f : X ⟶ Y
⊢ F.map (r • f) = r • F.map f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommRingCat).sections
this✝¹ : (forget₂ CommRingCat RingCat).ReflectsIsomorphisms
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat).sections
F' : J ⥤ SemiRingCat := F ⋙ forget₂ CommRingCat RingCat ⋙ forget₂ RingCat SemiRingCat
this : Small.{u, max u v} ↑(F' ⋙ forget SemiRingCat).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).map f ≫
      ofHom (SemiRingCat.limitπRingHom F' x✝) =
    ofHom (SemiRingCat.limitπRingHom F' x✝¹) ≫ F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
E : Type u₃
inst✝⁶ : Category.{v₃, u₃} E
inst✝⁵ : MonoidalCategory E
E' : Type u₄
inst✝⁴ : Category.{v₄, u₄} E'
inst✝³ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝² : F₁.LaxMonoidal
inst✝¹ : F₂.LaxMonoidal
inst✝ : F₃.LaxMonoidal
F G : LaxMonoidalFunctor C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit : ε F.toFunctor ≫ (e (𝟙_ C)).hom = ε G.toFunctor
tensor : ∀ (X Y : C), μ F.toFunctor X Y ≫ (e (X ⊗ Y)).hom = ((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y
⊢ NatTrans.IsMonoidal (NatIso.ofComponents e ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F G : C ⥤ D
inst✝ : F.Monoidal
e : F ≅ G
⊢ NatTrans.IsMonoidal e.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
⊢ f = (F.objObjPreimageIso X).inv ≫ F.map f' ≫ (F.objObjPreimageIso Y).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommRingCat).sections
⊢ IsLimit ((forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
⊢ ∃ X' Y' eX eY f', f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
⊢ Linear R G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F G : C ⥤ D
e : F ≅ G
inst✝ : Linear R F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
r : R
⊢ G.map (r • f) = r • G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F G : C ⥤ D
e : F ≅ G
inst✝ : Linear R F
⊢ Linear R G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{v_1, u_2} C
inst✝⁵ : Category.{v_2, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Linear R C
inst✝¹ : Linear R D
F : C ⥤ D
e : C ≌ D
inst✝ : Functor.Linear R e.functor
X✝ Y✝ : D
r : X✝ ⟶ Y✝
f : R
⊢ e.inverse.map (f • r) = f • e.inverse.map r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
⊢ f ⊗ₘ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : Y ⟶ Z
⊢ 0 ⊗ₘ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
g h : Y ⟶ Z
⊢ f ⊗ₘ (g + h) = f ⊗ₘ g + f ⊗ₘ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f g : W ⟶ X
h : Y ⟶ Z
⊢ (f + g) ⊗ₘ h = f ⊗ₘ h + g ⊗ₘ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D}, X ◁ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D}, 0 ▷ X = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D} (f g : Y ⟶ Z), X ◁ (f + g) = X ◁ f + X ◁ g

Tactic:
by

Goal state after: