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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| g ≫ coeqHom g h ≫ rightToMax (coeq f g) (coeq g h)

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))

Tactic:
← Category.assoc,

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| (g ≫ coeqHom g h) ≫ rightToMax (coeq f g) (coeq g h)

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
| coeqHom (coeqHom f g ≫ leftToMax (coeq f g) (coeq g h)) (coeqHom g h ≫ rightToMax (coeq f g) (coeq g h))
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ (hom (t.ι.app i)) xi = (hom (t.ι.app j)) xj ↔ ∃ k f g, (hom (F.map f)) xi = (hom (F.map g)) xj

Tactic:
have : HasColimit F := ⟨_, ht⟩
  refine Iff.trans ?_ (colimit_eq_iff_aux F)
  rw [← (IsColimit.coconePointUniqueUpToIso ht (colimitCoconeIsColimit F)).toEquiv.injective.eq_iff]
  convert! Iff.rfl
  · exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xi).symm
  · exact (congr_hom
      (IsColimit.comp_coconePointUniqueUpToIso_hom ht (colimitCoconeIsColimit F) _) xj).symm

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
rw [CategoryTheory.Functor.map_id]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, 0⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, 0⟩.fst))) ⟨j, x⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 j))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩

Tactic:
rw [CategoryTheory.Functor.map_id]

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨j,
        (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, x⟩.snd *
          (ConcreteCategory.hom (𝟙 ((F ⋙ forget₂ SemiRingCat MonCat).obj ⟨j, x⟩.fst))) ⟨j, 0⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat) ⟨j, 0⟩
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • ∏ i', A ((decomposeFin.symm (i.succ, σ)) i') i' =
    (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i', A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
by
      simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f ≫ (preservesColimitIso G Y✝).hom =
    ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁵ : Category.{w', w} J
F : J ⥤ C
inst✝⁴ : PreservesColimit F G
inst✝³ : HasColimit F
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ((preservesColimitIso G X✝).inv ≫ (colim ⋙ G).map f) ≫ (preservesColimitIso G Y✝).hom =
    ((Functor.whiskeringRight J C D).obj G ⋙ colim).map f
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X ×ₘ 𝟙 Y) = 𝟙 (F.obj (X, Y))

Tactic:
rw [← prod_id]; exact F.map_id ⟨X,Y⟩

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip).map (f₁, f₂) = eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
by
    dsimp
    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

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

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip)).map (f₁, f₂) =
    eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
by
    dsimp
    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ (liftedLimitMapsToOriginal t).inv.hom ≫ (liftedLimitMapsToOriginal t).hom.hom ≫ c.π.app j = c.π.app j

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F : C ⥤ D
inst✝ : CreatesLimit K F
c : Cone (K ⋙ F)
t : IsLimit c
j : J
⊢ ((liftedLimitMapsToOriginal t).inv.hom ≫ (liftedLimitMapsToOriginal t).hom.hom) ≫ c.π.app j = c.π.app j
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ (s.pt.map f ≫ (t Y).lift { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) }) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j

Tactic:
rw [assoc, (t Y).fac _ j]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
c : Cone F
t : (k : K) → IsLimit (((evaluation K C).obj k).mapCone c)
s : Cone F
X Y : K
f : X ⟶ Y
j : J
⊢ s.pt.map f ≫ { pt := s.pt.obj Y, π := whiskerRight s.π ((evaluation K C).obj Y) }.π.app j =
    ((t X).lift { pt := s.pt.obj X, π := whiskerRight s.π ((evaluation K C).obj X) } ≫ c.pt.map f) ≫
      (((evaluation K C).obj Y).mapCone c).π.app j
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f =
    (limitObjIsoLimitCompEvaluation F i).hom ≫
      limMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))) ≫
      (limitObjIsoLimitCompEvaluation F j).inv
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    colimMap (F.whiskerLeft ((evaluation K C).map f))

Tactic:
← Category.assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ ((colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f) ≫ (colimitObjIsoColimitCompEvaluation F j).hom =
    colimMap (F.whiskerLeft ((evaluation K C).map f))
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f) = shrinkCoyonedaObjObjEquiv.symm f.unop

Tactic:
by
  simp [shrinkCoyonedaEquiv, shrinkYoneda, shrinkYonedaObjObjEquiv]

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

Goal state before:
pp: case refine_5
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
s : Cone F
⊢ ∀ (r : R),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
      (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r

Tactic:
· intro r
    simp only [Equiv.algebraMap_def, Equiv.symm_symm]
    apply congrArg
    apply Subtype.ext
    ext j
    exact (s.π.app j).hom.commutes r

Goal state after:
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.Full
inst✝ : L.Faithful
⊢ IsIso (whiskerRight h.counit R)

Tactic:
have := h.right_triangle

Goal state after:
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.Full
inst✝ : L.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)
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.Full
inst✝ : R.Faithful
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
have := h.right_triangle

Goal state after:
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.Full
inst✝ : R.Faithful
this : R.whiskerLeft h.unit ≫ (R.associator L R).inv ≫ whiskerRight h.counit R = R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (R.whiskerLeft h.unit)
Module: Mathlib.CategoryTheory.Monoidal.Category

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

Tactic:
simp [← cancel_epi ((α_ W X Y).hom ▷ Z)]

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

Goal state before:
pp: 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 β
⊢ ε H ≫ ((prod' α β).app (𝟙_ C)).2 = ε K

Tactic:
prod'_app_snd,

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 β
⊢ ε H ≫ β.app (𝟙_ C) = ε K
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom

Tactic:
← Category.assoc,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ (δ F (𝟙_ C) X ≫ η F ▷ F.obj X) ≫ (λ_ (F.obj X)).hom = F.map (λ_ X).hom
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X = F.map (λ_ X).hom ≫ F.map (λ_ X).inv ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj X

Tactic:
← Category.assoc,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F (𝟙_ C) X ≫ η F ▷ F.obj X = (F.map (λ_ X).hom ≫ F.map (λ_ X).inv) ≫ δ F (𝟙_ C) X ≫ η F ▷ F.obj 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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Tactic:
← Category.assoc,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ (δ F X (𝟙_ C) ≫ F.obj X ◁ η F) ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F = F.map (ρ_ X).hom ≫ F.map (ρ_ X).inv ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F

Tactic:
← Category.assoc,

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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F = (F.map (ρ_ X).hom ≫ F.map (ρ_ X).inv) ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
← Category.assoc,

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

Tactic:
← Category.assoc,

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hη)]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    (pullbackIsoOpPushout g₁.op g₂.op).inv ≫
      pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pullbackIsoOpPushout f₁.op f₂.op).hom

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    ((pullbackIsoOpPushout g₁.op g₂.op).inv ≫ pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) ≫
      (pullbackIsoOpPushout f₁.op f₂.op).hom
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 =
    G.obj X ◁ (εIso F ≪≫ i.app (𝟙_ C)).hom ≫
      ((i.symm.app X ⊗ᵢ i.symm.app (𝟙_ C)) ≪≫ μIso F X (𝟙_ C) ≪≫ i.app (X ⊗ 𝟙_ C)).hom ≫ G.map (ρ_ X).hom

Tactic:
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp,
      Iso.hom_inv_id_app, Category.comp_id]
    rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]
    simp

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)
s : Cocone F
r : R
⊢ colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s) ≫
      s.pt.smul r =
    (colimitCocone F).pt.smul r ≫
      colimit.desc (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ((forget₂ (ModuleCat R) AddCommGrpCat).mapCocone s)

Tactic:
apply colimit.hom_ext
    intro j
    dsimp
    rw [colimit.ι_desc_assoc]
    -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
    erw [mkOfSMul_smul]
    dsimp
    simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc,
      Functor.mapCocone_pt, Functor.mapCocone_ι_app, forget₂_map]
    exact smul_naturality (s.ι.app j) r

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
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom) = s.ι.app j

Tactic:
ext x
    dsimp
    conv_lhs => erw [← Quot.ι_desc F c j x]
    rw [← AddEquiv.ofBijective_apply _ h, AddEquiv.symm_apply_apply]
    simp only [Quot.ι_desc, Functor.const_obj_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (L₂.map (G.map (adj₁.unit.app c))) ≫
        R₂.map (α.natTrans.app (R₁.obj (L₁.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)

Tactic:
slice_lhs 2 3 =>
    rw [← R₂.map_comp, ← Functor.comp_map G L₂, α.naturality]

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
c : C
⊢ adj₂.unit.app (G.obj c) ≫
      R₂.map (α.app c ≫ (L₁ ⋙ H).map (adj₁.unit.app c)) ≫ R₂.map (H.map (adj₁.counit.app (L₁.obj c))) =
    adj₂.unit.app (G.obj c) ≫ R₂.map (α.app c)