mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
X : C
a : limit (F.op ⋙ yoneda.obj X)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ (ConcreteCategory.hom (limit.π (F.op ⋙ yoneda.obj X) (op x✝))) a =
    (ConcreteCategory.hom (limit.π (F.op ⋙ yoneda.obj X) (op x✝¹))) a ≫ ((const J).obj X).map f

Tactic:
by simpa using (limit.w_apply (F.op ⋙ yoneda.obj X) f.op a)

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✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this✝¹ : (Cone.functoriality K F).map f = i.inv
this✝ : IsIso ((Cone.functoriality K F).map f)
this : IsIso f
⊢ IsLimit d

Tactic:
exact IsLimit.ofIsoLimit hd' (asIso f).symm

Goal state after:
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
F : J ⥤ K ⥤ C
j : J
k : K
⊢ (limitObjIsoLimitCompEvaluation F k).inv ≫ (limit.π F j).app k = limit.π (F ⋙ (evaluation K C).obj k) j

Tactic:
dsimp [limitObjIsoLimitCompEvaluation]
  rw [Iso.inv_comp_eq]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
P : Cᵒᵖ ⥤ Type w
τ : shrinkYoneda.{w, v, u}.obj X ⟶ P
⊢ (fun x ↦
        {
          app := fun Y ↦
            ↾fun f ↦ (ConcreteCategory.hom (P.map (Quiver.Hom.op ((equivShrink ((yoneda.obj X).obj Y)).symm f)))) x,
          naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) ((equivShrink ((yoneda.obj X).obj (op X))) (𝟙 X))) τ) =
    τ

Tactic:
ext Y f
    obtain ⟨f, rfl⟩ := (equivShrink _).surjective f
    simpa [shrinkYoneda] using ((τ.naturality_apply f.op) (equivShrink _ (𝟙 X))).symm

Goal state after:
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 : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))

Tactic:
haveI := H X

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 : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))
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 : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesColimit G (F ⋙ (evaluation K C).obj k)
c : Cocone G
hc : IsColimit c
X : K
⊢ IsColimit (((evaluation K C).obj X).mapCocone (F.mapCocone c))

Tactic:
haveI := H X

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 : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesColimit G (F ⋙ (evaluation K C).obj k)
c : Cocone G
hc : IsColimit c
X : K
this : PreservesColimit G (F ⋙ (evaluation K C).obj X)
⊢ IsColimit (((evaluation K C).obj X).mapCocone (F.mapCocone c))
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ (c : Cone (F ⋙ forget MonCat)) → (t : IsLimit c) → LiftsToLimit F (forget MonCat) c t

Tactic:
intro c

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
⊢ (t : IsLimit c) → LiftsToLimit F (forget MonCat) c t
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (ConcreteCategory.hom
          (((forget MonCat).mapCone
                  { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
                    π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).π.app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso.hom ≫
            c.π.app x✝¹)).toFun
      x✝

Tactic:
simp [Types.isLimitEquivSections]

Goal state after:
case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (limitπMonoidHom F x✝¹) x✝ =
    (ConcreteCategory.hom (c.π.app x✝¹)) ((ConcreteCategory.hom (t.lift (Types.coneOfSection ⋯))) PUnit.unit)
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✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ f = g

Tactic:
apply Mono.right_cancellation (f := h.unit.app Y)
    apply (h.homEquiv X (L.obj Y)).symm.injective
    simpa using hfg

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ CreatesLimit F (forget CommGrpCat)

Tactic:
by
  set e : forget₂ CommGrpCat.{u} GrpCat.{u} ⋙ forget GrpCat.{u} ≅ forget CommGrpCat.{u} := .refl _
  exact createsLimitOfNatIso e

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), X ◁ Y ◁ biproduct.ι f j ≫ g = X ◁ Y ◁ biproduct.ι f j ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (α_ _ _ _).hom).mp
  ext
  simp [w]

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

Tactic:
← cancel_epi (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom,

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.Monoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
      F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z) ≫ 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj X) = (εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom) ≫ (λ_ (F.obj X)).inv

Tactic:
oplax_left_unitality

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
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (𝟙_ D ⊗ F.obj X) =
    (εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom) ≫
      F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ 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
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✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)

Tactic:
suffices F.obj (G.obj X) ◁ F.map (G.map g) ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]

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✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : W.multiplicativeClosure' f
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' (f ≫ g)

Tactic:
induction hf with

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W f✝

Tactic:
induction hf with

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W' f✝

Tactic:
induction hf with

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x y : C
f : x ⟶ y
hf : W.multiplicativeClosure' f
⊢ W.multiplicativeClosure f

Tactic:
induction hf with

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
f : X✝ ⟶ Y✝
hf : W.multiplicativeClosure.strictMap F f
⊢ (W.strictMap F).multiplicativeClosure f

Tactic:
induction hf with

