mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
X Y : C
f : Y ⟶ X
⊢ inv (inv f) = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u
inst✝¹ : Groupoid C
X Y : C
D : Type u_1
inst✝ : Groupoid D
F : C ⥤ D
u✝ v✝ : C
f : u✝ ⟶ v✝
⊢ F.toPrefunctor.map (Quiver.reverse f) = Quiver.reverse (F.toPrefunctor.map f)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y Y' : T
f : X ⟶ Y
h : Y = Y'
⊢ (mk (f ≫ eqToHom h)).hom = eqToHom ⋯ ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X' X Y : T
f : X ⟶ Y
h : X' = X
⊢ (mk (eqToHom h ≫ f)).hom = eqToHom h ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i = g.inv ≫ f ≫ h.hom

Tactic:
Iso.eq_inv_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ g.hom ≫ i = f ≫ h.hom
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
inst✝¹ : F.EssSurj
inst✝ : F.Full
X Y : D
f : X ⟶ Y
a✝ : ⊤ f
⊢ (F.objObjPreimageIso X).hom ≫ f =
    F.map (F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)) ≫ (F.objObjPreimageIso Y).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left e.hom ≫ Hom.left e.inv = 𝟙 f.left

Tactic:
← comp_left,

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (e.hom ≫ e.inv) = 𝟙 f.left
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : X✝ ⟶ Y✝
he : IsIso e
f : Y✝ ⟶ Z✝
x✝ : P.isoClosure f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom) ≪≫ asIso (inv e)).hom ≫ (Arrow.mk (e ≫ f)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom)).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left e.inv ≫ Hom.left e.hom = 𝟙 g.left

Tactic:
← comp_left,

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (e.inv ≫ e.hom) = 𝟙 g.left
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ Z✝ : C
e : Y✝ ⟶ Z✝
he : IsIso e
f : X✝ ⟶ Y✝
x✝ : P.isoClosure f
w✝¹ w✝ : C
f' : w✝¹ ⟶ w✝
hf' : P f'
iso : Arrow.mk f' ≅ Arrow.mk f
⊢ (asIso (Arrow.Hom.left iso.hom)).hom ≫ (Arrow.mk (f ≫ e)).hom =
    (Arrow.mk f').hom ≫ (asIso (Arrow.Hom.right iso.hom) ≪≫ asIso e).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : SplitEpi f
⊢ (f.op ≫ h.section_.op).unop = (𝟙 (Opposite.op Y)).unop

Tactic:
by simp

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

Goal state before:
pp: X Y : Type u
i : X ≅ Y
x : X
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

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

Goal state before:
pp: X Y : Type u
i : X ≅ Y
y : Y
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) y) = y

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
e : X ≅ Y
⊢ (F.mapIso e).hom ≫ (Arrow.mk (α.app Y)).hom = (Arrow.mk (α.app X)).hom ≫ (G.mapIso e).hom

Tactic:
by simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ L'.map (F₁.map φ.left) ≫
      { left := F₁.obj Y.left, right := F₂.obj Y.right, hom := α.app Y.left ≫ F.map Y.hom ≫ β.app Y.right }.hom =
    { left := F₁.obj X.left, right := F₂.obj X.right, hom := α.app X.left ≫ F.map X.hom ≫ β.app X.right }.hom ≫
      R'.map (F₂.map φ.right)

Tactic:
dsimp
        rw [assoc, assoc, ← Functor.comp_map, α.naturality_assoc, ← Functor.comp_map,
          ← β.naturality]
        dsimp
        rw [← F.map_comp_assoc, ← F.map_comp_assoc, φ.w]

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X : Comma L R
⊢ ((map α β).obj X).hom = (α.app X.left ≫ F.map X.hom) ≫ β.app X.right

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1

Tactic:
by simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
⊢ ∀ {X Y : Comma L R} (f : X ⟶ Y),
    (map α β ⋙ fst L' R').map f ≫ (Iso.refl ((map α β ⋙ fst L' R').obj Y)).hom =
      (Iso.refl ((map α β ⋙ fst L' R').obj X)).hom ≫ (fst L R ⋙ F₁).map f

Tactic:
by simp

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
A' : Type u₄
inst✝² : Category.{v₄, u₄} A'
B' : Type u₅
inst✝¹ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (R.op.map (op f.right) ≫ (unop (op { left := op X✝.right, right := op X✝.left, hom := op X✝.hom })).hom).unop =
    ((unop (op { left := op Y✝.right, right := op Y✝.left, hom := op Y✝.hom })).hom ≫ L.op.map (op f.left)).unop

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (α.homCongr γ) (f ≫ g) = (α.homCongr β) f ≫ (β.homCongr γ) g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ ((refl X).homCongr (refl Y)) f = f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
f : X₁ ⟶ Y₁
⊢ ((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 C).map f✝ ≫ (adj.homEquiv Y✝ (F.obj Y✝)) (𝟙 (F.obj Y✝)) =
    (adj.homEquiv X✝ (F.obj X✝)) (𝟙 (F.obj X✝)) ≫ (F ⋙ G).map f✝

Tactic:
simp [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]

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

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
hc : IsColimit t
X X' : C
f : X ⟶ X'
g : t.pt ⟶ X
j : J
⊢ (hc.homEquiv (g ≫ f)).app j = ((ConcreteCategory.hom (F.cocones.map f)) (hc.homEquiv g)).app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

Goal state after: