mathlib-initiative/mathlib-tactics huggingface dataset:
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 (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCone (Cone.whisker F c)).π.app j =
      (Iso.refl (H.mapCone (Cone.whisker F c)).pt).hom ≫ (Cone.whisker F (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✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (ofι f.op.unop ⋯).pt).hom ≫ (ofι f ⋯).ι =
    (ofι f.op.unop ⋯).ι ≫ (Iso.refl (Opposite.unop (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
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) := (isLimitWhiskerEquiv F (H.mapCone c)).symm hc
⊢ ∀ (j : C),
    (Cone.whisker F (H.mapCone c)).π.app j =
      (Iso.refl (Cone.whisker F (H.mapCone c)).pt).hom ≫ (H.mapCone (Cone.whisker F c)).π.app j

Tactic:
simp

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

Goal state before:
pp: case refine_2
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f =
    ((pushoutIsoUnopPullback f f).inv.op ≫ pullback.snd f.op f.op).unop

Tactic:
pushoutIsoUnopPullback_inv_snd,

Goal state after:
case refine_2
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 : IsColimit (Cofork.ofπ f.op ⋯)
⊢ (Iso.refl (Opposite.unop (Opposite.op Y))).hom ≫ pushout.inr f f = (pushout.inr f f).op.unop
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 ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.fst f.unop f.unop =
    (pushout.inl f f).unop ≫ (Iso.refl (Opposite.unop 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 ⋯)
⊢ ((pushoutIsoOpPullback f f).unop.symm ≪≫ eqToIso ⋯).hom ≫ pullback.snd f.unop f.unop =
    (pushout.inr f f).unop ≫ (Iso.refl (Opposite.unop 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.unop Y)).inv ≫ (Cofork.ofπ f.unop ⋯).π ≫ (Iso.refl (Cofork.ofπ f.unop ⋯).pt).hom =
    (Cofork.ofπ f.unop ⋯).π

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 : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (ofι f.unop.op ⋯).pt).hom ≫ (ofι f ⋯).ι =
    (ofι f.unop.op ⋯).ι ≫ (Iso.refl (Opposite.op (Opposite.unop Y))).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Fork (𝟙 Y) (𝟙 Y)), (s.ι ≫ e.inv) ≫ (Fork.ofι e.hom ⋯).ι = s.ι

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y W : C
f : X ⟶ Y
inst✝ : IsRegularMono f
k : W ⟶ Y
h : k ≫ left f = k ≫ right f
m : W ⟶ X
hm : m ≫ f = k
⊢ lift f k h ≫ (Fork.ofι f ⋯).ι = k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasLimit (parallelPair g h)
⊢ ∀ (s : Fork g h), limit.lift (parallelPair g h) s ≫ (Fork.ofι (equalizer.ι g h) ⋯).ι = s.ι

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
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ (StructuredArrow.mk (f ≫ Final.homToLift F Y)).hom ≫ F.map (𝟙 (StructuredArrow.mk (f ≫ Final.homToLift F Y)).right) =
    f ≫ Final.homToLift F Y ≫ F.map (𝟙 (Final.lift F Y))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
⊢ ∀ (s : Cofork (𝟙 X) (𝟙 X)), (Cofork.ofπ e.hom ⋯).π ≫ e.inv ≫ s.π = s.π

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
inst✝ : IsRegularEpi f
k : X ⟶ Z
h : left f ≫ k = right f ≫ k
m : Y ⟶ Z
hm : f ≫ m = k
⊢ (Cofork.ofπ f ⋯).π ≫ desc f k h = k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst✝ : HasColimit (parallelPair g h)
⊢ ∀ (s : Cofork g h), (Cofork.ofπ (coequalizer.π g h) ⋯).π ≫ colimit.desc (parallelPair g h) s = s.π

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
S : C
k : IsKernelPair f a b
p q : S ⟶ X
w : p ≫ f = q ≫ f
⊢ k.lift p q w ≫ a = p ∧ k.lift p q w ≫ b = q

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)), small_k.lift s.fst s.snd ⋯ ≫ (PullbackCone.mk a b ⋯).fst = s.fst

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ ∀ (s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)), small_k.lift s.fst s.snd ⋯ ≫ (PullbackCone.mk a b ⋯).snd = s.snd

Tactic:
simp

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

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
          (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).fiber =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.fiber

Tactic:
simp

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

Goal state before:
pp: case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
pf✝ :
  ((G ⋙ F).map (StructuredArrow.Hom.right g)).toFunctor.obj
      { base := X✝.right, fiber := (F.map X✝.hom).toFunctor.obj f }.fiber =
    { base := Y✝.right, fiber := (F.map Y✝.hom).toFunctor.obj f }.fiber
⊢ ((StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
        (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom pf✝ }).base =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom.base

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
⊢ IsConnected (StructuredArrow { base := d, fiber := f } (pre F G))

Tactic:
let : Nonempty (StructuredArrow ⟨d, f⟩ (pre F G)) :=
    ⟨u, ⟨c, (F.map g).toFunctor.obj f⟩, ⟨(by exact g), (by exact 𝟙 _)⟩⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
⊢ IsConnected (StructuredArrow { base := d, fiber := f } (pre F G))
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ s.π.app WalkingCospan.left = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).fst

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bi))).toFunctor.obj
      (StructuredArrow.mk
            { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).right.fiber =
    (F.map gbi).toFunctor.obj f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt
hm : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk a b ⋯).π.app j = s.π.app j
⊢ s.π.app WalkingCospan.right = small_k.lift s.fst s.snd ⋯ ≫ (IsPullback.cone small_k).snd

Tactic:
simp

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

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk
              { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
          (pre F G).map { base := _root_.id (𝟙 bi), fiber := eqToHom ⋯ ≫ gfi }).fiber =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bi, fiber := fi },
          hom := { base := gbi, fiber := gfi } }).fiber

Tactic:
simp

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

Goal state before:
pp: case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((StructuredArrow.mk { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
        (pre F G).map { base := _root_.id (𝟙 bi), fiber := eqToHom ⋯ ≫ gfi }).base =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bi, fiber := fi },
          hom := { base := gbi, fiber := gfi } }).base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
R X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
a b : R ⟶ X✝
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((G ⋙ F).map (_root_.id (𝟙 bj))).toFunctor.obj
      (StructuredArrow.mk
            { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).right.fiber =
    (F.map gbj).toFunctor.obj f

Tactic:
simp

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

Goal state before:
pp: case w_fiber
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ eqToHom ⋯ ≫
      ((StructuredArrow.mk
              { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
          (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).fiber =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).fiber

Tactic:
simp

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

Goal state before:
pp: case w_base
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ ((StructuredArrow.mk { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) }).hom ≫
        (pre F G).map { base := _root_.id (𝟙 bj), fiber := eqToHom ⋯ ≫ gfj }).base =
    (StructuredArrow.hom
        { left := { as := PUnit.unit }, right := { base := bj, fiber := fj },
          hom := { base := gbj, fiber := gfj } }).base

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_3.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.fst f g =
    s.fst ≫ pullback.fst f g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.snd f g =
    s.fst ≫ pullback.snd f g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).snd) ≫
      pullback.snd f g =
    s.snd ≫ pullback.snd f g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ diagonal f ≫ fst f f = diagonal f ≫ snd f f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a

Tactic:
rw [←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
          WalkingCospan.left)]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (Iso.refl X).hom = (Iso.refl A).hom ≫ p ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 A ≫ (asIso p).hom = (Iso.refl A).hom ≫ p

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ 𝟙 X ≫ (asIso f).hom = (Iso.refl X).hom ≫ f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
X Y : C
f : X ⟶ Y
a✝ : IsIso f
A B : C
p : A ⟶ B
hp : P p
g : B ⟶ X
h✝ : IsIso p
⊢ (p ≫ g) ≫ (asIso f).hom = (asIso p).hom ≫ g ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    fst i₁ i₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    snd i₁ i₂

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
S S' X Y : C
f : S' ⟶ S
v₁₂ : X ⟶ S
v₂₂ : Y ⟶ S
g : X ⟶ Y
hv₁₂ : v₁₂ = g ≫ v₂₂
inst✝¹ : HasPullback v₁₂ f
inst✝ : HasPullback v₂₂ f
H : P g
⊢ (pullback.fst v₁₂ f ≫ g) ≫ v₂₂ = pullback.snd v₁₂ f ≫ f

Tactic:
by simp [pullback.condition, ← hv₁₂]

Goal state after: