[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) _
