-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K)
    {F : K ⥤ C} {c : Cocone F} (hc : IsUniversalColimit c) :
    IsUniversalColimit (c.whisker e.functor)

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
⊢ IsUniversalColimit (Cocone.whisker e.functor c)

Tactic:
intro F' c' α f e' hα H

Result:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ Nonempty (IsColimit c')

Proof state:
case a
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
⊢ Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr

Result:
no goals

Proof state:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)

Tactic:
rw [← Category.comp_id f]

Result:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app k)
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)

Proof state:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app k)
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)

Tactic:
refine (H (e.inverse.obj k)).paste_vert ?_

Result:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.functor c).ι.app (e.inverse.obj k)) ((e.invFunIdAssoc F).hom.app k)
    (𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
this : IsIso (𝟙 (Cocone.whisker e.functor c).pt)
⊢ (Cocone.whisker e.functor c).ι.app (e.inverse.obj k) ≫ 𝟙 (Cocone.whisker e.functor c).pt =
    (e.invFunIdAssoc F).hom.app k ≫ c.ι.app k

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.w.h
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
e_1✝ :
  (e.inverse ⋙ F' ⟶ (Functor.const K).obj c.pt) =
    (e.inverse ⋙ F' ⟶ e.inverse ⋙ (Functor.const J).obj (Cocone.whisker e.functor c).pt)
x✝ : K
⊢ ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app x✝ =
    (whiskerLeft e.inverse (α ≫ (Cocone.whisker e.functor c).ι)).app x✝

Tactic:
simp

Result:
no goals

Proof state:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
this : IsIso (𝟙 (Cocone.whisker e.functor c).pt)
⊢ IsPullback ((Cocone.whisker e.functor c).ι.app (e.inverse.obj k)) ((e.invFunIdAssoc F).hom.app k)
    (𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)

Tactic:
exact IsPullback.of_vert_isIso ⟨by simp⟩

Result:
no goals