[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj X).obj X_1 ⟶ (Functor.empty C).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (X_1 : Discrete PEmpty) → (Functor.empty C).obj X_1 ⟶ ((Functor.const (Discrete PEmpty)).obj X).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ (X : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj Y).obj X ⟶ F.obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ ∀ ⦃X Y_1 : Discrete PEmpty⦄ (f : X ⟶ Y_1),
    ((Functor.const (Discrete PEmpty)).obj Y).map f ≫ id (Discrete.casesOn Y_1 fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫ F.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
t : IsLimit { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }
X : C
⊢ (X_1 : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj X).obj X_1 ⟶ F.obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
t : IsLimit { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty)).obj X).map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ F.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
t : IsLimit { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }
X : C
f : X ⟶ Y
⊢ (X_1 : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj X).obj X_1 ⟶ F.obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
t : IsLimit { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }
X : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty)).obj X).map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ F.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
t : IsLimit { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }
X : C
f : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty),
    f ≫
        NatTrans.app { pt := Y, π := NatTrans.mk fun X => id (Discrete.casesOn X fun as => False.elim (_ : False)) }.π
          j =
      NatTrans.app { pt := X, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }.π
        j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ Function.LeftInverse (fun u => IsLimit.mk fun s => default) fun t X =>
    {
      toInhabited :=
        {
          default :=
            IsLimit.lift t
              { pt := X, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) } },
      uniq :=
        (_ :
          ∀ (f : X ⟶ Y),
            f =
              IsLimit.lift t
                { pt := X, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }) }
[PROOFSTEP]
dsimp [Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ ∀ (x : IsLimit { pt := Y, π := NatTrans.mk fun X => False.elim (_ : False) }),
    (IsLimit.mk fun s => IsLimit.lift x { pt := s.pt, π := NatTrans.mk fun X_1 => False.elim (_ : False) }) = x
[PROOFSTEP]
intro x
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
x : IsLimit { pt := Y, π := NatTrans.mk fun X => False.elim (_ : False) }
⊢ (IsLimit.mk fun s => IsLimit.lift x { pt := s.pt, π := NatTrans.mk fun X_1 => False.elim (_ : False) }) = x
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ Function.RightInverse (fun u => IsLimit.mk fun s => default) fun t X =>
    {
      toInhabited :=
        {
          default :=
            IsLimit.lift t
              { pt := X, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) } },
      uniq :=
        (_ :
          ∀ (f : X ⟶ Y),
            f =
              IsLimit.lift t
                { pt := X, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }) }
[PROOFSTEP]
dsimp [Function.RightInverse, Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
⊢ ∀ (x : (X : C) → Unique (X ⟶ Y)),
    (fun X => { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ Y), f = default) }) = x
[PROOFSTEP]
intro u
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
u : (X : C) → Unique (X ⟶ Y)
⊢ (fun X => { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ Y), f = default) }) = u
[PROOFSTEP]
funext X
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
Y : C
u : (X : C) → Unique (X ⟶ Y)
X : C
⊢ { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ Y), f = default) } = u X
[PROOFSTEP]
simp only
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ (X_1 : Discrete PEmpty) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty)).obj X).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ ((Functor.const (Discrete PEmpty)).obj X).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }
X : C
⊢ (X_1 : Discrete PEmpty) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty)).obj X).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }
X : C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ ((Functor.const (Discrete PEmpty)).obj X).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }
X : C
f : X✝ ⟶ X
⊢ (X_1 : Discrete PEmpty) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty)).obj X).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }
X : C
f : X✝ ⟶ X
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ ((Functor.const (Discrete PEmpty)).obj X).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X✝ : C
t : IsColimit { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }
X : C
f : X✝ ⟶ X
⊢ ∀ (j : Discrete PEmpty),
    NatTrans.app { pt := X✝, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) }.ι
          j ≫
        f =
      NatTrans.app { pt := X, ι := NatTrans.mk fun X_2 => id (Discrete.casesOn X_2 fun as => False.elim (_ : False)) }.ι
        j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ Function.LeftInverse (fun u => IsColimit.mk fun s => default) fun t X_1 =>
    {
      toInhabited :=
        {
          default :=
            IsColimit.desc t
              { pt := X_1, ι := NatTrans.mk fun X_2 => id (Discrete.casesOn X_2 fun as => False.elim (_ : False)) } },
      uniq :=
        (_ :
          ∀ (f : X ⟶ X_1),
            f =
              IsColimit.desc t
                { pt := X_1, ι := NatTrans.mk fun X_2 => id (Discrete.casesOn X_2 fun as => False.elim (_ : False)) }) }
[PROOFSTEP]
dsimp [Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ ∀ (x : IsColimit { pt := X, ι := NatTrans.mk fun X_1 => False.elim (_ : False) }),
    (IsColimit.mk fun s => IsColimit.desc x { pt := s.pt, ι := NatTrans.mk fun X_2 => False.elim (_ : False) }) = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
x✝ : IsColimit { pt := X, ι := NatTrans.mk fun X_1 => False.elim (_ : False) }
⊢ (IsColimit.mk fun s => IsColimit.desc x✝ { pt := s.pt, ι := NatTrans.mk fun X_2 => False.elim (_ : False) }) = x✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ Function.RightInverse (fun u => IsColimit.mk fun s => default) fun t X_1 =>
    {
      toInhabited :=
        {
          default :=
            IsColimit.desc t
              { pt := X_1, ι := NatTrans.mk fun X_2 => id (Discrete.casesOn X_2 fun as => False.elim (_ : False)) } },
      uniq :=
        (_ :
          ∀ (f : X ⟶ X_1),
            f =
              IsColimit.desc t
                { pt := X_1, ι := NatTrans.mk fun X_2 => id (Discrete.casesOn X_2 fun as => False.elim (_ : False)) }) }
[PROOFSTEP]
dsimp [Function.RightInverse, Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
⊢ ∀ (x : (Y : C) → Unique (X ⟶ Y)),
    (fun X_1 => { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ X_1), f = default) }) = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
x✝ : (Y : C) → Unique (X ⟶ Y)
⊢ (fun X_1 => { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ X_1), f = default) }) = x✝
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete PEmpty ⥤ C
X : C
x✝¹ : (Y : C) → Unique (X ⟶ Y)
x✝ : C
⊢ { toInhabited := { default := default }, uniq := (_ : ∀ (f : X ⟶ x✝), f = default) } = x✝¹ x✝
[PROOFSTEP]
simp only
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f g : Y ⟶ X
⊢ ∀ (j : Discrete PEmpty), f ≫ NatTrans.app (asEmptyCone X).π j = g ≫ NatTrans.app (asEmptyCone X).π j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f g : X ⟶ Y
⊢ ∀ (j : Discrete PEmpty), NatTrans.app (asEmptyCocone X).ι j ≫ f = NatTrans.app (asEmptyCocone X).ι j ≫ g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
⊢ Mono f
[PROOFSTEP]
haveI := t.isSplitMono_from f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsTerminal X
f : X ⟶ Y
this : IsSplitMono f
⊢ Mono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
⊢ Epi f
[PROOFSTEP]
haveI := t.isSplitEpi_to f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
t : IsInitial X
f : Y ⟶ X
this : IsSplitEpi f
⊢ Epi f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ (X : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj c.pt).obj X ⟶ F₁.obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty)).obj c.pt).map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫ F₁.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty), f ≫ NatTrans.app c₂.π j = NatTrans.app c.π j
⊢ f =
    (fun c =>
        IsLimit.lift hl
            { pt := c.pt, π := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) } ≫
          hi.hom)
      c
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty), f ≫ NatTrans.app c₂.π j = NatTrans.app c.π j
⊢ f = IsLimit.lift hl { pt := c.pt, π := NatTrans.mk fun X_1 => False.elim (_ : False) } ≫ hi.hom
[PROOFSTEP]
rw [← hl.uniq _ (f ≫ hi.inv) _]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty), f ≫ NatTrans.app c₂.π j = NatTrans.app c.π j
⊢ f = (f ≫ hi.inv) ≫ hi.hom
[PROOFSTEP]
simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
x✝ : ∀ (j : Discrete PEmpty), f ≫ NatTrans.app c₂.π j = NatTrans.app c.π j
⊢ ∀ (j : Discrete PEmpty),
    (f ≫ hi.inv) ≫ NatTrans.app c₁.π j =
      NatTrans.app { pt := c.pt, π := NatTrans.mk fun X_1 => False.elim (_ : False) }.π j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl => isLimitChangeEmptyCone C hl c₁ h.symm) fun hl => isLimitChangeEmptyCone C hl c₂ h
[PROOFSTEP]
dsimp [Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsLimit c₁), isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x c₂ h) c₁ h.symm = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsLimit c₁
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x✝ c₂ h) c₁ h.symm = x✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl => isLimitChangeEmptyCone C hl c₁ h.symm) fun hl => isLimitChangeEmptyCone C hl c₂ h
[PROOFSTEP]
dsimp [Function.LeftInverse, Function.RightInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsLimit c₂), isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x c₁ h.symm) c₂ h = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsLimit c₂
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x✝ c₁ h.symm) c₂ h = x✝
[PROOFSTEP]
funext
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsLimit c₂
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x✝ c₁ h.symm) c₂ h = x✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasLimit F₁
⊢ (X : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj (limit F₁)).obj X ⟶ F₂.obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasLimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty)).obj (limit F₁)).map f ≫
        id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫ F₂.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ (X : Discrete PEmpty) → F₁.obj X ⟶ ((Functor.const (Discrete PEmpty)).obj c.pt).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty⦄ (f : X ⟶ Y),
    F₁.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫ ((Functor.const (Discrete PEmpty)).obj c.pt).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app c₂.ι j ≫ f = NatTrans.app c.ι j
⊢ f =
    (fun c =>
        hi.inv ≫
          IsColimit.desc hl
            { pt := c.pt, ι := NatTrans.mk fun X_1 => id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) })
      c
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app c₂.ι j ≫ f = NatTrans.app c.ι j
⊢ f = hi.inv ≫ IsColimit.desc hl { pt := c.pt, ι := NatTrans.mk fun X_1 => False.elim (_ : False) }
[PROOFSTEP]
rw [← hl.uniq _ (hi.hom ≫ f) _]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app c₂.ι j ≫ f = NatTrans.app c.ι j
⊢ f = hi.inv ≫ hi.hom ≫ f
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty), NatTrans.app c₂.ι j ≫ f = NatTrans.app c.ι j
⊢ ∀ (j : Discrete PEmpty),
    NatTrans.app c₁.ι j ≫ hi.hom ≫ f =
      NatTrans.app { pt := c.pt, ι := NatTrans.mk fun X_1 => False.elim (_ : False) }.ι j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl => isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl =>
    isColimitChangeEmptyCocone C hl c₂ h
[PROOFSTEP]
dsimp [Function.LeftInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsColimit c₁), isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x c₂ h) c₁ h.symm = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsColimit c₁
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x✝ c₂ h) c₁ h.symm = x✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl => isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl =>
    isColimitChangeEmptyCocone C hl c₂ h
[PROOFSTEP]
dsimp [Function.LeftInverse, Function.RightInverse]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ ∀ (x : IsColimit c₂), isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x c₁ h.symm) c₂ h = x
[PROOFSTEP]
intro
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsColimit c₂
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x✝ c₁ h.symm) c₂ h = x✝
[PROOFSTEP]
funext
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x✝ : IsColimit c₂
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x✝ c₁ h.symm) c₂ h = x✝
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasColimit F₁
⊢ (X : Discrete PEmpty) → F₂.obj X ⟶ ((Functor.const (Discrete PEmpty)).obj (colimit F₁)).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty ⥤ C
F₂ : Discrete PEmpty ⥤ C
h : HasColimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty⦄ (f : X ⟶ Y),
    F₂.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X fun as => False.elim (_ : False)) ≫
        ((Functor.const (Discrete PEmpty)).obj (colimit F₁)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty ⥤ C
⊢ (X_1 : Discrete PEmpty) → ((Functor.const (Discrete PEmpty)).obj X).obj X_1 ⟶ F.obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty)).obj X).map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ F.map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty ⥤ C
⊢ (X_1 : Discrete PEmpty) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty)).obj X).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as => False.elim (_ : False)) =
      id (Discrete.casesOn X_1 fun as => False.elim (_ : False)) ≫ ((Functor.const (Discrete PEmpty)).obj X).map f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P Q : C
f : P ⟶ Q
⊢ f ≫ from Q = from P
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P Q : C
f : P ⟶ Q
⊢ to P ≫ f = to Q
[PROOFSTEP]
aesop
[GOAL]
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : HasTerminal C
j : J
⊢ limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j = terminal.from (⊤_ C)
[PROOFSTEP]
aesop_cat
[GOAL]
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : HasInitial C
j : J
⊢ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to (⊥_ C)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f
[PROOFSTEP]
rw [hI.hom_ext f (hI.to X)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (to hI X)
[PROOFSTEP]
apply InitialMonoClass.isInitial_mono_from
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono (IsInitial.to hI' X)
[PROOFSTEP]
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((IsInitial.uniqueUpToIso hI' hI).hom ≫ IsInitial.to hI X)
[PROOFSTEP]
apply mono_comp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ ((Functor.const J).obj (F.obj X)).map k ≫ (fun j => F.map (IsInitial.to tX j)) j' =
    (fun j => F.map (IsInitial.to tX j)) j ≫ F.map k
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ 𝟙 (F.obj X) ≫ F.map (IsInitial.to tX j') = F.map (IsInitial.to tX j) ≫ F.map k
[PROOFSTEP]
rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
⊢ m = (fun s => NatTrans.app s.π X) s
[PROOFSTEP]
conv_lhs => dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
| m
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
| m
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
| m
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
⊢ m = (fun s => NatTrans.app s.π X) s
[PROOFSTEP]
simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
⊢ m = m ≫ F.map (𝟙 X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfDiagramInitial tX F).π j = NatTrans.app s.π j
⊢ m = m ≫ F.map (𝟙 X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    ((Functor.const J).obj (F.obj X)).map f ≫ (fun i => inv (F.map (IsTerminal.from hX i))) Y =
      (fun i => inv (F.map (IsTerminal.from hX i))) X_1 ≫ F.map f
[PROOFSTEP]
intro i j f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ ((Functor.const J).obj (F.obj X)).map f ≫ (fun i => inv (F.map (IsTerminal.from hX i))) j =
    (fun i => inv (F.map (IsTerminal.from hX i))) i ≫ F.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ 𝟙 (F.obj X) ≫ inv (F.map (IsTerminal.from hX j)) = inv (F.map (IsTerminal.from hX i)) ≫ F.map f
[PROOFSTEP]
simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.id_comp, ← F.map_comp, hX.hom_ext (hX.from i) (f ≫ hX.from j)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ (fun j => F.map (IsTerminal.from tX j)) j' =
    (fun j => F.map (IsTerminal.from tX j)) j ≫ ((Functor.const J).obj (F.obj X)).map k
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (IsTerminal.from tX j') = F.map (IsTerminal.from tX j) ≫ 𝟙 (F.obj X)
[PROOFSTEP]
rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s => NatTrans.app s.ι X) s
[PROOFSTEP]
conv_rhs =>
  dsimp
    -- Porting note: why do I need this much firepower?
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
| (fun s => NatTrans.app s.ι X) s
[PROOFSTEP]
dsimp
    -- Porting note: why do I need this much firepower?
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
| (fun s => NatTrans.app s.ι X) s
[PROOFSTEP]
dsimp
    -- Porting note: why do I need this much firepower?
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
| (fun s => NatTrans.app s.ι X) s
[PROOFSTEP]
dsimp
  -- Porting note: why do I need this much firepower?
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = NatTrans.app s.ι X
[PROOFSTEP]
rw [← w X, coconeOfDiagramTerminal_ι_app, tX.hom_ext (tX.from X) (𝟙 _)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfDiagramTerminal tX F).ι j ≫ m = NatTrans.app s.ι j
⊢ m = F.map (𝟙 X) ≫ m
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    F.map f ≫ (fun i => inv (F.map (IsInitial.to hX i))) Y =
      (fun i => inv (F.map (IsInitial.to hX i))) X_1 ≫ ((Functor.const J).obj (F.obj X)).map f
[PROOFSTEP]
intro i j f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ (fun i => inv (F.map (IsInitial.to hX i))) j =
    (fun i => inv (F.map (IsInitial.to hX i))) i ≫ ((Functor.const J).obj (F.obj X)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (IsInitial.to hX j)) = inv (F.map (IsInitial.to hX i)) ≫ 𝟙 (F.obj X)
[PROOFSTEP]
simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.comp_id, ← F.map_comp, hX.hom_ext (hX.to i ≫ f) (hX.to j)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.lift F (coneOfDiagramInitial I F) ≫ limit.π F j = 𝟙 (F.obj j)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.lift F (coneOfDiagramTerminal I F) ≫ limit.π F j = 𝟙 (F.obj j)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramTerminal I F) = 𝟙 (F.obj j)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = 𝟙 (colimit F)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j) ∧
    colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)
[PROOFSTEP]
refine ⟨?_, by ext; simp⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j)
[PROOFSTEP]
simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app, Functor.const_obj_obj,
  IsInitial.to_self, Functor.map_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ inv (𝟙 (F.obj j)) = 𝟙 (F.obj j)
[PROOFSTEP]
dsimp [inv]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Classical.choose (_ : ∃ inv, 𝟙 (F.obj j) ≫ inv = 𝟙 (F.obj j) ∧ inv ≫ 𝟙 (F.obj j) = 𝟙 (F.obj j)) = 𝟙 (F.obj j)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, and_self]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Classical.choose (_ : ∃ x, (fun x => x = 𝟙 (F.obj j)) x) = 𝟙 (F.obj j)
[PROOFSTEP]
apply @Classical.choose_spec _ (fun x => x = 𝟙 F.obj j) _


[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ (e ≫ π₁) ≫ f = (e ≫ π₂) ≫ g
[PROOFSTEP]
rw [Category.assoc, equalizer.condition]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ equalizer.ι (π₁ ≫ f) (π₂ ≫ g) ≫ π₂ ≫ g = (e ≫ π₂) ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
    prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g
[PROOFSTEP]
rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
⊢ NatTrans.app (BinaryFan.mk (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right)).π
        { as := WalkingPair.left } ≫
      f =
    NatTrans.app (BinaryFan.mk (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right)).π
        { as := WalkingPair.right } ≫
      g
[PROOFSTEP]
exact PullbackCone.condition _
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        e ≫ π₁ =
      PullbackCone.fst s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
⊢ ∀ (s : PullbackCone f g),
    (fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        e ≫ π₂ =
      PullbackCone.snd s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ m =
    (fun s =>
        equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
          (_ :
            prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
              prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
      s
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.fst =
    ((fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.fst
[PROOFSTEP]
dsimp
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g)) ≫ prod.fst =
    (equalizer.lift (prod.lift (PullbackCone.fst s) (PullbackCone.snd s))
          (_ :
            prod.lift (PullbackCone.fst s) (PullbackCone.snd s) ≫ prod.fst ≫ f =
              prod.lift (PullbackCone.fst s) (PullbackCone.snd s) ≫ prod.snd ≫ g) ≫
        equalizer.ι (prod.fst ≫ f) (prod.snd ≫ g)) ≫
      prod.fst
[PROOFSTEP]
simpa using h₁
[GOAL]
case h.h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasLimit (pair X Y)
inst✝ : HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))
π₁ : X ⨯ Y ⟶ X := prod.fst
π₂ : X ⨯ Y ⟶ Y := prod.snd
e : equalizer (π₁ ≫ f) (π₂ ≫ g) ⟶ X ⨯ Y := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
s : PullbackCone f g
m : s.pt ⟶ equalizer (π₁ ≫ f) (π₂ ≫ g)
h₁ : m ≫ e ≫ π₁ = PullbackCone.fst s
h₂ : m ≫ e ≫ π₂ = PullbackCone.snd s
⊢ (m ≫ equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫ prod.snd =
    ((fun s =>
            equalizer.lift (prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right))
              (_ :
                prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₁ ≫ f =
                  prod.lift (NatTrans.app s.π WalkingCospan.left) (NatTrans.app s.π WalkingCospan.right) ≫ π₂ ≫ g))
          s ≫
        equalizer.ι (π₁ ≫ f) (π₂ ≫ g)) ≫
      prod.snd
[PROOFSTEP]
simpa using h₂
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, coequalizer.condition]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
    (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)
[PROOFSTEP]
rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
⊢ f ≫
      NatTrans.app (BinaryCofan.mk (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)).ι
        { as := WalkingPair.left } =
    g ≫
      NatTrans.app (BinaryCofan.mk (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)).ι
        { as := WalkingPair.right }
[PROOFSTEP]
exact PushoutCocone.condition _
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ ∀ (s : PushoutCocone f g),
    (ι₁ ≫ c) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s =
      PushoutCocone.inl s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ ∀ (s : PushoutCocone f g),
    (ι₂ ≫ c) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s =
      PushoutCocone.inr s
[PROOFSTEP]
simp
[GOAL]
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ m =
    (fun s =>
        coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
          (_ :
            (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
              (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
      s
[PROOFSTEP]
ext
[GOAL]
case h.h₁
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ coprod.inl ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inl ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s
[PROOFSTEP]
simpa using h₁
[GOAL]
case h.h₂
C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
s : PushoutCocone f g
m : coequalizer (f ≫ ι₁) (g ≫ ι₂) ⟶ s.pt
h₁ : (ι₁ ≫ c) ≫ m = PushoutCocone.inl s
h₂ : (ι₂ ≫ c) ≫ m = PushoutCocone.inr s
⊢ coprod.inr ≫ coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫ m =
    coprod.inr ≫
      coequalizer.π (f ≫ ι₁) (g ≫ ι₂) ≫
        (fun s =>
            coequalizer.desc (coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right))
              (_ :
                (f ≫ ι₁) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right) =
                  (g ≫ ι₂) ≫ coprod.desc (NatTrans.app s.ι WalkingSpan.left) (NatTrans.app s.ι WalkingSpan.right)))
          s
[PROOFSTEP]
simpa using h₂


[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteLimits C
⊢ HasLimitsOfShape J C
[PROOFSTEP]
apply @hasLimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteLimits C
⊢ HasLimitsOfShape (FinCategory.AsType J) C
[PROOFSTEP]
apply HasFiniteLimits.out
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasLimitsOfShape J C
[PROOFSTEP]
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift J)) C
⊢ HasLimitsOfShape J C
[PROOFSTEP]
have l : @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasLimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasLimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasLimitsOfShape J C
[PROOFSTEP]
apply
  @hasLimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
    (@Equivalence.symm J hJ (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l)
    _
      /- Porting note: tried to factor out (@instCategoryULiftHom (ULift J) (@uliftCategory J hJ)
          but when doing that would then find the instance and say it was not definitionally equal to
          the provided one (the same thing factored out) -/
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteColimits C
⊢ HasColimitsOfShape J C
[PROOFSTEP]
refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasFiniteColimits C
⊢ HasColimitsOfShape (FinCategory.AsType J) C
[PROOFSTEP]
apply HasFiniteColimits.out
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
⊢ HasColimitsOfShape J C
[PROOFSTEP]
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
⊢ HasColimitsOfShape J C
[PROOFSTEP]
have l : @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
  @ULiftHomULiftCategory.equiv J hJ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J}, FinCategory J → HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift J)) C
l : J ≌ ULiftHom (ULift J)
⊢ HasColimitsOfShape J C
[PROOFSTEP]
apply
  @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
    (@Equivalence.symm J hJ (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ List.toFinset [zero, one]
[PROOFSTEP]
cases x
[GOAL]
case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ zero ∈ List.toFinset [zero, one]
[PROOFSTEP]
simp
[GOAL]
case one
C : Type u
inst✝ : Category.{v, u} C
⊢ one ∈ List.toFinset [zero, one]
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
j j' : WalkingParallelPair
⊢ ∀ (x : WalkingParallelPairHom j j'),
    x ∈
      WalkingParallelPair.recOn j
        (WalkingParallelPair.recOn j' (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
        (WalkingParallelPair.recOn j' ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
⊢ left ∈
    WalkingParallelPair.recOn zero
      (WalkingParallelPair.recOn one (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn one ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
⊢ right ∈
    WalkingParallelPair.recOn zero
      (WalkingParallelPair.recOn one (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn one ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
j : WalkingParallelPair
⊢ WalkingParallelPairHom.id j ∈
    WalkingParallelPair.recOn j
      (WalkingParallelPair.recOn j (List.toFinset [WalkingParallelPairHom.id zero]) (List.toFinset [left, right]))
      (WalkingParallelPair.recOn j ∅ (List.toFinset [WalkingParallelPairHom.id one]))
[PROOFSTEP]
simp
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
j : WalkingParallelPair
⊢ 𝟙 j ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} j) (WalkingParallelPair.rec ∅ {𝟙 one} j) j
[PROOFSTEP]
cases j
[GOAL]
case id.zero
C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟙 zero ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} zero)
      (WalkingParallelPair.rec ∅ {𝟙 one} zero) zero
[PROOFSTEP]
simp
[GOAL]
case id.one
C : Type u
inst✝ : Category.{v, u} C
⊢ 𝟙 one ∈
    WalkingParallelPair.rec (WalkingParallelPair.rec {𝟙 zero} {left, right} one) (WalkingParallelPair.rec ∅ {𝟙 one} one)
      one
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteLimits C
⊢ HasEqualizers C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasFiniteColimits C
⊢ HasCoequalizers C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (WidePullbackShape J)
[PROOFSTEP]
rw [WidePullbackShape]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (Option J)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ Finset (j ⟶ j')
[PROOFSTEP]
cases' j' with j'
[GOAL]
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)
[PROOFSTEP]
cases' j with j
[GOAL]
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
[PROOFSTEP]
exact {Hom.id none}
[GOAL]
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)
[PROOFSTEP]
exact {Hom.term j}
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
by_cases some j' = j
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
by_cases some j' = j
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
rw [h]
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : some j' = j
⊢ Finset (j ⟶ j)
[PROOFSTEP]
exact {Hom.id j}
[GOAL]
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')
[PROOFSTEP]
exact ∅
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePullbackShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn (motive := fun t => j' = t → Finset (j ⟶ j')) j'
        (fun h =>
          (_ : none = j') ▸
            Option.casesOn (motive := fun t => j = t → Finset (j ⟶ none)) j (fun h => (_ : none = j) ▸ {Hom.id none})
              (fun j_1 h => (_ : some j_1 = j) ▸ {Hom.term j_1}) (_ : j = j))
        (fun j'_1 h =>
          (_ : some j'_1 = j') ▸
            if h : some j'_1 = j then Eq.mpr (_ : Finset (j ⟶ some j'_1) = Finset (j ⟶ j)) {Hom.id j} else ∅)
        (_ : j' = j')
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Hom.id j ∈
    Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j)) j
      (fun h =>
        (_ : none = j) ▸
          Option.casesOn (motive := fun t => j = t → Finset (j ⟶ none)) j (fun h => (_ : none = j) ▸ {Hom.id none})
            (fun j_1 h => (_ : some j_1 = j) ▸ {Hom.term j_1}) (_ : j = j))
      (fun j' h =>
        (_ : some j' = j) ▸
          if h : some j' = j then Eq.mpr (_ : Finset (j ⟶ some j') = Finset (j ⟶ j)) {Hom.id j} else ∅)
      (_ : j = j)
[PROOFSTEP]
cases j
[GOAL]
case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
            (fun h => (_ : none = none) ▸ {Hom.id none}) (fun j h => (_ : some j = none) ▸ {Hom.term j})
            (_ : none = none))
      (fun j' h =>
        (_ : some j' = none) ▸
          if h : some j' = none then Eq.mpr (_ : Finset (none ⟶ some j') = Finset (none ⟶ none)) {Hom.id none} else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ some val✝)) (some val✝)
      (fun h =>
        (_ : none = some val✝) ▸
          Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ none)) (some val✝)
            (fun h => (_ : none = some val✝) ▸ {Hom.id none}) (fun j h => (_ : some j = some val✝) ▸ {Hom.term j})
            (_ : some val✝ = some val✝))
      (fun j' h =>
        (_ : some j' = some val✝) ▸
          if h : some j' = some val✝ then
            Eq.mpr (_ : Finset (some val✝ ⟶ some j') = Finset (some val✝ ⟶ some val✝)) {Hom.id (some val✝)}
          else ∅)
      (_ : some val✝ = some val✝)
[PROOFSTEP]
simp
[GOAL]
case term
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.term j✝ ∈
    Option.casesOn (motive := fun t => none = t → Finset (some j✝ ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => some j✝ = t → Finset (some j✝ ⟶ none)) (some j✝)
            (fun h => (_ : none = some j✝) ▸ {Hom.id none}) (fun j h => (_ : some j = some j✝) ▸ {Hom.term j})
            (_ : some j✝ = some j✝))
      (fun j' h =>
        (_ : some j' = none) ▸
          if h : some j' = some j✝ then
            Eq.mpr (_ : Finset (some j✝ ⟶ some j') = Finset (some j✝ ⟶ some j✝)) {Hom.id (some j✝)}
          else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (WidePushoutShape J)
[PROOFSTEP]
rw [WidePushoutShape]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : Fintype J
⊢ Fintype (Option J)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')
[PROOFSTEP]
cases' j with j
[GOAL]
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')
[PROOFSTEP]
cases' j' with j'
[GOAL]
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)
[PROOFSTEP]
exact {Hom.id none}
[GOAL]
case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : J
⊢ Finset (none ⟶ some j')
[PROOFSTEP]
exact {Hom.init j'}
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
by_cases some j = j'
[GOAL]
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
by_cases some j = j'
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
rw [h]
[GOAL]
case pos
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : some j = j'
⊢ Finset (j' ⟶ j')
[PROOFSTEP]
exact {Hom.id j'}
[GOAL]
case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')
[PROOFSTEP]
exact ∅
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ ∀ (x : j ⟶ j'),
    x ∈
      Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j')) j
        (fun h =>
          (_ : none = j) ▸
            Option.casesOn (motive := fun t => j' = t → Finset (none ⟶ j')) j'
              (fun h => (_ : none = j') ▸ {Hom.id none}) (fun j'_1 h => (_ : some j'_1 = j') ▸ {Hom.init j'_1})
              (_ : j' = j'))
        (fun j_1 h =>
          (_ : some j_1 = j) ▸
            if h : some j_1 = j' then Eq.mpr (_ : Finset (some j_1 ⟶ j') = Finset (j' ⟶ j')) {Hom.id j'} else ∅)
        (_ : j = j)
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case id
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePushoutShape J
⊢ Hom.id j ∈
    Option.casesOn (motive := fun t => j = t → Finset (j ⟶ j)) j
      (fun h =>
        (_ : none = j) ▸
          Option.casesOn (motive := fun t => j = t → Finset (none ⟶ j)) j (fun h => (_ : none = j) ▸ {Hom.id none})
            (fun j' h => (_ : some j' = j) ▸ {Hom.init j'}) (_ : j = j))
      (fun j_1 h =>
        (_ : some j_1 = j) ▸
          if h : some j_1 = j then Eq.mpr (_ : Finset (some j_1 ⟶ j) = Finset (j ⟶ j)) {Hom.id j} else ∅)
      (_ : j = j)
[PROOFSTEP]
cases j
[GOAL]
case id.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Hom.id none ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => none = t → Finset (none ⟶ none)) none
            (fun h => (_ : none = none) ▸ {Hom.id none}) (fun j' h => (_ : some j' = none) ▸ {Hom.init j'})
            (_ : none = none))
      (fun j h =>
        (_ : some j = none) ▸
          if h : some j = none then Eq.mpr (_ : Finset (some j ⟶ none) = Finset (none ⟶ none)) {Hom.id none} else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
val✝ : J
⊢ Hom.id (some val✝) ∈
    Option.casesOn (motive := fun t => some val✝ = t → Finset (some val✝ ⟶ some val✝)) (some val✝)
      (fun h =>
        (_ : none = some val✝) ▸
          Option.casesOn (motive := fun t => some val✝ = t → Finset (none ⟶ some val✝)) (some val✝)
            (fun h => (_ : none = some val✝) ▸ {Hom.id none}) (fun j' h => (_ : some j' = some val✝) ▸ {Hom.init j'})
            (_ : some val✝ = some val✝))
      (fun j h =>
        (_ : some j = some val✝) ▸
          if h : some j = some val✝ then
            Eq.mpr (_ : Finset (some j ⟶ some val✝) = Finset (some val✝ ⟶ some val✝)) {Hom.id (some val✝)}
          else ∅)
      (_ : some val✝ = some val✝)
[PROOFSTEP]
simp
[GOAL]
case init
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j✝ : J
⊢ Hom.init j✝ ∈
    Option.casesOn (motive := fun t => none = t → Finset (none ⟶ some j✝)) none
      (fun h =>
        (_ : none = none) ▸
          Option.casesOn (motive := fun t => some j✝ = t → Finset (none ⟶ some j✝)) (some j✝)
            (fun h => (_ : none = some j✝) ▸ {Hom.id none}) (fun j' h => (_ : some j' = some j✝) ▸ {Hom.init j'})
            (_ : some j✝ = some j✝))
      (fun j h =>
        (_ : some j = none) ▸
          if h : some j = some j✝ then
            Eq.mpr (_ : Finset (some j ⟶ some j✝) = Finset (some j✝ ⟶ some j✝)) {Hom.id (some j✝)}
          else ∅)
      (_ : none = none)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
cases nonempty_fintype J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
val✝ : Fintype J
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
haveI := @HasFiniteWidePullbacks.out C _ _ J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
val✝ : Fintype J
this : ∀ [inst : Fintype J], HasLimitsOfShape (WidePullbackShape J) C
⊢ HasLimitsOfShape (WidePullbackShape J) C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
cases nonempty_fintype J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
val✝ : Fintype J
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
haveI := @HasFiniteWidePushouts.out C _ _ J
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePushouts C
val✝ : Fintype J
this : ∀ [inst : Fintype J], HasColimitsOfShape (WidePushoutShape J) C
⊢ HasColimitsOfShape (WidePushoutShape J) C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
J : Type v
x : WalkingPair
⊢ x ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
cases x
[GOAL]
case left
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.left ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
simp
[GOAL]
case right
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ WalkingPair.right ∈ {WalkingPair.left, WalkingPair.right}
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePullbacks C
⊢ HasPullbacks C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type v
inst✝ : HasFiniteWidePushouts C
⊢ HasPushouts C
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
⊢ HasInitial C
[PROOFSTEP]
let endos := T ⟶ T
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
⊢ HasInitial C
[PROOFSTEP]
let i := wideEqualizer.ι (id : endos → endos)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
⊢ HasInitial C
[PROOFSTEP]
haveI : Nonempty endos := ⟨𝟙 _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial C
[PROOFSTEP]
have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) :=
  by
  intro X
  refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
  let E := equalizer a (i ≫ Classical.choice (hT _))
  let e : E ⟶ wideEqualizer id := equalizer.ι _ _
  let h : T ⟶ E := Classical.choice (hT E)
  have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
    rw [Category.assoc, Category.assoc]
    apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
  rw [Category.comp_id, cancel_mono_id i] at this
  haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
  rw [← cancel_epi e]
  apply equalizer.condition
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ (X : C) → Unique (wideEqualizer id ⟶ X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
⊢ Unique (wideEqualizer id ⟶ X)
[PROOFSTEP]
refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
⊢ a = default
[PROOFSTEP]
let E := equalizer a (i ≫ Classical.choice (hT _))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
[PROOFSTEP]
let e : E ⟶ wideEqualizer id := equalizer.ι _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
[PROOFSTEP]
let h : T ⟶ E := Classical.choice (hT E)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ a = default
[PROOFSTEP]
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
  rw [Category.assoc, Category.assoc]
  apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
[PROOFSTEP]
apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
[PROOFSTEP]
rw [Category.comp_id, cancel_mono_id i] at this
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default
[PROOFSTEP]
haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default
[PROOFSTEP]
rw [← cancel_epi e]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ e ≫ a = e ≫ default
[PROOFSTEP]
apply equalizer.condition
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C
[PROOFSTEP]
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))