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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
⊢ { toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ } B ↔
    A ≤ B

Tactic:
dsimp
    constructor
    · intro h
      apply_fun (map e.inv).obj at h
      · simpa only [← map_comp, e.hom_inv_id, map_id] using h
      · apply Functor.monotone
    · intro h
      apply_fun (map e.hom).obj at h
      · exact h
      · apply Functor.monotone

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ kernel.ι f ≫ f = 0 ≫ f

Tactic:
kernel.condition,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ 0 = 0 ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op

Tactic:
rw [← opCoproductIsoProduct'_inv_comp_inj hc hf]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.inj j).op = (c.ι.app { as := j }).op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
⊢ L.lanUnit.app F₁ ≫ L.whiskerLeft (((L.lan.obj F₁).homEquivOfIsLeftKanExtension (L.lanUnit.app F₁) G).symm (f ≫ α)) =
    L.lanUnit.app F₁ ≫
      L.whiskerLeft (L.lan.map f ≫ ((L.lan.obj F₂).homEquivOfIsLeftKanExtension (L.lanUnit.app F₂) G).symm α)

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ (L.lanUnit.app F₁ ≫
          L.whiskerLeft (((L.lan.obj F₁).homEquivOfIsLeftKanExtension (L.lanUnit.app F₁) G).symm (f ≫ α))).app
      X =
    (L.lanUnit.app F₁ ≫
          L.whiskerLeft (L.lan.map f ≫ ((L.lan.obj F₂).homEquivOfIsLeftKanExtension (L.lanUnit.app F₂) G).symm α)).app
      X
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
⊢ StructuredArrow.hom E ≫
      ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ } =
    StructuredArrow.hom G

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
X : C
⊢ (StructuredArrow.hom E ≫
          ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ }).app
      X =
    (StructuredArrow.hom G).app X
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : D ⥤ H
G : C ⥤ H
β : F₁ ⟶ F₂
f : F₂ ⟶ L.ran.obj G
⊢ ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₁).symm.symm (β ≫ f) =
    ((whiskeringLeft C D H).obj L).map β ≫
      ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₂).symm.symm f

Tactic:
by
        dsimp [homEquivOfIsRightKanExtension]
        rw [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
⊢ L.whiskerLeft (((L.ran.obj G₂).homEquivOfIsRightKanExtension (L.ranCounit.app G₂) F).symm (β ≫ f)) ≫
      L.ranCounit.app G₂ =
    L.whiskerLeft (((L.ran.obj G₁).homEquivOfIsRightKanExtension (L.ranCounit.app G₁) F).symm β ≫ L.ran.map f) ≫
      L.ranCounit.app G₂

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F : D ⥤ H
G₁ G₂ : C ⥤ H
β : ((whiskeringLeft C D H).obj L).obj F ⟶ G₁
f : G₁ ⟶ G₂
X : C
⊢ (L.whiskerLeft (((L.ran.obj G₂).homEquivOfIsRightKanExtension (L.ranCounit.app G₂) F).symm (β ≫ f)) ≫
          L.ranCounit.app G₂).app
      X =
    (L.whiskerLeft (((L.ran.obj G₁).homEquivOfIsRightKanExtension (L.ranCounit.app G₁) F).symm β ≫ L.ran.map f) ≫
          L.ranCounit.app G₂).app
      X
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
⊢ ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.hom G

Tactic:
ext X

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
X : C
⊢ (((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
          CostructuredArrow.hom E).app
      X =
    (CostructuredArrow.hom G).app X
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasLimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringLeft C E D).obj F).mapCone c)

Tactic:
apply evaluationJointlyReflectsLimits
      intro Y
      change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
      exact isLimitOfPreserves _ hc

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasColimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cocone K
hc : IsColimit c
Y : C
⊢ IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)

Tactic:
exact isColimitOfPreserves _ hc

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringRight C D E).obj F).mapCone c)

Tactic:
apply evaluationJointlyReflectsLimits _ (fun k => ?_)

Goal state after:
C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C E).obj k).mapCone (((whiskeringRight C D E).obj F).mapCone c))
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cocone K
hc : IsColimit c
k : C
⊢ IsColimit (((evaluation C D).obj k ⋙ F).mapCocone c)

Tactic:
exact isColimitOfPreserves _ hc

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
letI (y : (L ⋙ L').LeftExtension F₀) :
      Unique ((precomp₂ L' α).obj b ⟶ y) := by
    let u : L'.LeftExtension F₁ :=
      mk y.right <|
        hα.desc <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom
    refine
      ⟨⟨StructuredArrow.homMk (hb.desc u) <| by
          ext x
          have hb_fac_app := congr_app (hb.fac u) (L.obj x)
          have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]⟩, fun a => ?_⟩
    dsimp
    ext1
    apply hb.hom_ext
    apply hα.hom_ext
    ext t
    dsimp
    have a_w_t := congr_app a.w t
    have hb_fac_app := congr_app (hb.fac u) (L.obj t)
    have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t
    dsimp at hb_fac_app hα_fac_app
    simp only [whiskeringLeft_obj_obj, comp_obj,
      precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app,
      precomp₂_obj_hom_app, whiskerLeft_app, assoc] at a_w_t
    simp [← a_w_t, hb_fac_app, u, hα_fac_app]
  apply IsInitial.ofUnique

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
⊢ (fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ })
      ((fun f ↦
          { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
            naturality := ⋯ })
        f) =
    f

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ ((fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ })
          ((fun f ↦
              { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
                naturality := ⋯ })
            f)).app
      X =
    f.app X
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteLimits C
inst✝¹ : HasCountableCoproducts C
inst✝ : HasExactColimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C

Tactic:
exact fun _ ↦ inferInstance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
⊢ P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
⊢ P.inverseImage (proj S T) X ↔ ObjectProperty.ofObj (fun f ↦ mk f.snd) X
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
⊢ P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ P.inverseImage (proj S T) X ↔ ObjectProperty.ofObj (fun f ↦ mk f.snd) X
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYonedaEquiv.symm ((hom (P.map ↑f.unop)) (unop x₂).snd) = uliftYonedaEquiv.symm (unop x₁).snd

Tactic:
f.unop.2

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYonedaEquiv.symm (unop x₁).snd = uliftYonedaEquiv.symm (unop x₁).snd
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (coconeOfRepresentable P).pt.obj X
this :
  (functorToRepresentables P).map
        (CategoryOfElements.homMk (P.elementsMk X x) (P.elementsMk Y ((hom (P.map f)) x)) f ⋯).op ≫
      s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((coconeOfRepresentable P).pt.map f ≫ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y x))))).toFun x =
    (hom ((↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x)))) ≫ s.pt.map f)).toFun x

Tactic:
dsimp at this x ⊢

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ lift s ≫ t.π.app zero ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one

Tactic:
reassoc_of% fac,

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
t : Trident f
lift : (s : Trident f) → s.pt ⟶ t.pt
fac : ∀ (s : Trident f), lift s ≫ t.ι = s.ι
uniq : ∀ (s : Trident f) (m : s.pt ⟶ t.pt), (∀ (j : WalkingParallelFamily J), m ≫ t.π.app j = s.π.app j) → m = lift s
s : Cone (parallelFamily f)
j : WalkingParallelFamily J
⊢ ι s ≫ (parallelFamily f).map (line (Classical.arbitrary J)) = s.π.app one
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
· have := h X
    refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)
    simpa using hh j.as

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ (ConcreteCategory.hom (f.app { as := j })) (g j) =
    (ConcreteCategory.hom ((getLimitCone Y).cone.π.app { as := j }))
      ((limit.lift Y ((Cone.postcompose f).obj (Pi.cone X))).hom'
        ((limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
              { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
                π :=
                  Discrete.natTrans fun j ↦
                    AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) }).hom'
          g))

Tactic:
change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
g : (i : J) → ↑(X.obj { as := i })
j : J
⊢ (ConcreteCategory.hom (f.app { as := j })) (g j) =
    (ConcreteCategory.hom
        (limit.lift (Discrete.functor fun j ↦ X.obj { as := j })
            { pt := AddCommGrpCat.of ((j : J) → ↑(X.obj { as := j })),
              π :=
                Discrete.natTrans fun j ↦
                  AddCommGrpCat.ofHom (Pi.evalAddMonoidHom (fun j ↦ ↑(X.obj { as := j })) j.as) } ≫
          limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)) ≫ limit.π Y { as := j }))
      g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ObjectProperty.pair G H = ObjectProperty.ofObj fun j ↦ WalkingPair.casesOn j G H

Tactic:
ext X

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ ObjectProperty.pair G H X ↔ ObjectProperty.ofObj (fun j ↦ WalkingPair.casesOn j G H) X
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

Tactic:
rintro (rfl | rfl)

Goal state after:
case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ ∃ i, WalkingPair.rec G H i = H
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ObjectProperty.pair G H = ObjectProperty.ofObj fun j ↦ WalkingPair.casesOn j G H

Tactic:
ext X

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ ObjectProperty.pair G H X ↔ ObjectProperty.ofObj (fun j ↦ WalkingPair.casesOn j G H) X
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

Tactic:
rintro (rfl | rfl)

Goal state after:
case e'_2.mp.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = G

case e'_2.mp.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ ∃ i, WalkingPair.rec G H i = H
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case snd
G H : AddGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddGrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddGrpCat.{u}) G H) (p, q)

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
by
  rw [← add_assoc, h, h.int_even_mul_periodic]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
rw [← addLeftEmbedding_eq_addRightEmbedding]
  apply disjoint_range_addLeftEmbedding

Goal state after: