mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).map f ≫ ↟(limitπLinearMap F x✝) =
    ↟(limitπLinearMap F x✝¹) ≫ F.map f

Tactic:
ext

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).map f ≫
          ↟(limitπLinearMap F x✝¹)))
      x✝ =
    (Hom.hom (↟(limitπLinearMap F x✝²) ≫ F.map f)) x✝
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).map f ≫ ofHom (limitπAlgHom F x✝) =
    ofHom (limitπAlgHom F x✝¹) ≫ F.map f

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).map f ≫
          ofHom (limitπAlgHom F x✝¹)))
      x✝ =
    (Hom.hom (ofHom (limitπAlgHom F x✝²) ≫ F.map f)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
⊢ ↟(f i i ⋯) = 𝟙 (of R (G i))

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
i : ι
x✝ : ↑(of R (G i))
⊢ (Hom.hom (↟(f i i ⋯))) x✝ = (Hom.hom (𝟙 (of R (G i)))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
⊢ ↟(f X✝ Z✝ ⋯) = ↟(f X✝ Y✝ ⋯) ≫ ↟(f Y✝ Z✝ ⋯)

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
X✝ Y✝ Z✝ : ι
hij : X✝ ⟶ Y✝
hjk : Y✝ ⟶ Z✝
x✝ : ↑(of R (G X✝))
⊢ (Hom.hom (↟(f X✝ Z✝ ⋯))) x✝ = (Hom.hom (↟(f X✝ Y✝ ⋯) ≫ ↟(f Y✝ Z✝ ⋯))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
x✝¹ x✝ : ι
hij : x✝¹ ⟶ x✝
⊢ (directLimitDiagram G f).map hij ≫ ↟(DirectLimit.of R ι G f x✝) =
    ↟(DirectLimit.of R ι G f x✝¹) ≫ ((Functor.const ι).obj (of R (Module.DirectLimit G f))).map hij

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
x✝² x✝¹ : ι
hij : x✝² ⟶ x✝¹
x✝ : ↑((directLimitDiagram G f).obj x✝²)
⊢ (Hom.hom ((directLimitDiagram G f).map hij ≫ ↟(DirectLimit.of R ι G f x✝¹))) x✝ =
    (Hom.hom (↟(DirectLimit.of R ι G f x✝²) ≫ ((Functor.const ι).obj (of R (Module.DirectLimit G f))).map hij)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯) = s.ι.app i

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
i : ι
x✝ : ↑((directLimitDiagram G f).obj i)
⊢ (Hom.hom ((directLimitCocone G f).ι.app i ≫ ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯))) x✝ =
    (Hom.hom (s.ι.app i)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
this : s.ι.app = fun i ↦ ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
⊢ m = ↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯)

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
this : s.ι.app = fun i ↦ ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
x✝ : ↑(directLimitCocone G f).pt
⊢ (Hom.hom m) x✝ = (Hom.hom (↟(Module.DirectLimit.lift R ι G f (fun i ↦ Hom.hom (s.ι.app i)) ⋯))) x✝
Module: Mathlib.Algebra.Category.Grp.Limits

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

Tactic:
constructor

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections → HasLimit F
Module: Mathlib.Algebra.Category.Grp.Limits

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

Tactic:
constructor

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections → HasLimit F
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ (ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
        kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯) ≫
      equalizer.ι f 0 =
    𝟙 (kernel f) ≫ equalizer.ι f 0

Tactic:
ext

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom
        ((ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
            kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯) ≫
          equalizer.ι f 0))
      x✝ =
    (Hom.hom (𝟙 (kernel f) ≫ equalizer.ι f 0)) x✝
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ (kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype = kernel.ι f

Tactic:
ext

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) ↔ L.essImage X

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) → L.essImage X

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) → R.essImage Y

case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ R.essImage Y → IsIso (h.unit.app Y)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = ((α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ f)) ≫ (α_ X Y Z').inv

Tactic:
← associator_naturality

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ f) ≫ (α_ X Y Z').hom) ≫ (α_ X Y Z').inv
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z = ((α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ f ⊗ₘ 𝟙 Z)) ≫ (α_ X Y' Z).inv

Tactic:
← associator_naturality

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z = (((𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ ε (F.prod' H) ≫ (prod' α β).app (𝟙_ C) = ε (G.prod' K)

Tactic:
ext

Goal state after:
case h₁
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ (ε (F.prod' H) ≫ (prod' α β).app (𝟙_ C)).1 = (ε (G.prod' K)).1

case h₂
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
⊢ (ε (F.prod' H) ≫ (prod' α β).app (𝟙_ C)).2 = (ε (G.prod' K)).2
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y) = ((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y

Tactic:
ext

Goal state after:
case h₁
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ (μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y)).1 = (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).1

case h₂
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 : C ⥤ D
H K : C ⥤ E
α : F ⟶ G
β : H ⟶ K
inst✝⁵ : F.LaxMonoidal
inst✝⁴ : G.LaxMonoidal
inst✝³ : IsMonoidal α
inst✝² : H.LaxMonoidal
inst✝¹ : K.LaxMonoidal
inst✝ : IsMonoidal β
X Y : C
⊢ (μ (F.prod' H) X Y ≫ (prod' α β).app (X ⊗ Y)).2 = (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).2
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ homMk (x✝¹.hom ⊗ₘ x✝.hom) = homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
P : ObjectProperty C
tensorUnit : P (𝟙_ C)
tensorObj : ∀ (X Y : C), P X → P Y → P (X ⊗ Y)
X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (homMk (x✝¹.hom ⊗ₘ x✝.hom)).hom = (homMk (x✝¹.hom ▷ X₂✝.obj) ≫ homMk (Y₁✝.obj ◁ x✝.hom)).hom
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
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).map f ≫ ofHom (limitπRingHom F x✝) =
    ofHom (limitπRingHom F x✝¹) ≫ F.map f

Tactic:
ext

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).map f ≫
          ofHom (limitπRingHom F x✝¹)))
      x✝ =
    (Hom.hom (ofHom (limitπRingHom F x✝²) ≫ F.map f)) x✝
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:
ext

Goal state after:
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✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).map f ≫
          ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝¹)))
      x✝ =
    (Hom.hom (ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝²) ≫ F.map f)) x✝
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:
constructor

Goal state after:
case mp
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)

case mpr
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
⊢ (∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)) → Linear R F
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:
constructor

Goal state after:
case unit
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
⊢ autoParam (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (𝟙_ C) = ε G.toFunctor)
    NatTrans.IsMonoidal.unit._autoParam

case tensor
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
⊢ autoParam
    (∀ (X Y : C),
      μ F.toFunctor X Y ≫ (NatIso.ofComponents e ⋯).hom.app (X ⊗ Y) =
        ((NatIso.ofComponents e ⋯).hom.app X ⊗ₘ (NatIso.ofComponents e ⋯).hom.app Y) ≫ μ G.toFunctor X Y)
    NatTrans.IsMonoidal.tensor._autoParam
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:
ext

Goal state after:
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✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).map f ≫
          ofHom (SemiRingCat.limitπRingHom F' x✝¹)))
      x✝ =
    (Hom.hom (ofHom (SemiRingCat.limitπRingHom F' x✝²) ≫ F.map f)) x✝