mathlib-initiative/mathlib-tactics huggingface dataset:
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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (G.map (δ F x✝¹ X✝) ≫ δ G (F.obj x✝¹) (F.obj X✝)) ≫ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ =
    (F ⋙ G).map (x✝¹ ◁ x✝) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)

Tactic:
dsimp

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (G.map (δ F x✝¹ X✝) ≫ δ G (F.obj x✝¹) (F.obj X✝)) ≫ G.obj (F.obj x✝¹) ◁ G.map (F.map x✝) =
    G.map (F.map (x✝¹ ◁ x✝)) ≫ G.map (δ F x✝¹ Y✝) ≫ δ G (F.obj x✝¹) (F.obj Y✝)
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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ (F ⋙ G).obj Z ≫
        (α_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)).hom =
    (F ⋙ G).map (α_ X Y Z).hom ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        (F ⋙ G).obj X ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
dsimp

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫
        (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ (((α_ (unop W) (unop X) (unop Y)).symm.op.hom.unop ▷ unop Z).op ≫
        (α_ (unop W) (unop (op (unop X ⊗ unop Y))) (unop Z)).symm.op.hom ≫
          (unop W ◁ (α_ (unop X) (unop Y) (unop Z)).symm.op.hom.unop).op).unop =
    ((α_ (unop (op (unop W ⊗ unop X))) (unop Y) (unop Z)).symm.op.hom ≫
        (α_ (unop W) (unop X) (unop (op (unop Y ⊗ unop Z)))).symm.op.hom).unop

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ (unop W ◁ (α_ (unop X) (unop Y) (unop Z)).inv ≫ (α_ (unop W) (unop X ⊗ unop Y) (unop Z)).inv) ≫
      (α_ (unop W) (unop X) (unop Y)).inv ▷ unop Z =
    (α_ (unop W) (unop X) (unop Y ⊗ unop Z)).inv ≫ (α_ (unop W ⊗ unop X) (unop Y) (unop Z)).inv
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ ((α_ (unop X) (unop (op (𝟙_ C))) (unop Y)).symm.op.hom ≫ (unop X ◁ (λ_ (unop Y)).symm.op.hom.unop).op).unop =
    ((ρ_ (unop X)).symm.op.hom.unop ▷ unop Y).op.unop

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ unop X ◁ (λ_ (unop Y)).inv ≫ (α_ (unop X) (𝟙_ C) (unop Y)).inv = (ρ_ (unop X)).inv ▷ unop Y
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ ((Z.unmop ◁ (α_ Y.unmop X.unmop W.unmop).symm.mop.hom.unmop).mop ≫
        (α_ Z.unmop { unmop := Y.unmop ⊗ X.unmop }.unmop W.unmop).symm.mop.hom ≫
          ((α_ Z.unmop Y.unmop X.unmop).symm.mop.hom.unmop ▷ W.unmop).mop).unmop =
    ((α_ Z.unmop Y.unmop { unmop := X.unmop ⊗ W.unmop }.unmop).symm.mop.hom ≫
        (α_ { unmop := Z.unmop ⊗ Y.unmop }.unmop X.unmop W.unmop).symm.mop.hom).unmop

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ Z.unmop ◁ (α_ Y.unmop X.unmop W.unmop).inv ≫
      (α_ Z.unmop (Y.unmop ⊗ X.unmop) W.unmop).inv ≫ (α_ Z.unmop Y.unmop X.unmop).inv ▷ W.unmop =
    (α_ Z.unmop Y.unmop (X.unmop ⊗ W.unmop)).inv ≫ (α_ (Z.unmop ⊗ Y.unmop) X.unmop W.unmop).inv
Module: Mathlib.CategoryTheory.Monoidal.Opposite

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ ((α_ Y.unmop { unmop := 𝟙_ C }.unmop X.unmop).symm.mop.hom ≫ ((ρ_ Y.unmop).mop.hom.unmop ▷ X.unmop).mop).unmop =
    (Y.unmop ◁ (λ_ X.unmop).mop.hom.unmop).mop.unmop

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ (α_ Y.unmop (𝟙_ C) X.unmop).inv ≫ (ρ_ Y.unmop).hom ▷ X.unmop = Y.unmop ◁ (λ_ X.unmop).hom
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
j : J
⊢ (m.op ≫ c.π.app j).unop = ((hc.lift (coneOfCoconeLeftOp s)).unop.op ≫ c.π.app j).unop

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac, coneOfCoconeLeftOp_π_app] using! w (op j)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteWidePushouts Cᵒᵖ

