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

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 G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : G.obj X ⟶ Y
⊢ ((adj.ofNatIsoLeft iso).homEquiv X Y) f = (adj.homEquiv X Y) (iso.hom.app X ≫ f)

Tactic:
by

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 G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
Y : D
f : X ⟶ H.obj Y
⊢ ((adj.ofNatIsoLeft iso).homEquiv X Y).symm f = iso.inv.app X ≫ (adj.homEquiv X Y).symm f

Tactic:
by

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 H : D ⥤ C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ((adj.ofNatIsoRight iso).homEquiv X Y) f = (adj.homEquiv X Y) f ≫ iso.hom.app Y

Tactic:
by

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 H : D ⥤ C
adj : F ⊣ G
iso : G ≅ H
X : C
Y : D
f : X ⟶ H.obj Y
⊢ ((adj.ofNatIsoRight iso).homEquiv X Y).symm f = (adj.homEquiv X Y).symm (f ≫ iso.inv.app Y)

Tactic:
by

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
H : D ⥤ E
I : E ⥤ D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : C
⊢ (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X))

Tactic:
by

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
H : D ⥤ E
I : E ⥤ D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : E
⊢ (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X

Tactic:
by

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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
by

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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
by

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✝ : Cone F✝
D : Type u₄
inst✝ : Category.{v₄, u₄} D
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (G.mapCone c)

Tactic:
by

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.cones.RepresentableBy X
s : Cone F
⊢ coneOfHom h (homOfCone h s) = s

Tactic:
by

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.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ homOfCone h (coneOfHom h f) = f

Tactic:
by

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

Tactic:
by

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.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ coneOfHom h f = (limitCone h).extend f

Tactic:
by

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.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (homOfCone h s) = s

Tactic:
by

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

Tactic:
by

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

Tactic:
by

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_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 ⟶ G_obj Y
⊢ F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g)

Tactic:
by

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 : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
j : J
⊢ homOfCone h s ≫ (limitCone h).π.app j = s.π.app j

Tactic:
by

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 : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ m = homOfCone h s

Tactic:
by

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

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
h : IsColimit t
W : C
ι : F ⟶ (const J).obj W
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (fun j ↦ ι.app j) j' = (fun j ↦ ι.app j) j

Tactic:
by

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'') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g') =
    (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫
      (e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g')

Tactic:
by

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

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
⊢ coconeOfHom h (homOfCocone h s) = s

Tactic:
by

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
Y : C
f : X ⟶ Y
⊢ homOfCocone h (coconeOfHom h f) = f

Tactic:
by

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
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = (colimitCocone h).extend 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 : op X ⟶ op Y
⊢ (ConcreteCategory.hom ((yoneda.obj X).map f)) (𝟙 X) = (ConcreteCategory.hom ((yoneda.map f.unop).app (op Y))) (𝟙 Y)

Tactic:
by

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
⊢ ∀ {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:
by

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

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

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
⊢ ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map 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 : coyoneda.obj X ⟶ coyoneda.obj Y),
    coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop X))) (𝟙 (unop X)))) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h s = s.ι.app j

Tactic:
by

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
⊢ (Function.Bijective fun g ↦ F.map f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g

Tactic:
by

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

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

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
⊢ (Function.Bijective fun f ↦ f ≫ G.map g) ↔ Function.Bijective fun f ↦ f ≫ g

Tactic:
by

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

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ G.IsLeftAdjoint

Tactic:
by

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsRightAdjoint ↔ G.IsRightAdjoint

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ F.IsLeftAdjoint

Tactic:
by

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
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
⊢ m = homOfCocone h s

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by

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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsRightAdjoint ↔ F.IsRightAdjoint

Tactic:
by

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

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

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

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 Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ Y), ε (f ≫ g) = f ≫ ε g

Tactic:
by

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

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

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : AsSmall C
h : X = Y
⊢ (eqToHom h).down = eqToHom ⋯

Tactic:
by

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

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

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ x ≤ y

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : Preorder X
x y : X
h : x = y
⊢ IsIso (homOfLE ⋯)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderTop X
x : X
a : x ⟶ ⊤
⊢ a = homOfLE ⋯

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : Preorder X
inst✝ : OrderBot X
x : X
a : ⊥ ⟶ x
⊢ a = homOfLE ⋯

Tactic:
by

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

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

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

Goal state before:
pp: X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ IsIso f ↔ a = b

Tactic:
by

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 h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
by

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

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

Tactic:
by

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 Z' : C} (f : X' ⟶ Z) (g : Z ⟶ Z'), ε.symm (f ≫ g) = ε.symm f ≫ g

Tactic:
by

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 h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
by

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

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

Tactic:
by

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 k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.hom ≫ f ◁ g ◁ η.inv = 𝟙 (f ≫ g ≫ h)

Tactic:
by

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

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

Tactic:
by

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 k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom = 𝟙 (f ≫ g ≫ k)

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
η : f = g
h : b ⟶ c
⊢ eqToHom η ▷ h = eqToHom ⋯

Tactic:
by

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

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

Tactic:
by

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 h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.hom ▷ k ≫ f ◁ η.inv ▷ k = 𝟙 (f ≫ g ≫ k)

Tactic:
by

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 h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.inv ▷ k ≫ f ◁ η.hom ▷ k = 𝟙 (f ≫ h ≫ k)

Tactic:
by

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 h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η

Tactic:
by

Goal state after: