-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.mapCocone_iff (G : C ⥤ D) {F : J ⥤ C} {c : Cocone F}
    [G.IsEquivalence] : IsVanKampenColimit (G.mapCocone c) ↔ IsVanKampenColimit c :=
  ⟨IsVanKampenColimit.of_mapCocone G, fun hc ↦ by
    let e : F ⋙ G ⋙ Functor.inv G ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
    apply IsVanKampenColimit.of_mapCocone G.inv
    apply (IsVanKampenColimit.precompose_isIso_iff e.inv).mp
    exact hc.of_iso (Cocones.ext (G.asEquivalence.unitIso.app c.pt) (fun j => (by simp [e])))⟩

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit ((Cocones.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))

Tactic:
exact hc.of_iso (Cocones.ext (G.asEquivalence.unitIso.app c.pt) (fun j => (by simp [e])))

Result:
no goals

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.mapCocone c)

Tactic:
apply IsVanKampenColimit.of_mapCocone G.inv

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))

Tactic:
apply (IsVanKampenColimit.precompose_isIso_iff e.inv).mp

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit ((Cocones.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
⊢ IsVanKampenColimit (G.mapCocone c)

Tactic:
let e : F ⋙ G ⋙ Functor.inv G ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm

Result:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.mapCocone c)

Proof state:
J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_2
inst✝¹ : Category.{u_3, u_2} D
G : C ⥤ D
F : J ⥤ C
c : Cocone F
inst✝ : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
j : J
⊢ c.ι.app j ≫ (G.asEquivalence.unitIso.app c.pt).hom =
    ((Cocones.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c))).ι.app j

Tactic:
simp [e]

Result:
no goals