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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((yoneda.map f).app (op c))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
τ : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op y.down))) x, naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) { down := 𝟙 (unop (op X)) }) τ) =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
x : F.obj (op X)
⊢ (fun τ ↦ (ConcreteCategory.hom (τ.app (op X))) { down := 𝟙 (unop (op X)) })
      ((fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op y.down))) x, naturality := ⋯ })
        x) =
    x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type (max w v₁)
f : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (uliftYonedaEquiv f) = uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map g.unop ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
t : F.obj X
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
⊢ uliftYonedaEquiv (uliftYonedaEquiv.symm x ≫ f) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.app (op (unop X)))) x))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f) = { down := f }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ ∀ {X_1 Y : Cᵒᵖ ⥤ Type (max w v₁)} (f : X_1 ⟶ Y),
    ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj X).map f ≫ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                  (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                    uliftFunctor.{u₁, max v₁ w}).obj
              X).map
          f

Tactic:
by

Goal state after:
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).Full

Tactic:
by

Goal state after:
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

Goal state after:
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
x✝ : C
⊢ { hom := (fromSkeletonToSkeletonIso x✝).hom ≫ 𝟙 x✝ ≫ (fromSkeletonToSkeletonIso x✝).inv } = 𝟙 (toSkeleton x✝)

Tactic:
by

Goal state after:
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
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { hom := (fromSkeletonToSkeletonIso X✝).hom ≫ (x✝¹ ≫ x✝) ≫ (fromSkeletonToSkeletonIso Z✝).inv }.hom =
    ({ hom := (fromSkeletonToSkeletonIso X✝).hom ≫ x✝¹ ≫ (fromSkeletonToSkeletonIso Y✝).inv } ≫
        { hom := (fromSkeletonToSkeletonIso Y✝).hom ≫ x✝ ≫ (fromSkeletonToSkeletonIso Z✝).inv }).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ Skeletal (Skeleton C)

Tactic:
by

Goal state after:
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
⊢ ∀ (a₁ b₁ a₂ b₂ : C), a₁ ≈ a₂ → b₁ ≈ b₂ → Nonempty (a₁ ⟶ b₁) = Nonempty (a₂ ⟶ b₂)

Tactic:
by

Goal state after:
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
⊢ ∀ (a : ThinSkeleton C), Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ a a

Tactic:
refine Quotient.ind fun a => ?_

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
a : C
⊢ Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ ⟦a⟧ ⟦a⟧
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
⊢ ∀ (a : ThinSkeleton C), Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ a a

Tactic:
by

Goal state after:
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
x✝¹ x✝ : ThinSkeleton C
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
              (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                uliftFunctor.{u₁, max v₁ w}).map
          f

Tactic:
by

Goal state after:
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
inst✝ : Quiver.IsThin C
⊢ ∀ (a b : C), ⟦a⟧ ≤ ⟦b⟧ → ⟦b⟧ ≤ ⟦a⟧ → ⟦a⟧ = ⟦b⟧

Tactic:
by

Goal state after:
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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X

Tactic:
by

Goal state after:
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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : coyoneda.obj (op X) ⟶ F
⊢ (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
      ((fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)) η) =
    η

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
⊢ Function.RightInverse (fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ })
    fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F G : C ⥤ Type v₁
α : coyoneda.obj (op X) ⟶ F
β : F ⟶ G
⊢ coyonedaEquiv (α ≫ β) = (ConcreteCategory.hom (β.app X)) (coyonedaEquiv α)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ coyonedaEquiv (coyoneda.map f.op) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (coyonedaEquiv f) = (ConcreteCategory.hom (f.app Y)) g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
t : F.obj X
⊢ coyonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C × (C ⥤ Type v₁)} (f : X ⟶ Y),
    (coyonedaPairing C).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (coyonedaEvaluation C).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ coyonedaEquiv.toIso) ⋯).hom ≫ (evaluation C (Type u₁)).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type v₁} (f : X_1 ⟶ Y),
    ((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type v₁) ⋙
                  (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
              X).map
          f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F : C ⟶ D
⊢ 𝟙 C ≫ F = F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F : C ⟶ D
⊢ F ≫ 𝟙 D = F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: ⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (coyoneda.rightOp ⋙ coyoneda).map f ≫
        (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
        (evaluation C (Type v₁) ⋙
              (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
          f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C : Cat
X : ↑C
⊢ (𝟙 C).toFunctor.obj X = X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C : Cat
X Y : ↑C
f : X ⟶ Y
⊢ (𝟙 C).toFunctor.map f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ E
X : ↑C
⊢ (F ≫ G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ E
X Y : ↑C
f : X ⟶ Y
⊢ (F ≫ G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F : C ⟶ D
X : ↑C
⊢ (𝟙 F).toNatTrans.app X = 𝟙 (F.toFunctor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F G : C ⟶ D
h : F = G
⊢ (eqToHom h).toNatTrans = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D : Cat
F G : C ⟶ D
h : F = G
X : ↑C
⊢ (eqToHom h).toNatTrans.app X = eqToHom ⋯

Tactic:
by

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 : Discrete PUnit.{?u.21 + 1} ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit.{?u.21 + 1}⦄ (f : X ⟶ Y),
    (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).map f ≫
        match Y with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
      (match X with
        | { as := PUnit.unit } =>
          𝟙 (((const (Discrete PUnit.{?u.21 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
        F.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G H : D ⟶ E
η : G ⟶ H
X : ↑C
⊢ (F ◁ η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: C D E : Cat
F G : C ⟶ D
H : D ⟶ E
η : F ⟶ G
X : ↑C
⊢ (η ▷ H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (𝟙 B ≫ F).toFunctor.obj X = F.toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (λ_ F).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ F.toFunctor.obj X = (𝟙 B ≫ F).toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
        coyonedaEquiv.toIso.hom =
      coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (λ_ F).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ c.π.app j ≫ F.map f = c.π.app j'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
F : C ⥤ Type u₁
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    ((yoneda ⋙ (whiskeringLeft C (C ⥤ Type u₁)ᵒᵖ (Type u₁)).obj coyoneda.rightOp).obj F).map f ≫
        coyonedaEquiv.toIso.hom =
      coyonedaEquiv.toIso.hom ≫ ((𝟭 (C ⥤ Type u₁)).obj F).map f

Tactic:
by
    intro X Y f
    ext a
    simp [coyonedaEquiv, ← NatTrans.naturality_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (F ≫ 𝟙 C).toFunctor.obj X = F.toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (ρ_ F).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ F.toFunctor.obj X = (F ≫ 𝟙 C).toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c : Cocone F
j j' : J
f : j' ⟶ j
F' : C → C → Type uF
carrier : C → Type w
instFunLike : (X Y : C) → FunLike (F' X Y) (carrier X) (carrier Y)
inst : ConcreteCategory C F'
x : carrier (F.obj j')
⊢ (ConcreteCategory.hom (c.ι.app j)) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (c.ι.app j')) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C : Cat
F : B ⟶ C
X : ↑B
⊢ (ρ_ F).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ ((F ≫ G) ≫ H).toFunctor.obj X = (F ≫ G ≫ H).toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ (α_ F G H).hom.toNatTrans.app X = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ (F ≫ G ≫ H).toFunctor.obj X = ((F ≫ G) ≫ H).toFunctor.obj X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: B C D E : Cat
F : B ⟶ C
G : C ⟶ D
H : D ⟶ E
X : ↑B
⊢ (α_ F G H).inv.toNatTrans.app X = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ f ≫ x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x ↦ f ≫ x

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩
  intro T
  rw [bijective_iff_isIso_ofHom]
  exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

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✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd }) = 𝟙 (Cone F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x ↦ f ≫ x) ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
exact forall_congr' fun _ ↦ bijective_iff_isIso_ofHom _

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) }) τ) =
    τ

Tactic:
ext Y ⟨x⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F
Y : C
x : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom
          (((fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ })
                ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) }) τ)).app
            Y)).toFun
      { down := x } =
    (ConcreteCategory.hom (τ.app Y)).toFun { down := x }
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) }) τ) =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X : Type u
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).toCatHom = 𝟙 (Cat.of (Discrete X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
x : F.obj (unop X)
⊢ (fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) })
      ((fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ }) x) =
    x

Tactic:
by

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✝ F : J ⥤ C
⊢ ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩) = 𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type (max w v₁)
f : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (uliftCoyonedaEquiv f) = uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map g.op ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g)))).toCatHom =
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f))).toCatHom ≫
      (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))).toCatHom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C ↔ EssentiallySmall.{w, v', u'} D

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: _X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
⊢ _f = _g

Tactic:
by

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✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X✝ Y✝ : Type u
F : typeToCat.obj X✝ ⟶ typeToCat.obj Y✝
⊢ ∀ (X : ↑(typeToCat.obj X✝)),
    (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.obj X = F.toFunctor.obj X

Tactic:
by

Goal state after: