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

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).base =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G H : D ⥤ C
α : G ≅ H
X✝ Y✝ : Grothendieck (G ⋙ F)
f : X✝ ⟶ Y✝
⊢ eqToHom ⋯ ≫
      ((pre F G).map f ≫ ({ base := G.obj Y✝.base, fiber := Y✝.fiber }.transportIso (α.app Y✝.base)).symm.hom).fiber =
    (({ base := G.obj X✝.base, fiber := X✝.fiber }.transportIso (α.app X✝.base)).symm.hom ≫
        (map (whiskerRight α.hom F) ⋙ pre F H).map f).fiber

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
⊢ (F.map (𝟙 { base := c, fiber := X✝ }.base)).toFunctor.obj { base := c, fiber := X✝ }.fiber = X✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom = (inclLift F M hM).hom.app x ≫ M x

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
x : C
⊢ (match incl.obj x, star, starTerminal.from (incl.obj x) with
    | of a, of a_1, f => F.map (down f)
    | of x, star, x_1 => M x
    | star, star, x => 𝟙 Z) =
    M x
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.base =
    ({ base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f } ≫
        { base := 𝟙 { base := c, fiber := Y✝ }.base, fiber := eqToHom ⋯ ≫ g }).base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).base =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).base

Tactic:
simp

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

Goal state before:
pp: case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c : Comma (𝟭 (C ⥤ D)) (Functor.const C)
x y : C
f : x ⟶ y
⊢ c.left.map f ≫ c.hom.app y = c.hom.app x

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
⊢ ∀ (j : J),
    (limit.cone F).π.app j =
      ((asIso (limMap c.π)).symm ≪≫
            (limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom ≫
        c.π.app j

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
j : J
⊢ (limit.cone F).π.app j =
    ((asIso (limMap c.π)).symm ≪≫
          (limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom ≫
      c.π.app j
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f✝ : x ⟶ y
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
⊢ ((ofCommaObject c).map f ≫
      match of a✝ with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a✝¹ with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
a : C
x✝ : of a ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match of a with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
a : C
x✝ : of a ⟶ star
⊢ c.hom.app a ≫ φ.right = φ.left.app a ≫ c'.hom.app a
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (𝟭 (C ⥤ D)) (Functor.const C)
φ : c ⟶ c'
x y : WithTerminal C
f : x ⟶ y
x✝ : star ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.left.app x
      | star => φ.right) =
    (match star with
      | of x => φ.left.app x
      | star => φ.right) ≫
      (ofCommaObject c').map x✝

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasColimit F
c : Cocone F
inst✝ : IsIso (colimMap c.ι)
⊢ ∀ (j : J),
    (colimit.cocone F).ι.app j ≫
        (asIso (colimMap c.ι) ≪≫
            (colimit.isColimit ((Functor.const J).obj c.pt)).coconePointUniqueUpToIso
              (isColimitConstCocone J c.pt)).hom =
      c.ι.app j

Tactic:
simp

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        none) =
    none

Tactic:
simp

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

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
val✝ : J
⊢ (fun x ↦
        match x with
        | of x => some x.as
        | star => none)
      ((fun x ↦
          match x with
          | some x => of { as := x }
          | none => star)
        (some val✝)) =
    some val✝

Tactic:
simp

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

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
a✝ : Discrete J
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        (of a✝)) =
    of a✝

Tactic:
simp

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

Goal state before:
pp: case star
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
⊢ (fun x ↦
        match x with
        | some x => of { as := x }
        | none => star)
      ((fun x ↦
          match x with
          | of x => some x.as
          | star => none)
        star) =
    star

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (extendCocone.obj c)) := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ ∀ (j : D),
    (H.mapCocone (extendCocone.obj c)).ι.app j ≫ (Iso.refl (H.mapCocone (extendCocone.obj c)).pt).hom =
      (extendCocone.obj (H.mapCocone c)).ι.app j

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.snd =
    s.π.app j ≫ prod.snd

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (extendCocone.obj (H.mapCocone c)) := (isColimitExtendCoconeEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : D),
    (extendCocone.obj (H.mapCocone c)).ι.app j ≫ (Iso.refl (extendCocone.obj (H.mapCocone c)).pt).hom =
      (H.mapCocone (extendCocone.obj c)).ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm X✝) = X✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
X✝ Y✝ : WithTerminal (Discrete J)
f : X✝ ⟶ Y✝
⊢ Y✝ = widePullbackShapeEquivObj (widePullbackShapeEquivObj.symm Y✝)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) := isColimitOfPreserves H ((isColimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCocone (Cocone.whisker F c)).ι.app j ≫ (Iso.refl (H.mapCocone (Cocone.whisker F c)).pt).hom =
      (Cocone.whisker F (H.mapCocone c)).ι.app j

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), (m ≫ prod.snd) ≫ c.π.app j = (forgetCone s).π.app j

Tactic:
intro j

Goal state after:
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
j : J
⊢ (m ≫ prod.snd) ≫ c.π.app j = (forgetCone s).π.app j
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : C),
    (Cocone.whisker F (H.mapCocone c)).ι.app j ≫ (Iso.refl (Cocone.whisker F (H.mapCocone c)).pt).hom =
      (H.mapCocone (Cocone.whisker F c)).ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
W✝ : C
x✝¹ : X ⟶ W✝
x✝ : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ x✝¹ = g₂ ≫ x✝¹
⊢ f ≫ inv f ≫ x✝¹ = x✝¹

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
e_1✝ : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ (fromPUnit d).obj j₂.right)
⊢ j₁.hom = j₁.hom ≫ (fromPUnit d).map f.right

Tactic:
simp

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
e_1✝ : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ (fromPUnit d).obj j₂.right)
⊢ j₁.hom = j₁.hom ≫ (fromPUnit d).map f.right

Tactic:
simp

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

Goal state before:
pp: case of
C : Type u
inst✝ : Category.{v, u} C
a✝¹ b✝ c✝ d✝ : Cat
f✝ : a✝¹ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
a✝ : ↑a✝¹
⊢ (prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).toNatTrans.app (of a✝) =
    ((Cat.Hom.isoMk (mapComp (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
            Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom (prelaxfunctor.map h✝) ≫
              (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫
                Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv ≫
                  (Cat.Hom.isoMk (mapComp f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv).toNatTrans.app
      (of a✝)

Tactic:
simp

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

Goal state before:
pp: case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ (lift F M hM).map PUnit.unit = (M Y ≫ h.symm.hom.app Y) ≫ h.hom.app Y

Tactic:
simp

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

Goal state before:
pp: case star.star.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
⊢ G.map (𝟙 star) ≫ hG.hom = hG.hom ≫ 𝟙 Z

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsColimit (ofπ f ⋯)
⊢ (Iso.refl (Fork.ofι f.op ⋯).pt).hom ≫ (Fork.ofι f.op ⋯).ι = (Fork.ofι f.op ⋯).ι ≫ (Iso.refl (Opposite.op X)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (Functor.const C) (𝟭 (C ⥤ D))
φ : c ⟶ c'
x y : WithInitial C
f✝ : x ⟶ y
a✝¹ a✝ : C
f : of a✝¹ ⟶ of a✝
⊢ ((ofCommaObject c).map f ≫
      match of a✝ with
      | of x => φ.right.app x
      | star => φ.left) =
    (match of a✝¹ with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pullbackIsoUnopPushout f f).symm.hom ≫ pullback.fst f f =
    (pushout.inl f.op f.op).unop ≫ (Iso.refl (Opposite.unop (Opposite.op X))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (pullbackIsoUnopPushout f f).symm.hom ≫ pullback.snd f f =
    (pushout.inr f.op f.op).unop ≫ (Iso.refl (Opposite.unop (Opposite.op X))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op X))).inv ≫ (ofπ f.op.unop ⋯).π ≫ (Iso.refl (ofπ f.op.unop ⋯).pt).hom =
    (ofπ f ⋯).π

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (Functor.const C) (𝟭 (C ⥤ D))
φ : c ⟶ c'
x y : WithInitial C
f : x ⟶ y
x✝ : star ⟶ star
⊢ ((ofCommaObject c).map x✝ ≫
      match star with
      | of x => φ.right.app x
      | star => φ.left) =
    (match star with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
hc' : IsLimit (H.mapCone (extendCone.obj c)) := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
⊢ ∀ (j : D),
    (H.mapCone (extendCone.obj c)).π.app j =
      (Iso.refl (H.mapCone (extendCone.obj c)).pt).hom ≫ (extendCone.obj (H.mapCone c)).π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsColimit (ofπ f ⋯)
⊢ (Iso.refl (Fork.ofι f.unop ⋯).pt).hom ≫ (Fork.ofι f.unop ⋯).ι =
    (Fork.ofι f.unop ⋯).ι ≫ (Iso.refl (Opposite.unop X)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit G H
c : Cone (F ⋙ G)
hc : IsLimit (H.mapCone c)
hc' : IsLimit (extendCone.obj (H.mapCone c)) := (isLimitExtendConeEquiv F (H.mapCone c)).symm hc
⊢ ∀ (j : D),
    (extendCone.obj (H.mapCone c)).π.app j =
      (Iso.refl (extendCone.obj (H.mapCone c)).pt).hom ≫ (H.mapCone (extendCone.obj c)).π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (pullbackIsoOpPushout f f).symm.hom ≫ pullback.fst f f =
    (pushout.inl f.unop f.unop).op ≫ (Iso.refl (Opposite.op (Opposite.unop X))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (pullbackIsoOpPushout f f).symm.hom ≫ pullback.snd f f =
    (pushout.inr f.unop f.unop).op ≫ (Iso.refl (Opposite.op (Opposite.unop X))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPullback f f
h : IsLimit (Fork.ofι f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop X))).inv ≫ (ofπ f.unop.op ⋯).π ≫ (Iso.refl (ofπ f.unop.op ⋯).pt).hom =
    (ofπ f ⋯).π

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯).hom ≫ pullback.fst f.op f.op =
    (pushout.inl f f).op ≫ (Iso.refl (Opposite.op Y)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
j✝ : C
⊢ (limMap f ≫ limit.pre Y✝ F) ≫ limit.π (F ⋙ Y✝) j✝ = (limit.pre X✝ F ≫ limMap (F.whiskerLeft f)) ≫ limit.π (F ⋙ Y✝) j✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ ((pushoutIsoUnopPullback f f).op.symm ≪≫ eqToIso ⋯).hom ≫ pullback.snd f.op f.op =
    (pushout.inr f f).op ≫ (Iso.refl (Opposite.op Y)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsLimit (ofι f ⋯)
⊢ (Iso.refl (Opposite.op Y)).inv ≫ (Cofork.ofπ f.op ⋯).π ≫ (Iso.refl (Cofork.ofπ f.op ⋯).pt).hom = (Cofork.ofπ f.op ⋯).π

Tactic:
simp

Goal state after: