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

Goal state before:
pp: M N : MonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : MonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M : CommMonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N T : CommMonCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: M N : CommMonCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : GrpCat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y T : GrpCat
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X : CommGrpCat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y T : CommGrpCat
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑X
⊢ ((CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom)) x✝ = (MonoidHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv)) x✝ = (MonoidHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : SemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : SemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : RingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : RingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : CommSemiRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : CommSemiRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R : CommRingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

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

Tactic:
simp

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

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

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

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

Goal state after:
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:
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 : C
Y : D
f : F.obj X ⟶ Y
⊢ (F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X)) ≫ (𝟭 D).map f = f

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 : C
Y : D
g : X ⟶ G.obj Y
⊢ ((𝟭 C).map g ≫ adj.unit.app (G.obj Y)) ≫ G.map (adj.counit.app Y) = 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 : C
⊢ (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X)) = adj.unit.app X

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 : D
⊢ (adj.homEquiv (G.obj X) X).symm (𝟙 (G.obj X)) = adj.counit.app X

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 : C
⊢ (adj.homEquiv X (F.obj X)).symm (adj.unit.app X) = 𝟙 (F.obj X)

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

Tactic:
by
  rw [← Equiv.eq_symm_apply]
  simp only [Equiv.symm_apply_apply, homEquiv_naturality_left_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 : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g

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
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointUniqueUpToIso Q).hom) ≫ t.π.app j = r.π.app j

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
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointUniqueUpToIso Q).inv) ≫ s.π.app j = r.π.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
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:
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✝ : 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:
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
s t : Cone F
hs : IsLimit s
x✝ : Nonempty (IsLimit t)
ht : IsLimit t
⊢ ∀ (j : J), (hs.lift t ≫ ht.lift s) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j

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
s t : Cone F
hs : IsLimit s
x✝ : Nonempty (IsLimit t)
ht : IsLimit t
⊢ ∀ (j : J), (ht.lift s ≫ hs.lift t) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.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
adj : F ⊣ G
X' X✝ : C
Y Y' : D
X : C
⊢ ∀ {Y Y' : D} (g : Y ⟶ Y') (f : F.obj X ⟶ Y),
    (adj.homEquiv X Y') (f ≫ g) =
      (ConcreteCategory.hom ((G ⋙ coyoneda.obj (Opposite.op X)).map g)) ((adj.homEquiv X Y) f)

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✝ : Cone F✝
F G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (map s Q w.hom ≫ map t P w.inv) ≫ s.π.app j = 𝟙 s.pt ≫ s.π.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
adj : F ⊣ G
X' X : C
Y✝ Y' Y : D
⊢ ∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ G.obj Y),
    (adj.homEquiv X Y).symm (f ≫ g) =
      (ConcreteCategory.hom ((F.op ⋙ yoneda.obj Y).map f.op)) ((adj.homEquiv X' Y).symm g)

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✝ : Cone F✝
F G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (map t P w.inv ≫ map s Q w.hom) ≫ t.π.app j = 𝟙 t.pt ≫ t.π.app j

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 G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j

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 G : J ⥤ C
s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
j : J
⊢ (P.conePointsIsoOfNatIso Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j

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 G : J ⥤ C
r s : Cone F
t : Cone G
P : IsLimit s
Q : IsLimit t
w : F ≅ G
⊢ ∀ (j : J), (P.lift r ≫ (P.conePointsIsoOfNatIso Q w).hom) ≫ t.π.app j = map r Q w.hom ≫ t.π.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
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:
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 G : J ⥤ C
r s : Cone G
t : Cone F
P : IsLimit t
Q : IsLimit s
w : F ≅ G
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointsIsoOfNatIso Q w).inv) ≫ t.π.app j = map r P w.inv ≫ t.π.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
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:
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 : CoreHomEquivUnitCounit F G
X : C
⊢ adj.unit.app X = adj.unit.app X ≫ G.map (𝟙 (F.obj 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✝ : 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:
intro j

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 := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc 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.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 : CoreHomEquivUnitCounit F G
Y : D
⊢ adj.counit.app Y = F.map (𝟙 (G.obj Y)) ≫ adj.counit.app Y

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✝ : 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 := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫ F.map (e.unitInv.app j) ≫ w.inv.app ((𝟭 J).obj j) ≫ w.hom.app j =
    s.π.app j

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 : Cone F
h : IsLimit t
W : C
f : W ⟶ t.pt
⊢ ∀ (j : J), (fun π ↦ h.lift { pt := W, π := π }) ((fun f ↦ (t.extend f).π) f) ≫ t.π.app j = f ≫ t.π.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
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g ↦ iso.hom.app X ≫ g) ((fun f ↦ iso.inv.app X ≫ f) f) = f

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
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
g : F'.obj X ⟶ Y
⊢ (fun f ↦ iso.inv.app X ≫ f) ((fun g ↦ iso.hom.app X ≫ g) g) = 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 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:
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 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:
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 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:
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 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:
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
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✝
⊢ (f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) = f ≫ f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))

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

Goal state after: