mathlib-initiative/mathlib-tactics huggingface dataset:
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
hc : IsLimit t
X X' : C
f : X ⟶ X'
g : X' ⟶ t.pt
j : J
⊢ (hc.homEquiv (f ≫ g)).app j = ((ConcreteCategory.hom (F.cones.map f.op)) (hc.homEquiv g)).app j

Tactic:
simp

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ (ConcreteCategory.hom ((yoneda.obj X).map f)) (𝟙 X) = (ConcreteCategory.hom ((yoneda.map f.unop).app (op Y))) (𝟙 Y)

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (homOfCocone h s) = s

Tactic:
by
  rw [← coconeOfHom_homOfCocone h s]
  conv_lhs => simp only [homOfCocone_coconeOfHom]
  apply (coconeOfHom_fac _ _).symm

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 Y : C
f : X ⟶ Y
Z : D
x✝ g : Y ⟶ G.obj Z
⊢ ((⇑(adj.homEquiv X Z) ∘ fun g ↦ F.map f ≫ g) ∘ ⇑(adj.homEquiv Y Z).symm) g = f ≫ g

Tactic:
simp

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 Y : D
g : X ⟶ Y
Z : C
x✝ : Z ⟶ G.obj X
⊢ x✝ ≫ G.map g = ((⇑(adj.homEquiv Z Y) ∘ fun f ↦ f ≫ g) ∘ ⇑(adj.homEquiv Z X).symm) x✝

Tactic:
simp

Goal state after:
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
hc : IsColimit t
X X' : C
f : X ⟶ X'
g : t.pt ⟶ X
j : J
⊢ (hc.homEquiv (g ≫ f)).app j = ((ConcreteCategory.hom (F.cocones.map f)) (hc.homEquiv g)).app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z : C} (f : Z ⟶ Y), ε.symm (ε f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z : C} (f : Z ⟶ Y'), ε (ε.symm f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z : C} (f : X ⟶ Z), ε.symm (ε f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X X' : C
e : F.CorepresentableBy X
e' : F.CorepresentableBy X'
ε : {Y : C} → (X ⟶ Y) ≃ (X' ⟶ Y) := fun {Y} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z : C} (f : X' ⟶ Z), ε (ε.symm f) = f

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x ≤ y
heq : x = y
⊢ homOfLE h ≫ homOfLE ⋯ = 𝟙 x ∧ homOfLE ⋯ ≫ homOfLE h = 𝟙 y

Tactic:
simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : Preorder X
inst✝ : Preorder Y
e : X ≃o Y
x✝ : X
⊢ (𝟭 X).obj x✝ = (⋯.functor ⋙ ⋯.functor).obj x✝

Tactic:
simp

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : Preorder X
inst✝ : Preorder Y
e : X ≃o Y
x✝ : Y
⊢ (⋯.functor ⋙ ⋯.functor).obj x✝ = (𝟭 Y).obj x✝

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i) =
    inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom) ≫ (α_ (f ≫ g) h i).inv =
    (f ◁ (α_ g h i).inv ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) ≫ (α_ (f ≫ g) h i).inv

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ ((α_ f g (h ≫ i)).inv ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv) ≫ (α_ f g h).inv ▷ i =
    ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) ≫ (α_ f g h).inv ▷ i

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h = (α_ f g h).hom ≫ η ▷ (g ≫ h) ≫ (α_ f' g h).inv

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h ≫ (α_ f g' h).inv = (α_ f g h).inv ≫ (f ◁ η) ▷ h

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ f ◁ η ▷ h = (α_ f g h).inv ≫ (f ◁ η) ▷ h ≫ (α_ f g' h).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ g ◁ η

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η ≫ (α_ f g h').inv = (α_ f g h).inv ≫ (f ≫ g) ◁ η

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η : h ⟶ h'
⊢ f ◁ g ◁ η = (α_ f g h).inv ≫ (f ≫ g) ◁ η ≫ (α_ f g h').hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (λ_ g).inv = (λ_ f).inv ≫ 𝟙 a ◁ η

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η ≫ (ρ_ g).inv = (ρ_ f).inv ≫ η ▷ 𝟙 b

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy X
⊢ ((fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝)).homEquiv (𝟙 X) = x✝.homEquiv (𝟙 X)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (ρ_ f).inv ≫ η ▷ 𝟙 b ≫ (ρ_ g).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy Y
⊢ ((fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝)).homEquiv (𝟙 Y) = x✝.homEquiv (𝟙 Y)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ 𝟙 a ◁ η = 𝟙 a ◁ θ ↔ η = θ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy X
⊢ ((fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝)).homEquiv (𝟙 X) = x✝.homEquiv (𝟙 X)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy Y
⊢ ((fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝)).homEquiv (𝟙 Y) = x✝.homEquiv (𝟙 Y)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv ((λ_ f).inv ▷ g) = inv ((λ_ (f ≫ g)).inv ≫ (α_ (𝟙 a) f g).inv)

Tactic:
simp

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₁
ξ : F.obj (op X)
⊢ (fun η ↦ (ConcreteCategory.hom (η.app (op X))) (𝟙 X))
      ((fun ξ ↦ { app := fun x ↦ ↾fun f ↦ (ConcreteCategory.hom (F.map (Quiver.Hom.op f))) ξ, naturality := ⋯ }) ξ) =
    ξ

Tactic:
simp

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
⊢ (ConcreteCategory.hom ((yoneda.map f).app (op X))) (𝟙 X) = f

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ inv (f ◁ (ρ_ g).inv) = inv ((ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom)

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (λ_ (f ≫ g)).inv = (λ_ f).inv ▷ g ≫ (α_ (𝟙 a) f g).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom

Tactic:
simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Tactic:
simp

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:
simp

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₁)
u : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F
⊢ uliftYonedaEquiv.symm (uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop ≫ u)) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm (uliftYonedaEquiv u)

Tactic:
simp

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
⊢ (ConcreteCategory.hom (f.app (op (unop X)))) (uliftYonedaEquiv (uliftYonedaEquiv.symm x)) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm ((ConcreteCategory.hom (f.app (op (unop X)))) x))

Tactic:
simp

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:
simp

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
F : C ⥤ D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ((fromSkeletonToSkeletonIso (F.obj ((skeletonEquivalence C).functor.obj ((toSkeletonFunctor C).obj X✝)))).hom ≫
        F.map ((skeletonEquivalence C).functor.map ((toSkeletonFunctor C).map f)) ≫
          (fromSkeletonToSkeletonIso
              (F.obj ((skeletonEquivalence C).functor.obj ((toSkeletonFunctor C).obj Y✝)))).inv) ≫
      ((toSkeletonFunctor D).mapIso (F.mapIso (fromSkeletonToSkeletonIso Y✝))).hom.hom =
    ((toSkeletonFunctor D).mapIso (F.mapIso (fromSkeletonToSkeletonIso X✝))).hom.hom ≫
      ((F ⋙ toSkeletonFunctor D).map f).hom

Tactic:
simp

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₁
ξ : F.obj X
⊢ (fun η ↦ (ConcreteCategory.hom (η.app X)) (𝟙 X))
      ((fun ξ ↦ { app := fun x ↦ ↾fun x_1 ↦ (ConcreteCategory.hom (F.map x_1)) ξ, naturality := ⋯ }) ξ) =
    ξ

Tactic:
simp

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 ((coyoneda.obj (op X)).map g ≫ f.app Y)) (𝟙 X) = (ConcreteCategory.hom (f.app Y)) (g ≫ 𝟙 Y)

Tactic:
simp

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
⊢ (ConcreteCategory.hom ((coyoneda.map f.op).app Y)) (𝟙 Y) = f

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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.56 + 1} ⥤ C
X Y : Discrete PUnit.{?u.56 + 1}
f : X ⟶ Y
A B : PUnit.{?u.56 + 1}
g : PLift ({ as := A }.as = { as := B }.as)
⊢ (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).map { down := g } ≫
      match { as := B } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) =
    (match { as := A } with
      | { as := PUnit.unit } =>
        𝟙 (((const (Discrete PUnit.{?u.56 + 1})).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit })) ≫
      F.map { down := g }

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

Goal state after:
B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = F.toFunctor.rightUnitor
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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case h_obj
X : Type u
⊢ ∀ (X_1 : Discrete X),
    (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).obj X_1 = (𝟭 (Discrete X)).obj X_1

Tactic:
simp

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:
simp

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₁)
u : uliftCoyoneda.{w, v₁, u₁}.obj (op X) ⟶ F
⊢ uliftCoyonedaEquiv.symm (uliftCoyonedaEquiv (uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ u)) =
    uliftCoyoneda.{w, v₁, u₁}.map f.op ≫ uliftCoyonedaEquiv.symm (uliftCoyonedaEquiv u)

Tactic:
simp

Goal state after: