mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Function.LeftInverse
    (fun h ↦
      (ofπ f.op.unop ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoUnopPushout f f).symm (Iso.refl (Opposite.unop (Opposite.op X))) (Iso.refl (ofπ f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.op ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) h) (Fork.ofι f.op ⋯)
      (Iso.refl (Opposite.op X)) (pullbackIsoUnopPushout f f).op.symm (Iso.refl (Fork.ofι f.op ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by

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

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
⊢ Function.RightInverse
    (fun h ↦
      (ofπ f.op.unop ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitUnop f.op f.op ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoUnopPushout f f).symm (Iso.refl (Opposite.unop (Opposite.op X))) (Iso.refl (ofπ f.op.unop ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.op ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) h) (Fork.ofι f.op ⋯)
      (Iso.refl (Opposite.op X)) (pullbackIsoUnopPushout f f).op.symm (Iso.refl (Fork.ofι f.op ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by

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 ⋯)
⊢ f.unop ≫ (pullback.fst f f).unop = f.unop ≫ (pullback.snd f f).unop

Tactic:
by

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
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of x)) ≫ (incl ⋙ F).map f = F.map (starInitial.to (of y))

Tactic:
simp only [Functor.comp_obj, Functor.comp_map]
          rw [← F.map_comp]
          congr 1

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
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of x)) ≫ (incl ⋙ F).map f = F.map (starInitial.to (of y))

Tactic:
by

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
s : Cone (F ⋙ G)
j : C
⊢ s.π.app (lift F (F.obj j)) ≫ G.map (homToLift F (F.obj j)) = s.π.app j

Tactic:
by

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 (Opposite.unop X)).hom ≫ pushout.inl f.unop f.unop =
    (pullback.fst f f).unop ≫ (pullbackIsoOpPushout f f).unop.symm.hom

Tactic:
by

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
F : WithInitial C ⥤ D
x : C
⊢ (Iso.refl (F.obj star)).symm.hom ≫ F.map (starInitial.to (incl.obj x)) =
    F.map (starInitial.to (of x)) ≫ (Iso.refl (incl ⋙ F)).symm.hom.app x

Tactic:
by

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 (Opposite.unop X)).hom ≫ pushout.inr f.unop f.unop =
    (pullback.snd f f).unop ≫ (pullbackIsoOpPushout f f).unop.symm.hom

Tactic:
by

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

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

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
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
by

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 ⋯)
⊢ (pushout.inl f.unop f.unop).op ≫ f.unop.op = (pushout.inr f.unop f.unop).op ≫ f.unop.op

Tactic:
by

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
x y : WithInitial C ⥤ D
f : x ⟶ y
⊢ (𝟭 (WithInitial C ⥤ D)).map f ≫
      (liftUnique (incl ⋙ y) (fun x ↦ y.map (starInitial.to (of x))) ⋯ y (Iso.refl (incl ⋙ y)) (Iso.refl (y.obj star))
          ⋯).hom =
    (liftUnique (incl ⋙ x) (fun x_1 ↦ x.map (starInitial.to (of x_1))) ⋯ x (Iso.refl (incl ⋙ x)) (Iso.refl (x.obj star))
          ⋯).hom ≫
      ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by

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

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

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

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)
⊢ Nonempty (IsLimit c)

Tactic:
by

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
x : WithInitial C ⥤ D
⊢ { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun F ↦
                  liftUnique (incl ⋙ F) (fun x ↦ F.map (starInitial.to (of x))) ⋯ F (Iso.refl (incl ⋙ F))
                    (Iso.refl (F.obj star)) ⋯)
                ⋯).hom.app
          x) ≫
      (NatIso.ofComponents
              (fun F ↦
                Iso.refl
                  (({ obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }).obj
                    F))
              ⋯).hom.app
        ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x) =
    𝟙 ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x)

Tactic:
by

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

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✝ : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
⊢ LiftableCone (F ⋙ G) H c

Tactic:
by

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
⊢ Function.LeftInverse
    (fun h ↦
      (ofπ f.unop.op ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoOpPushout f f).symm (Iso.refl (Opposite.op (Opposite.unop X))) (Iso.refl (ofπ f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.unop ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitUnop f f ⋯ ⋯ ⋯) h) (Fork.ofι f.unop ⋯)
      (Iso.refl (Opposite.unop X)) (pullbackIsoOpPushout f f).unop.symm (Iso.refl (Fork.ofι f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by

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
⊢ Function.RightInverse
    (fun h ↦
      (ofπ f.unop.op ⋯).isColimitOfIsos ((Fork.isLimitOfιEquivIsColimitOp f.unop f.unop ⋯ ⋯ ⋯) h) (ofπ f ⋯)
        (pullbackIsoOpPushout f f).symm (Iso.refl (Opposite.op (Opposite.unop X))) (Iso.refl (ofπ f.unop.op ⋯).pt) ⋯ ⋯
        ⋯)
    fun h ↦
    (Fork.ofι f.unop ⋯).isLimitOfIsos ((isColimitOfπEquivIsLimitUnop f f ⋯ ⋯ ⋯) h) (Fork.ofι f.unop ⋯)
      (Iso.refl (Opposite.unop X)) (pullbackIsoOpPushout f f).unop.symm (Iso.refl (Fork.ofι f.unop ⋯).pt) ⋯ ⋯ ⋯

Tactic:
by

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✝ : HasLimit G
⊢ IsIso (limit.pre G F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithTerminal C)ᵒᵖ
x : WithTerminal C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (down f).op
      | op star, op (of a), x, x_1 =>
        WithInitial.starInitial.to
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithInitial.of (op x)
            | star => WithInitial.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithInitial.of (op x)
        | star => WithInitial.star)

Tactic:
by

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 ⋯)
⊢ (pushout.inl f f).op ≫ f.op = (pushout.inr f f).op ≫ f.op

Tactic:
by

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

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✝
⊢ lim.map f ≫ (limitIso F Y✝).symm.hom = (limitIso F X✝).symm.hom ≫ ((whiskeringLeft C D E).obj F ⋙ lim).map f

Tactic:
by

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

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithInitial Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match x with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

Tactic:
by

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

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 ⋯)
⊢ f.op.unop ≫ (pullback.fst f.op f.op).unop = f.op.unop ≫ (pullback.snd f.op f.op).unop

Tactic:
by

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 (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
by

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y z : WithInitial Cᵒᵖ
f✝ : x ⟶ y
g✝ : y ⟶ z
x✝¹ x✝ : WithInitial Cᵒᵖ
f : WithInitial.star ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ (match WithInitial.star, x✝, f ≫ g with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    (match WithInitial.star, x✝¹, f with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (starTerminal.from
            (Opposite.unop
              (match WithInitial.of (op unop) with
              | WithInitial.of x => op (of (Opposite.unop x))
              | WithInitial.star => op star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star)) ≫
      match x✝¹, x✝, g with
      | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
      | WithInitial.star, WithInitial.of (op unop), x =>
        op
          (starTerminal.from
            (Opposite.unop
              (match WithInitial.of (op unop) with
              | WithInitial.of x => op (of (Opposite.unop x))
              | WithInitial.star => op star)))
      | WithInitial.star, WithInitial.star, x =>
        𝟙
          (match WithInitial.star with
          | WithInitial.of x => op (of (unop x))
          | WithInitial.star => op star)

Tactic:
by

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

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)
⊢ Nonempty (IsLimit c)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝¹ y✝ : (WithTerminal C)ᵒᵖ
f✝ : unop y✝ ⟶ unop x✝¹
x y : C
f : unop (op (of y)) ⟶ unop (op (of x))
x✝ : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithTerminal C)ᵒᵖ).map (op f) ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithTerminal C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithInitial.of (op x)
                  | star => WithInitial.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (down f).op
                  | op star, op (of a), x, x_2 =>
                    WithInitial.starInitial.to
                      (match op (of a) with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star)
                  | op star, op star, x, x_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithInitial.of (op x)
                        | star => WithInitial.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithInitial.of x => op (of (unop x))
                | WithInitial.star => op star,
              map := fun {x y} f ↦
                match x, y, f with
                | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
                | WithInitial.star, WithInitial.of (op unop), x =>
                  op
                    (starTerminal.from
                      (Opposite.unop
                        (match WithInitial.of (op unop) with
                        | WithInitial.of x => op (of (Opposite.unop x))
                        | WithInitial.star => op star)))
                | WithInitial.star, WithInitial.star, x =>
                  𝟙
                    (match WithInitial.star with
                    | WithInitial.of x => op (of (unop x))
                    | WithInitial.star => op star),
              map_id := ⋯, map_comp := ⋯ }).map
        (op f)

Tactic:
by

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 ⋯)
⊢ IsLimit (ofι f ⋯)

Tactic:
by

Goal state after: