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

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y ≫ e.counitInv.app Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
e.counitIso.hom_inv_id_app

Goal state after:
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (𝟙 ((e.inverse ⋙ e.functor).obj Y))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.hom ≫ NatTrans.op α.inv).app x✝ = (𝟙 G.op).app x✝

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.hom.app (unop x✝)).op ≫ (α.inv.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.op α.inv ≫ NatTrans.op α.hom).app x✝ = (𝟙 F.op).app x✝

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (α.inv.app (unop x✝)).op ≫ (α.hom.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
f : D ≌ E
X : C
⊢ (e.functor ⋙ f.functor).map
        ((e.unitIso ≪≫
                isoWhiskerRight
                    (e.functor.rightUnitor.symm ≪≫
                      e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm)
                    e.inverse ≪≫
                  (e.functor ⋙ f.functor).associator f.inverse e.inverse).hom.app
          X) ≫
      (((f.inverse ⋙ e.inverse).associator e.functor f.functor).symm ≪≫
              isoWhiskerRight
                  (f.inverse.associator e.inverse e.functor ≪≫
                    f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor)
                  f.functor ≪≫
                f.counitIso).hom.app
        ((e.functor ⋙ f.functor).obj X) =
    𝟙 ((e.functor ⋙ f.functor).obj X)

Tactic:
dsimp

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
e : C ≌ D
f : D ≌ E
X : C
⊢ f.functor.map
        (e.functor.map
          (e.unitIso.hom.app X ≫
            e.inverse.map
                (𝟙 (e.functor.obj X) ≫
                  f.unitIso.hom.app (e.functor.obj X) ≫ 𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
              𝟙 (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
      𝟙 (f.functor.obj (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X)))))) ≫
        f.functor.map
            (𝟙 (e.functor.obj (e.inverse.obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫
              e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X))) ≫
                𝟙 (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫
          f.counitIso.hom.app (f.functor.obj (e.functor.obj X)) =
    𝟙 (f.functor.obj (e.functor.obj X))
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
F : C ⥤ E
X : D
⊢ (((whiskeringLeft D C E).obj e.inverse).map ((ofComponents (fun F ↦ (e.funInvIdAssoc F).symm) ⋯).hom.app F) ≫
          (ofComponents (fun F ↦ e.invFunIdAssoc F) ⋯).hom.app (((whiskeringLeft D C E).obj e.inverse).obj F)).app
      X =
    (𝟙 (((whiskeringLeft D C E).obj e.inverse).obj F)).app X

Tactic:
dsimp

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
e : C ≌ D
F : C ⥤ E
X : D
⊢ (e.funInvIdAssoc F).inv.app (e.inverse.obj X) ≫ (e.invFunIdAssoc (e.inverse ⋙ F)).hom.app X =
    𝟙 (F.obj (e.inverse.obj X))
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (C ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop Y).opUnopIso.op.hom = (unop X).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f

Tactic:
intro F G f
        dsimp [opUnopIso]
        rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map ((e.unitIso ≪≫ e.functor.isoWhiskerLeft iso).hom.app X) ≫
      (isoWhiskerRight iso.symm e.functor ≪≫ e.counitIso).hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)

Tactic:
dsimp

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
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫
      e.functor.map (iso.inv.app (e.functor.obj X)) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map η ≫ (unop G).rightOpLeftOpIso.op.hom =
    (unop F).rightOpLeftOpIso.op.hom ≫
      ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯, map_comp := ⋯ }).map
        η

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η ≫ (unop G).rightOpLeftOpIso.hom.op =
    (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ ((fun i ↦ Groupoid.inv (f i)) ≫ f) i = 𝟙 Y✝ i

Tactic:
apply Groupoid.inv_comp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ P f'

Tactic:
by
  rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
  rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]

