-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem hasStrictInitial_of_isUniversal [HasInitial C]
    (H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))) : HasStrictInitialObjects C :=
  hasStrictInitialObjects_of_initial_is_strict
    (by
      intro A f
      suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A)) by
        obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
        rcases(Category.id_comp _).symm.trans h₂ with rfl
        exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
      refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> simp)
        (mapPair_equifibered _) ?_).some
      rintro ⟨⟨⟩⟩ <;> dsimp <;>
        exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι.app j) ((mapPair f f).app j) f
      ((BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι.app j)

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp <;>
  exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

Result:
no goals

Proof state:
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inl ≫ 𝟙 A = f ≫ initial.to A
h₂ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inr ≫ 𝟙 A = 𝟙 A
⊢ IsIso f

Tactic:
exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))

Tactic:
refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> simp)
  (mapPair_equifibered _) ?_).some

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (𝟙 A) (𝟙 A)).ι.app j) ((mapPair f f).app j) f
      ((BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι.app j)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsIso f

Tactic:
suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A)) by
  obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
  rcases(Category.id_comp _).symm.trans h₂ with rfl
  exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
⊢ IsIso f

Tactic:
obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)

Result:
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : (BinaryCofan.mk (𝟙 A) (𝟙 A)).pt ⟶ A
h₁ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inl ≫ l = f ≫ initial.to A
h₂ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inr ≫ l = 𝟙 A
⊢ IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ mapPair f f ≫ (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C))).ι =
    (BinaryCofan.mk (𝟙 A) (𝟙 A)).ι ≫ (Functor.const (Discrete WalkingPair)).map f

Tactic:
ext ⟨⟨⟩⟩ <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
⊢ ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f

Tactic:
intro A f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsIso f

Proof state:
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
l : (BinaryCofan.mk (𝟙 A) (𝟙 A)).pt ⟶ A
h₁ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inl ≫ l = f ≫ initial.to A
h₂ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inr ≫ l = 𝟙 A
⊢ IsIso f

Tactic:
rcases(Category.id_comp _).symm.trans h₂ with rfl

Result:
case mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
this : IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inl ≫ 𝟙 A = f ≫ initial.to A
h₂ : (BinaryCofan.mk (𝟙 A) (𝟙 A)).inr ≫ 𝟙 A = 𝟙 A
⊢ IsIso f