-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem isVanKampenColimit_of_isEmpty [HasStrictInitialObjects C] [IsEmpty J] {F : J ⥤ C}
    (c : Cocone F) (hc : IsColimit c) : IsVanKampenColimit c

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit (asEmptyCocone c.pt)
⊢ IsVanKampenColimit (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c)

Tactic:
exact (this.precompose_isIso (Functor.uniqueFromEmpty
  ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F)).hom).of_iso
  (Cocones.ext (Iso.refl _) (by simp))

Result:
no goals

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsInitial c.pt
⊢ IsVanKampenColimit c

Tactic:
replace this := IsInitial.isVanKampenColimit this

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit (asEmptyCocone c.pt)
⊢ IsVanKampenColimit c

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit (asEmptyCocone c.pt)
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.whiskerEquivalence_iff
  (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)).mp

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit (asEmptyCocone c.pt)
⊢ IsVanKampenColimit (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c)

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this :
  IsColimit
    ((Cocones.precompose ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F).uniqueFromEmpty.inv).obj
      (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c))
⊢ IsInitial c.pt

Tactic:
exact IsColimit.ofIsoColimit this (Cocones.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))

Result:
no goals

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
have : IsInitial c.pt := by
  have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
    (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
  exact IsColimit.ofIsoColimit this (Cocones.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsInitial c.pt
⊢ IsVanKampenColimit c

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit (asEmptyCocone c.pt)
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((Cocones.precompose ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F).uniqueFromEmpty.hom).obj
                (asEmptyCocone c.pt)).ι.app
          j ≫
        (Iso.refl
            ((Cocones.precompose ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F).uniqueFromEmpty.hom).obj
                (asEmptyCocone c.pt)).pt).hom =
      (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c).ι.app j

Tactic:
simp

Result:
no goals

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsInitial c.pt

Tactic:
have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
  (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasStrictInitialObjects C
inst✝ : IsEmpty J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this :
  IsColimit
    ((Cocones.precompose ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F).uniqueFromEmpty.inv).obj
      (Cocone.whisker (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor c))
⊢ IsInitial c.pt