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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (β_ X Y).hom ≫ i.hom.app (Y ⊗ X)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F G : C ⥤ D
i : F ≅ G
inst✝² : F.LaxBraided
inst✝¹ : G.LaxMonoidal
inst✝ : NatTrans.IsMonoidal i.hom
X Y : C
this : ∀ (X Y : C), μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (X ⊗ Y)) ≫ G.map (β_ X Y).hom =
    (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (β_ X Y).hom ≫ i.hom.app (Y ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : BraidedCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : C ⥤ D
X Y : C
inst✝ : F.Braided
⊢ F.map (β_ X Y).hom = F.map (β_ X Y).hom

Tactic:
]

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

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
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.toAdjunction.comp e'.toAdjunction).IsMonoidal

Tactic:
]

Goal state after:
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
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.toAdjunction.comp e'.toAdjunction).IsMonoidal
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)

Tactic:
]

Goal state after:
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (X ⊗ Y) ▷ G.obj Z ≫
          (i.inv.app (X ⊗ Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ i.hom.app (X ⊗ Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z) ≫ i.hom.app (X ⊗ Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case e_a
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      (F.obj X ⊗ F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫ LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
]

Goal state after:
case e_a
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      (F.obj X ⊗ F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫ LaxMonoidal.μ F (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case e_a
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      (i.inv.app X ⊗ₘ i.inv.app Y ⊗ₘ 𝟙 (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
]

Goal state after:
case e_a
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      (i.inv.app X ⊗ₘ i.inv.app Y ⊗ₘ 𝟙 (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    ((𝟙 (𝟙_ D) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X))) ≫
      LaxMonoidal.μ F (𝟙_ C) X ≫ F.map (λ_ X).hom ≫ i.hom.app X

Tactic:
]

Goal state after:
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (λ_ (G.obj X)).hom =
    ((𝟙 (𝟙_ D) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X))) ≫
      LaxMonoidal.μ F (𝟙_ C) X ≫ F.map (λ_ X).hom ≫ i.hom.app X
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j +
      (F.obj j).smul s ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } +
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ }

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j +
      (F.obj j).smul s ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } +
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ }
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    ((i.inv.app X ⊗ₘ 𝟙 (𝟙_ D)) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F)) ≫
      LaxMonoidal.μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom ≫ i.hom.app X

Tactic:
]

Goal state after:
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
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X : C
⊢ (ρ_ (G.obj X)).hom =
    ((i.inv.app X ⊗ₘ 𝟙 (𝟙_ D)) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F)) ≫
      LaxMonoidal.μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom ≫ i.hom.app X
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
j : J
r : R
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (coconePointSMul F) r =
    (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
j : J
r : R
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (coconePointSMul F) r =
    (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝ ∈
    ↑(DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝ ∈
    ↑(DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
i j : J
f : i ⟶ j
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i = colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (c.ι.app w✝³ ≫ ((Functor.const J).obj c.pt).map w✝¹)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
a✝ : Π₀ (j : J), ↑(F.obj j)
w✝³ w✝² : J
w✝¹ : w✝³ ⟶ w✝²
w✝ : ↑(F.obj w✝³)
eq : a✝ = DFinsupp.single w✝² ((ConcreteCategory.hom (F.map w✝¹)) w✝) - DFinsupp.single w✝³ w✝
⊢ (ConcreteCategory.hom (c.ι.app w✝³ ≫ ((Functor.const J).obj c.pt).map w✝¹)) w✝ - (Hom.hom (c.ι.app w✝³)) w✝ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimitCocone F).pt.smul r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimitCocone F).pt.smul r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (coconePointSMul F) r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
r : R
j : J
⊢ ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (coconePointSMul F) r ≫
        colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ (forget₂ (ModuleCat R) AddCommGrpCat).map m =
    ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s).ι.app j
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom ((colimitCocone F).ι.app j ≫ m))

Tactic:
]

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ AddCommGrpCat.ofHom ↑(Hom.hom m) =
    AddCommGrpCat.ofHom ↑(Hom.hom ((colimitCocone F).ι.app j ≫ m))
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    Relations F

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    Relations F
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ ((Quot.ι (F ⋙ uliftFunctor) j').comp AddEquiv.ulift.symm.toAddMonoidHom) ((ConcreteCategory.hom (F.map u)) a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ ((Quot.ι (F ⋙ uliftFunctor) j').comp AddEquiv.ulift.symm.toAddMonoidHom) ((ConcreteCategory.hom (F.map u)) a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.ulift.symm a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ (Quot.ι (F ⋙ uliftFunctor) j) (AddEquiv.ulift.symm a) -
      ((Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom) a =
    0
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
⊢ ?m.79 x = (AddMonoidHom.id (Quot F)) x

pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
⊢ Quot F →+ Quot F

pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ ((quotUliftToQuot F).comp (quotToQuotUlift F)) ((Quot.ι F j) a) = ?m.79 ((Quot.ι F j) a)

Tactic:
]

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x : Quot F
j : J
a : ↑(F.obj j)
⊢ ((quotUliftToQuot F).comp (quotToQuotUlift F)) ((Quot.ι F j) a) = (AddMonoidHom.id (Quot F)) ((Quot.ι F j) a)