Goal state after:
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
y : F.obj j
⊢ (e j') ((⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) ((e j) y)) =
    (e j') ((⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) ((e j) y))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
y : F.obj j
⊢ (e j') ((e j').symm ((ConcreteCategory.hom (G.map f)) ((e j) y))) =
    (e j') ((ConcreteCategory.hom (F.map f)) ((e j).symm ((e j) y)))
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫
      { left := F₁.obj Y.left, right := F₂.obj Y.right, hom := α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right }.hom ≫
      R'.map (F₂.map φ.right)

Tactic:
dsimp

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫ α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right =
    (α.app X.left ≫ F.map X.hom ≫ β.app X.right) ≫ R'.map (F₂.map φ.right)
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right

Tactic:
dsimp

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    ((map α β).obj
          { left := F₁.objPreimage X.left, right := F₂.objPreimage X.right,
            hom :=
              F.preimage
                ((inv α).app (F₁.objPreimage X.left) ≫
                  L'.map (F₁.objObjPreimageIso X.left).hom ≫
                    X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app (F₂.objPreimage X.right)) }).hom ≫
      R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
dsimp

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    (α.app (F₁.objPreimage X.left) ≫
        F.map
            (F.preimage
              ((inv α).app (F₁.objPreimage X.left) ≫
                L'.map (F₁.objObjPreimageIso X.left).hom ≫
                  X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ (inv β).app (F₂.objPreimage X.right))) ≫
          β.app (F₂.objPreimage X.right)) ≫
      R'.map (F₂.objObjPreimageIso X.right).hom
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X : Comma (F ⋙ L) R
⊢ L.map (Iso.refl ((preLeft F L R).obj X).left).hom ≫
      ((map (F ⋙ L).rightUnitor.inv (R.rightUnitor.hom ≫ R.leftUnitor.inv)).obj X).hom =
    ((preLeft F L R).obj X).hom ≫ R.map (Iso.refl ((preLeft F L R).obj X).right).hom

Tactic:
simp -implicitDefEqProofs

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

Goal state before:
pp: X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget RingCat).map f)
    let ff : X →+* Y := f.hom
    let e : X ≃+* Y := { ff, i.toEquiv with }
    exact e.toRingCatIso.isIso_hom

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g ↦ F.map g ≫ adj.counit.app Y) ((fun f ↦ adj.unit.app X ≫ G.map f) f) = f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ F.map (adj.unit.app X ≫ G.map f) ≫ adj.counit.app Y = f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ ((const J).obj W).map f ≫ ↑p j' = ↑p j ≫ F.map f

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ 𝟙 W ≫ ↑p j' = ↑p j ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑p j' = ↑p j ≫ ((const J).obj W).map f

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
h : IsColimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ↑p j' = ↑p j ≫ 𝟙 W
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (e.homEquiv.trans (e'.app (op X)).toEquiv) (f ≫ g) =
    (ConcreteCategory.hom (F'.map f.op)) ((e.homEquiv.trans (e'.app (op X')).toEquiv) g)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
e' : F ≅ F'
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app (op X))) (e.homEquiv (f ≫ g)) =
    (ConcreteCategory.hom (F'.map f.op)) ((ConcreteCategory.hom (e'.hom.app (op X'))) (e.homEquiv g))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (e.homEquiv.trans (e'.app Y').toEquiv) (f ≫ g) =
    (ConcreteCategory.hom (F'.map g)) ((e.homEquiv.trans (e'.app Y).toEquiv) f)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F F' : C ⥤ Type v
X : C
e : F.CorepresentableBy X
e' : F ≅ F'
Y Y' : C
g : Y ⟶ Y'
f : X ⟶ Y
⊢ (ConcreteCategory.hom (e'.hom.app Y')) (e.homEquiv (f ≫ g)) =
    (ConcreteCategory.hom (F'.map g)) ((ConcreteCategory.hom (e'.hom.app Y)) (e.homEquiv f))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
g : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom ((yoneda.obj Y).map f ≫ r.homEquiv.toIso.hom)).toFun g =
    (ConcreteCategory.hom (r.homEquiv.toIso.hom ≫ F.map f)).toFun g

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
Y : C
r : F.RepresentableBy Y
X X' : Cᵒᵖ
f : X ⟶ X'
g : (yoneda.obj Y).obj X
⊢ r.homEquiv (f.unop ≫ g) = (ConcreteCategory.hom (F.map f)) (r.homEquiv g)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
r : F.CorepresentableBy X✝
X X' : C
f : X ⟶ X'
g : (coyoneda.obj (op X✝)).obj X
⊢ (ConcreteCategory.hom ((coyoneda.obj (op X✝)).map f ≫ r.homEquiv.toIso.hom)).toFun g =
    (ConcreteCategory.hom (r.homEquiv.toIso.hom ≫ F.map f)).toFun g

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
X✝ : C
r : F.CorepresentableBy X✝
X X' : C
f : X ⟶ X'
g : (coyoneda.obj (op X✝)).obj X
⊢ r.homEquiv (g ≫ f) = (ConcreteCategory.hom (F.map f)) (r.homEquiv g)
Module: Mathlib.CategoryTheory.Skeletal

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
⊢ (fromSkeleton C).Faithful

Tactic:
by
  apply InducedCategory.faithful

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ (f.hom.op ≫ X.op.π.app j).unop = (Y.op.π.app j).unop

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ X.ι.app (unop j) ≫ f.hom = Y.ι.app (unop j)
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ ((unop X).unop.ι.app j ≫ f.unop.hom.unop).op = ((unop Y).unop.ι.app j).op

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ f.unop.hom ≫ (unop X).π.app (op j) = (unop Y).π.app (op j)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f =
    hl.lift { pt := c.pt, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } } ≫
      hi.hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = hl.lift { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } } ≫ hi.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f =
    hi.inv ≫
      hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ ((Functor.const J).obj (F.obj X)).map k ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ ((Functor.const J).obj (F.obj X)).map f ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ 𝟙 (F.obj X) ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ ((Functor.const J).obj (F.obj X)).map k

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ ((Functor.const J).obj (F.obj X)).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ 𝟙 (F.obj X)