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

Tactic:
;

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.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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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
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
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = (e X Y) (F.map f ≫ (e X' Y).symm g)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8
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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ { pt := s.pt, ι := (colimitCocone h).ι ≫ (const J).map m } = s

Tactic:
;

Goal state after:
case e_8
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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ { pt := s.pt, ι := (colimitCocone h).ι ≫ (const J).map m } = s
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8.mk
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
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ { pt := { pt := pt✝, ι := ι✝ }.pt, ι := (colimitCocone h).ι ≫ (const J).map m } = { pt := pt✝, ι := ι✝ }

Tactic:
;

Goal state after:
case e_8.mk
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
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ { pt := { pt := pt✝, ι := ι✝ }.pt, ι := (colimitCocone h).ι ≫ (const J).map m } = { pt := pt✝, ι := ι✝ }
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8.mk
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
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
j : J
⊢ ((colimitCocone h).ι ≫ (const J).map m).app j = ι✝.app j

Tactic:
;

Goal state after:
case e_8.mk
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
X : C
h : F.cocones.CorepresentableBy X
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
m : (colimitCocone h).pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt✝, ι := ι✝ }.ι.app j
j : J
⊢ ((colimitCocone h).ι ≫ (const J).map m).app j = ι✝.app j
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : x✝¹ ⟶ Y
⊢ e x✝ = e' x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e g)
e' : {X : C} → (X ⟶ Y) ≃ F.obj (op X)
he' : ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) (e' g)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 Y) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 Y)
this :
  ∀ {X : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : x✝¹ ⟶ Y
⊢ e x✝ = e' x✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : X ⟶ x✝¹
⊢ e x✝ = e' x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e f)
e' : {Y : C} → (X ⟶ Y) ≃ F.obj Y
he' : ∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y), e' (f ≫ g) = (ConcreteCategory.hom (F.map g)) (e' f)
h : { homEquiv := e, homEquiv_comp := he }.homEquiv (𝟙 X) = { homEquiv := e', homEquiv_comp := he' }.homEquiv (𝟙 X)
this :
  ∀ {Y : C} (f : X ⟶ Y),
    { homEquiv := e, homEquiv_comp := he }.homEquiv f = { homEquiv := e', homEquiv_comp := he' }.homEquiv f
x✝¹ : C
x✝ : X ⟶ x✝¹
⊢ e x✝ = e' x✝
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:
;

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

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

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

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

Goal state after:
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 := ⋯ }) ξ) =
    ξ
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C : Cat
⊢ ↾Quot.map (𝟙 C).toFunctor.obj ⋯ = 𝟙 (Quotient (isIsomorphicSetoid ↑C))

Tactic:
ext x
    apply @Quot.recOn _ _ _ x
    all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.IsomorphismClasses

Goal state before:
pp: C D E : Cat
f : C ⟶ D
g : D ⟶ E
⊢ ↾Quot.map (f ≫ g).toFunctor.obj ⋯ = ↾Quot.map f.toFunctor.obj ⋯ ≫ ↾Quot.map g.toFunctor.obj ⋯

Tactic:
ext x
    apply @Quot.recOn _ _ _ x
    all_goals cat_disch

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

Goal state after:
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))
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:
rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩

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
x✝¹ x✝ : ThinSkeleton C
f₁ down✝ : x✝¹ ≤ x✝
⊢ { down := { down := f₁ } } = { down := { down := down✝ } }
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:
;

Goal state after:
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 := ⋯ }) ξ) =
    ξ
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ 𝟙 C ≫ { toFunctor := toFunctor✝ } = { toFunctor := toFunctor✝ }

Tactic:
;

Goal state after:
case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ 𝟙 C ≫ { toFunctor := toFunctor✝ } = { toFunctor := toFunctor✝ }
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ { toFunctor := toFunctor✝ } ≫ 𝟙 D = { toFunctor := toFunctor✝ }

Tactic:
;

Goal state after:
case ofFunctor
C D : Cat
toFunctor✝ : ↑C ⥤ ↑D
⊢ { toFunctor := toFunctor✝ } ≫ 𝟙 D = { toFunctor := toFunctor✝ }
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:
;

Goal state after:
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
Module: Mathlib.CategoryTheory.Category.Cat

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

Tactic:
;

Goal state after:
case refl
C D : Cat
F : C ⟶ D
⊢ (eqToHom ⋯).toNatTrans = eqToHom ⋯
Module: Mathlib.CategoryTheory.Category.Cat

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

Tactic:
;

Goal state after:
B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = F.toFunctor.rightUnitor
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
s : ↑F.sections
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
x : ((const C).obj X).obj x✝²
⊢ (ConcreteCategory.hom (((const C).obj X).map x✝ ≫ ↾fun x ↦ ↑s x✝¹)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ ↑s x✝²) ≫ F.map x✝)).toFun x

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
s : ↑F.sections
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
x : ((const C).obj X).obj x✝²
⊢ (ConcreteCategory.hom (((const C).obj X).map x✝ ≫ ↾fun x ↦ ↑s x✝¹)).toFun x =
    (ConcreteCategory.hom ((↾fun x ↦ ↑s x✝²) ≫ F.map x✝)).toFun x
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).obj X✝
⊢ (ConcreteCategory.hom
          ((F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftYoneda.{v₂, v₁, u₁}.obj X).map f)).toFun
      x✝

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X : C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝ : (F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).obj X✝
⊢ (ConcreteCategory.hom
          ((F.op ⋙ uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftYoneda.{v₂, v₁, u₁}.obj X).map f)).toFun
      x✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫
                (hF.homNatIso Y✝).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Cᵒᵖ
x✝ : ((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F ⋙ uliftYoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op).map f ≫
                (hF.homNatIso Y✝).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso X✝).hom ≫ uliftYoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).obj X✝
⊢ (ConcreteCategory.hom
          ((F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f)).toFun
      x✝

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : (F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).obj X✝
⊢ (ConcreteCategory.hom
          ((F ⋙ uliftCoyoneda.{v₁, v₂, u₂}.obj (op (F.obj X))).map f ≫
            (Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans (hF.homEquiv.symm.trans Equiv.ulift.symm)).toIso.hom ≫
            (uliftCoyoneda.{v₂, v₁, u₁}.obj (op X)).map f)).toFun
      x✝
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝¹ : C
x✝ : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
                (hF.homNatIso' (unop Y✝)).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝

Tactic:
;

Goal state after:
C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : F.FullyFaithful
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
x✝¹ : C
x✝ : ((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).obj X✝).obj x✝¹
⊢ (ConcreteCategory.hom
          (((F.op ⋙ uliftCoyoneda.{v₁, v₂, u₂} ⋙ (whiskeringLeft C D (Type (max v₁ v₂))).obj F).map f ≫
                (hF.homNatIso' (unop Y✝)).hom).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (((hF.homNatIso' (unop X✝)).hom ≫ uliftCoyoneda.{v₂, v₁, u₁}.map f).app x✝¹)).toFun x✝
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv X Z) (F.map f ≫ g) = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h

Tactic:
adj.homEquiv_naturality_left,

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 Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : f ≫ (adj.homEquiv Y Z) g = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : f ≫ (adj.homEquiv Y Z) g = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h

Tactic:
adj.homEquiv_naturality_left,

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 Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : f ≫ (adj.homEquiv Y Z) g = f ≫ (adj.homEquiv Y Z) h
⊢ g = h
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift

Tactic:
rw [← sq.left_adjoint_hasLift_iff adj]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ (x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }),
    { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
⊢ ∀ (x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }),
    { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }
⊢ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
Y : C
x : IsLimit { pt := Y, π := { app := fun X ↦ ⋯.elim, naturality := ⋯ } }
⊢ { lift := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ ∀ (x : IsColimit { pt := X, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }),
    { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty.{1} ⥤ C
X : C
⊢ ∀ (x : IsColimit { pt := X, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }),
    { desc := fun s ↦ default, fac := ⋯, uniq := ⋯ } = x