mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
x✝ : ↑R
⊢ ((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝

Tactic:
;

Goal state after:
R S : RingCat
e : R ≅ S
x✝ : ↑R
⊢ ((RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝

Tactic:
;

Goal state after:
R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝

Tactic:
;

Goal state after:
R S : CommSemiRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝

Tactic:
;

Goal state after:
R S : CommRingCat
e : R ≅ S
x✝ : ↑S
⊢ ((CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv)) x✝ = (RingHom.id ↑S) x✝
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝

Tactic:
;

Goal state after:
R S : CommRingCat
e : R ≅ S
x✝ : ↑R
⊢ ((CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom)) x✝ = (RingHom.id ↑R) x✝
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: case mk
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
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit =
    adj'.unit
h' :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit =
    adj'.counit
⊢ { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ } =
    adj'

Tactic:
;

Goal state after:
case mk
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
unit✝ : 𝟭 C ⟶ F ⋙ G
counit✝ : G ⋙ F ⟶ 𝟭 D
left_triangle_components✝ : ∀ (X : C), F.map (unit✝.app X) ≫ counit✝.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components✝ : ∀ (Y : D), unit✝.app (G.obj Y) ≫ G.map (counit✝.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.unit =
    adj'.unit
h' :
  { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
        right_triangle_components := right_triangle_components✝ }.counit =
    adj'.counit
⊢ { unit := unit✝, counit := counit✝, left_triangle_components := left_triangle_components✝,
      right_triangle_components := right_triangle_components✝ } =
    adj'
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
P Q : IsLimit t
⊢ P = Q

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 : Cone F
P Q : IsLimit t
⊢ P = Q
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case 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 : Cone F
Q : IsLimit t
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝, fac := fac✝, uniq := uniq✝ } = Q

Tactic:
;

Goal state after:
case 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 : Cone F
Q : IsLimit t
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝, fac := fac✝, uniq := uniq✝ } = Q
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case mk.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 : Cone F
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝¹, fac := fac✝¹, uniq := uniq✝¹ } = { lift := lift✝, fac := fac✝, uniq := uniq✝ }

Tactic:
;

Goal state after:
case mk.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 : Cone F
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ { lift := lift✝¹, fac := fac✝¹, uniq := uniq✝¹ } = { lift := lift✝, fac := fac✝, uniq := uniq✝ }
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case mk.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 : Cone F
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ lift✝¹ = lift✝

Tactic:
;

Goal state after:
case mk.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 : Cone F
lift✝¹ : (s : Cone F) → s.pt ⟶ t.pt
fac✝¹ : ∀ (s : Cone F) (j : J), lift✝¹ s ≫ t.π.app j = s.π.app j
uniq✝¹ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝¹ s
lift✝ : (s : Cone F) → s.pt ⟶ t.pt
fac✝ : ∀ (s : Cone F) (j : J), lift✝ s ≫ t.π.app j = s.π.app j
uniq✝ : ∀ (s : Cone F) (m : s.pt ⟶ t.pt), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = lift✝ s
⊢ lift✝¹ = lift✝
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
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s
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
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom
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
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s

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
r t : Cone F
P : IsLimit r
i : r ≅ t
s : Cone F
m : s ⟶ t
⊢ m ≫ i.inv = P.liftConeMorphism s
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : C
⊢ (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x✝ =
    (F.leftUnitor.hom ≫ F.rightUnitor.inv).app x✝

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
adj : F ⊣ G
x✝ : C
⊢ (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x✝ =
    (F.leftUnitor.hom ≫ F.rightUnitor.inv).app x✝
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✝ : D
⊢ (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x✝ =
    (G.rightUnitor.hom ≫ G.leftUnitor.inv).app x✝

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
adj : F ⊣ G
x✝ : D
⊢ (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x✝ =
    (G.rightUnitor.hom ≫ G.leftUnitor.inv).app x✝
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
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b ↦ f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b ↦ f' ≫ t.π.app b, naturality := ⋯ } }

Tactic:
;

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ h.lift { pt := W, π := { app := fun b ↦ f ≫ t.π.app b, naturality := ⋯ } } =
    h.lift { pt := W, π := { app := fun b ↦ f' ≫ t.π.app b, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e_8
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b ↦ f ≫ t.π.app b) = fun b ↦ f' ≫ t.π.app b

Tactic:
;

Goal state after:
case e_8
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
f f' : W ⟶ t.pt
w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j
⊢ (fun b ↦ f ≫ t.π.app b) = fun b ↦ f' ≫ t.π.app b
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 : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) 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
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) 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
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ 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
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := ⋯
⊢ ∀ (j : J),
    (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
          P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t)) ≫
        s.π.app j =
      𝟙 s.pt ≫ s.π.app 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✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := ⋯
⊢ ∀ (j : J),
    (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) ≫
          P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t)) ≫
        s.π.app j =
      𝟙 s.pt ≫ s.π.app j
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e'_3
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
π : (const J).obj W ⟶ F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
e_1✝ : (((const J).obj W).obj j✝ ⟶ F.obj j'✝) = (W ⟶ F.obj j'✝)
⊢ ((const J).obj W).map f ≫ π.app j'✝ = (fun j ↦ π.app j) j'✝

Tactic:
;

Goal state after:
case e'_3
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
π : (const J).obj W ⟶ F
j✝ j'✝ : J
f : j✝ ⟶ j'✝
e_1✝ : (((const J).obj W).obj j✝ ⟶ F.obj j'✝) = (W ⟶ F.obj j'✝)
⊢ ((const J).obj W).map f ≫ π.app j'✝ = (fun j ↦ π.app j) j'✝
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'
⊢ 𝟙 W ≫ ↑p j' = ↑p j ≫ F.map f

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 : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ 𝟙 W ≫ ↑p j' = ↑p j ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : 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'
⊢ ↑p j' = ↑p j ≫ F.map f

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 : 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'
⊢ ↑p j' = ↑p j ≫ F.map f
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ 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
⊢ G.map (lift s ≫ t.π.app j) = G.map (s.π.app 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✝ 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
⊢ G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)
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
⊢ ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app 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✝ 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
⊢ ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app j)
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
⊢ G.map m = G.map (lift s)

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✝ 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
⊢ G.map m = G.map (lift s)
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'
⊢ f ≫ G.map g = (e X Y) ((e X Y).symm f) ≫ G.map 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
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'
⊢ f ≫ G.map g = (e X Y) ((e X Y).symm f) ≫ G.map 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_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 ≫ (e X Y) ((e X Y).symm g) = f ≫ 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_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 ≫ (e X Y) ((e X Y).symm g) = f ≫ 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 : 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
⊢ { pt := s.pt, π := (const J).map m ≫ (limitCone h).π } = 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 : 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
⊢ { pt := s.pt, π := (const J).map m ≫ (limitCone h).π } = 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 : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
⊢ { pt := { pt := pt✝, π := π✝ }.pt, π := (const J).map m ≫ (limitCone h).π } = { 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 : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
⊢ { pt := { pt := pt✝, π := π✝ }.pt, π := (const J).map m ≫ (limitCone h).π } = { 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 : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
j : J
⊢ ((const J).map m ≫ (limitCone h).π).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 : Cone F
X : C
h : F.cones.RepresentableBy X
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
m : { pt := pt✝, π := π✝ }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt✝, π := π✝ }.π.app j
j : J
⊢ ((const J).map m ≫ (limitCone h).π).app j = π✝.app j
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: case e'_3
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'
e_1✝ : (F.obj j ⟶ ((const J).obj W).obj j') = (F.obj j ⟶ W)
⊢ ι.app j ≫ ((const J).obj W).map f = (fun j ↦ ι.app j) j

Tactic:
;

Goal state after:
case e'_3
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'
e_1✝ : (F.obj j ⟶ ((const J).obj W).obj j') = (F.obj j ⟶ W)
⊢ ι.app j ≫ ((const J).obj W).map f = (fun j ↦ ι.app j) j