Goal state after:
case map
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ (W.strictMap F).multiplicativeClosure (F.map f✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case map
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ (W.strictMap F).multiplicativeClosure (F.map f✝)

Tactic:
induction hf with

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
⊢ adj.IsMonoidal

Tactic:
by
  let := adj.leftAdjointOplaxMonoidal
  refine ⟨?_, fun X Y ↦ ?_⟩
  · simp [homEquiv_counit, leftAdjointOplaxMonoidal_η]
  · simp [homEquiv_counit, ← μ_natural, leftAdjointOplaxMonoidal_δ]

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
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.single j a) =
    0

Tactic:
map_sub,

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)
⊢ (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
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 : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
⊢ (Hom.hom (hc.desc (toCocone F f))).comp (desc F c) = f

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
j : J
x : ↑(F.obj j)
⊢ ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) ((ι F j) x) = f ((ι F j) x)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrpCat
inst✝ : Small.{w, max u w} (Quot F)
⊢ desc F (colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

Tactic:
refine Quot.addMonoidHom_ext F (fun j x ↦ ?_)

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : DecidableEq J
F : J ⥤ AddCommGrpCat
inst✝ : Small.{w, max u w} (Quot F)
j : J
x : ↑(F.obj j)
⊢ (desc F (colimitCocone F)) ((ι F j) x) = Shrink.addEquiv.symm.toAddMonoidHom ((ι F j) 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
inst✝ : F.LaxBraided
W X Y Z : C
⊢ tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ▷ (F.obj X ⊗ F.obj Z) ≫ F.obj (W ⊗ Y) ◁ μ F X Z) ≫ μ F (W ⊗ Y) (X ⊗ Z) =
    (μ F W X ⊗ₘ μ F Y Z) ≫ μ F (W ⊗ X) (Y ⊗ Z) ≫ F.map (tensorμ W X Y Z)

Tactic:
simp only [tensorμ, Category.assoc]

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
F : C ⥤ D
inst✝ : F.LaxBraided
W X Y Z : C
⊢ (α_ (F.obj W) (F.obj X) (F.obj Y ⊗ F.obj Z)).hom ≫
      F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫
        F.obj W ◁ (β_ (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          F.obj W ◁ (α_ (F.obj Y) (F.obj X) (F.obj Z)).hom ≫
            (α_ (F.obj W) (F.obj Y) (F.obj X ⊗ F.obj Z)).inv ≫
              μ F W Y ▷ (F.obj X ⊗ F.obj Z) ≫ F.obj (W ⊗ Y) ◁ μ F X Z ≫ μ F (W ⊗ Y) (X ⊗ Z) =
    (μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (W ⊗ X) (Y ⊗ Z) ≫
        F.map
          ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ W ◁ (β_ X Y).hom ▷ Z ≫ W ◁ (α_ Y X Z).hom ≫ (α_ W Y (X ⊗ Z)).inv)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ x ∈ (ι R).range, x ∈ (Algebra.linearMap R (TensorAlgebra R M)).range → x = 0

Tactic:
rintro _ ⟨x, hx⟩ ⟨r, rfl⟩

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : (ι R) x = (Algebra.linearMap R (TensorAlgebra R M)) r
⊢ (Algebra.linearMap R (TensorAlgebra R M)) r = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> x.snd <• x.fst ^ i.succ) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> x.snd <• x.fst ^ x_1 <• x.fst) (List.range (n✝ + 1))).sum

Tactic:
simp_rw [← smul_comm (_ : R) (_ : Rᵐᵒᵖ), smul_smul, pow_succ]

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• (x.fst ^ i * x.fst))) (List.range (n✝ + 1))).sum =
    (x.fst ^ n✝ * x.fst) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n✝ + 1))).sum
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a

Tactic:
simpa [← repr.eq, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a)

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Bialgebra R A
inst✝ : IsCocomm R A
x✝ : A
⊢ ((TensorProduct.comm R A A).toBialgHom.comp (comulBialgHom R A)) x✝ = (comulBialgHom R A) x✝

Tactic:
exact comm_comul _ _

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (b ⊔ aᶜ) = f b ⊔ (f a)ᶜ

Tactic:
map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : BooleanAlgebra α
inst✝¹ : BooleanAlgebra β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f b ⊔ f aᶜ = f b ⊔ (f a)ᶜ
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a \ f b ⊔ f b \ f a

Tactic:
map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a \ b) ⊔ f (b \ a) = f a \ f b ⊔ f b \ f a
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ η.unop = (ρ_ (unop A.X)).inv

Tactic:
← unop_whiskerLeft,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (A.X ◁ η).unop = (ρ_ (unop A.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ unop A.X ◁ μ.unop = μ.unop ≫ (μ ▷ A.X).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
← unop_whiskerLeft,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ (A.X ◁ μ).unop = μ.unop ≫ (μ ▷ A.X).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ¬x ∣ a

Tactic:
rintro ⟨d, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ False
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
obtain ⟨⟨a, ⟨-, n, rfl⟩⟩, h⟩ := IsLocalization.surj (Submonoid.powers x) z

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).1
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a