[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_to f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_to g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g
[PROOFSTEP]
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
⊢ X ⨯ I ≅ I
[PROOFSTEP]
have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct X I
hI : IsInitial I
this : IsIso prod.snd
⊢ X ⨯ I ≅ I
[PROOFSTEP]
exact asIso prod.snd
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
⊢ I ⨯ X ≅ I
[PROOFSTEP]
have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
I X : C
inst✝ : HasBinaryProduct I X
hI : IsInitial I
this : IsIso prod.fst
⊢ I ⨯ X ≅ I
[PROOFSTEP]
exact asIso prod.fst
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ IsInitial.to hI (⊥_ C))
⊢ f ≫ IsInitial.to hI (⊥_ C) ≫ inv (f ≫ IsInitial.to hI (⊥_ C)) = 𝟙 A
[PROOFSTEP]
rw [← assoc, IsIso.hom_inv_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_from f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this : IsIso f
⊢ f = g
[PROOFSTEP]
haveI := hI.isIso_from g
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictTerminalObjects C
I : C
hI : IsTerminal I
A : C
f g : I ⟶ A
this✝ : IsIso f
this : IsIso g
⊢ f = g
[PROOFSTEP]
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)
[PROOFSTEP]
classical
refine' ⟨⟨limit.lift _ ⟨_, ⟨_, _⟩⟩, _, _⟩⟩
· exact fun j => dite (j = i) (fun h => eqToHom (by cases h; rfl)) fun h => (H _ h).from _
· intro j k f
  split_ifs with h h_1 h_1
  · cases h
    cases h_1
    obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
    simp
  · cases h
    erw [Category.comp_id]
    haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
    rw [← IsIso.comp_inv_eq]
    apply (H _ h_1).hom_ext
  · cases h_1
    apply (H _ h).hom_ext
  · apply (H _ h).hom_ext
· ext
  rw [assoc, limit.lift_π]
  dsimp only
  split_ifs with h
  · cases h
    rw [id_comp, eqToHom_refl]
    exact comp_id _
  · apply (H _ h).hom_ext
· rw [limit.lift_π]
  simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)
[PROOFSTEP]
refine' ⟨⟨limit.lift _ ⟨_, ⟨_, _⟩⟩, _, _⟩⟩
[GOAL]
case refine'_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ (X : J) → ((Functor.const J).obj (F.toPrefunctor.1 i)).obj X ⟶ F.obj X
[PROOFSTEP]
exact fun j => dite (j = i) (fun h => eqToHom (by cases h; rfl)) fun h => (H _ h).from _
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
        if h : Y = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj Y = F.obj Y)
        else IsTerminal.from (H Y h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj Y)) =
      (if h : X = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj X = F.obj X)
        else IsTerminal.from (H X h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj X)) ≫
        F.map f
[PROOFSTEP]
intro j k f
[GOAL]
case refine'_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
⊢ (((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      if h : k = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k)
      else IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k)) =
    (if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
      else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j)) ≫
      F.map f
[PROOFSTEP]
split_ifs with h h_1 h_1
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h_1
[GOAL]
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
f : i ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map f
[PROOFSTEP]
obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
[GOAL]
case pos.refl.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map (𝟙 i) ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map (𝟙 i)
[PROOFSTEP]
simp
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj k = F.obj k) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
cases h
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
haveI : IsIso (F.map f) := (H _ h_1).isIso_from _
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
rw [← IsIso.comp_inv_eq]
[GOAL]
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫ inv (F.map f) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j)
[PROOFSTEP]
apply (H _ h_1).hom_ext
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j) ≫ F.map f
[PROOFSTEP]
cases h_1
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
k : J
h : ¬k = i
f : i ⟶ k
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) ≫ F.map f
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j k : J
f : j ⟶ k
h : ¬k = i
h_1 : ¬j = i
⊢ ((Functor.const J).obj (F.toPrefunctor.1 i)).map f ≫
      IsTerminal.from (H k h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj k) =
    IsTerminal.from (H j h_1) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) ≫ F.map f
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case refine'_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫
      limit.lift F
        { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) } =
    𝟙 (limit F)
[PROOFSTEP]
ext
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
        limit.lift F
          { pt := F.toPrefunctor.1 i,
            π :=
              NatTrans.mk fun j =>
                if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
                else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }) ≫
      limit.π F j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
rw [assoc, limit.lift_π]
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ limit.π F i ≫
      NatTrans.app
        { pt := F.toPrefunctor.1 i,
            π :=
              NatTrans.mk fun j =>
                if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
                else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }.π
        j✝ =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_3.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
⊢ (limit.π F i ≫
      if h : j✝ = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝ = F.obj j✝)
      else IsTerminal.from (H j✝ h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝)) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : j✝ = i
⊢ limit.π F i ≫ eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝ = F.obj j✝) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj i = F.obj i) = 𝟙 (limit F) ≫ limit.π F i
[PROOFSTEP]
rw [id_comp, eqToHom_refl]
[GOAL]
case pos.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.π F i ≫ 𝟙 (((Functor.const J).obj (F.toPrefunctor.1 i)).obj i) = limit.π F i
[PROOFSTEP]
exact comp_id _
[GOAL]
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j✝ : J
h : ¬j✝ = i
⊢ limit.π F i ≫ IsTerminal.from (H j✝ h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j✝) =
    𝟙 (limit F) ≫ limit.π F j✝
[PROOFSTEP]
apply (H _ h).hom_ext
[GOAL]
case refine'_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ limit.lift F
        { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) } ≫
      limit.π F i =
    𝟙 (F.obj i)
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case refine'_4
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
I : C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ NatTrans.app
      { pt := F.toPrefunctor.1 i,
          π :=
            NatTrans.mk fun j =>
              if h : j = i then eqToHom (_ : ((Functor.const J).obj (F.toPrefunctor.1 i)).obj j = F.obj j)
              else IsTerminal.from (H j h) (((Functor.const J).obj (F.toPrefunctor.1 i)).obj j) }.π
      i =
    𝟙 (F.obj i)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (IsTerminal.from hI' I ≫ f)
⊢ (inv (IsTerminal.from hI' I ≫ f) ≫ IsTerminal.from hI' I) ≫ f = 𝟙 A
[PROOFSTEP]
rw [assoc, IsIso.inv_hom_id]
