-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsUniversalColimit.map_reflective
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    {F : J ⥤ D} {c : Cocone (F ⋙ Gr)}
    (H : IsUniversalColimit c)
    [∀ X (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)]
    [∀ X (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl] :
    IsUniversalColimit (Gl.mapCocone c)

Proof state:
case refine_3.h₀
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.156042, ?u.156041, u_3, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
j : J
⊢ (adj.counit.app (F'.obj j) ≫ 𝟙 (F'.obj j)) ≫ c'.ι.app j = adj.counit.app (F'.obj j) ≫ c'.ι.app j

Tactic:
rw [Category.comp_id]

Result:
no goals

Proof state:
case refine_1
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.156042, ?u.156041, u_3, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
⊢ ((Cocones.precompose β.hom).obj c').pt ⟶ Gl.obj (Gr.obj c'.pt)

Tactic:
exact inv <| adj.counit.app c'.pt

Result:
no goals

Proof state:
case refine_3
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝⁴ : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr
this✝³ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))
this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' :=
  {
    hom :=
      pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv,
    w := ⋯ }
this✝ :
  cf.hom ≫
      (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫
        pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt =
    𝟙 ((Cocones.precompose β.hom).obj c').pt
this : IsIso cf
Hc'' : IsColimit c''
⊢ Nonempty (IsColimit c')

Tactic:
exact ⟨IsColimit.precomposeHomEquiv β c' <|
  (isColimitOfPreserves Gl Hc'').ofIsoColimit (asIso cf).symm⟩

Result:
no goals

Proof state:
case refine_2
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
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.156042, ?u.156041, u_3, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
⊢ inv (adj.counit.app c'.pt) ≫ Gl.map (Gr.map f) = f ≫ Gl.map (adj.unit.app c.pt)

Tactic:
simp [← cancel_mono (adj.counit.app <| Gl.obj c.pt)]

Result:
no goals