Tactic:
by
  refine ⟨fun J _ ↦ ?_⟩
  rw [hasColimitsOfShape_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasPullbacks C
⊢ HasPushouts Cᵒᵖ

Tactic:
by
  have : HasLimitsOfShape WalkingSpanᵒᵖ C :=
    hasLimitsOfShape_of_equivalence walkingSpanOpEquiv.symm
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan f g) G
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        none ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app none

Tactic:
dsimp

Goal state after:
case none
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.left) ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.left)

Tactic:
dsimp

Goal state after:
case some.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.right) ≫
      (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt).hom =
    (PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.right)

Tactic:
dsimp

Goal state after:
case some.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y : Cᵒᵖ
X : C
f : Opposite.unop Y ⟶ Opposite.unop (Opposite.op X)
⊢ identities Cᵒᵖ (Opposite.op f) ↔ identities C (Quiver.Hom.unop (Opposite.op f))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y : Cᵒᵖ
X : C
f : Opposite.unop Y ⟶ Opposite.unop (Opposite.op X)
⊢ identities Cᵒᵖ (Opposite.op f) ↔ identities C f
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ x₁ = x₂

Tactic:
rw [Subtype.ext_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ ↑x₁ = ↑x₂
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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    adj.unit.app (X ⊗ Y) ▷ (F ⋙ G).obj Z ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
dsimp

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    adj.unit.app (X ⊗ Y) ▷ G.obj (F.obj Z) ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
          G.obj (F.obj Z) ≫
        μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝ : HasPushout f g
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op).unop = (pushout.inl f g).op.unop

Tactic:
simp [← pushoutIsoUnopPullback_inl_hom]

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'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ ((F ⋙ G).obj X) Y Z).hom ≫
      (F ⋙ G).obj X ◁ adj.unit.app (Y ⊗ Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
          μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
dsimp

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁ adj.unit.app (Y ⊗ Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
          μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
⊢ μ (F ⋙ G) X Y ≫ (F ⋙ G).map (β_ X Y).hom = (β_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y)).hom ≫ μ (F ⋙ G) Y X

Tactic:
dsimp

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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxBraided
inst✝ : G.LaxBraided
X Y : C
⊢ (μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)) ≫ G.map (F.map (β_ X Y).hom) =
    (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))).hom ≫ μ G (F.obj Y) (F.obj X) ≫ G.map (μ F 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 X Y ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X

Tactic:
rw [← Functor.Braided.braided, δ_μ_assoc]

Goal state after:
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 ≫
      (((Functor.const J).obj (mkOfSMul (coconePointSMul F))).obj j).smul r =
    (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j

Tactic:
dsimp

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 ≫ (mkOfSMul (coconePointSMul F)).smul 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
⊢ Relations F ≤ (DFinsupp.sumAddHom fun x ↦ Hom.hom (c.ι.app x)).ker

Tactic:
dsimp

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ Relations F ≤ (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
⊢ (forget₂ (ModuleCat R) AddCommGrpCat).map (F.map f) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫
      (forget₂ (ModuleCat R) AddCommGrpCat).map (((Functor.const J).obj (mkOfSMul (coconePointSMul F))).map f)

Tactic:
dsimp

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)
i j : J
f : i ⟶ j
⊢ AddCommGrpCat.ofHom ↑(Hom.hom (F.map f)) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) i ≫ AddCommGrpCat.ofHom ↑LinearMap.id
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
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
        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:
dsimp

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
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
        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.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:
dsimp

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
⊢ AddCommGrpCat.ofHom ↑(Hom.hom (s.ι.app j)) ≫ s.pt.smul r =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } ≫
        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)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j'))
        ((ConcreteCategory.hom (F.map f)) x) -
      ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j)) x =
    0

Tactic:
← (QuotientAddGroup.mk' (Relations F)).map_sub,

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)
⊢ (QuotientAddGroup.mk' (Relations F))
      ((DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
        (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x) =
    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
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:
dsimp

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 (s.ι.app 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
j j' : J
u : j ⟶ j'
a : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom)
        (DFinsupp.single j' ((ConcreteCategory.hom (F.map u)) a)) -
      (DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom)
        (DFinsupp.single j a) =
    0

Tactic:
DFinsupp.sumAddHom_single,

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) -
      (DFinsupp.sumAddHom fun j ↦ (Quot.ι (F ⋙ uliftFunctor) j).comp AddEquiv.ulift.symm.toAddMonoidHom)
        (DFinsupp.single j a) =
    0