-- Mathlib/CategoryTheory/Adhesive.lean
theorem adhesive_of_reflective [HasPullbacks D] [Adhesive C] [HasPullbacks C] [HasPushouts C]
    [H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g]
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    [PreservesLimitsOfShape WalkingCospan Gl] :
    Adhesive D

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsVanKampenColimit
    ((Cocones.precompose (isoWhiskerLeft (span f g) (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
refine ((this.precompose_isIso (spanCompIso _ _ _).hom).map_reflective adj).of_iso
  (IsColimit.uniqueUpToIso ?_ ?_)

Result:
case refine_1
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    (Gl.mapCocone
      ((Cocones.precompose (spanCompIso Gr f g).hom).obj
        (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))

case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocones.precompose (isoWhiskerLeft (span f g) (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
⊢ Adhesive D

Tactic:
have := adj.rightAdjoint_preservesLimits

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.118037, ?u.118036, v'', v, u'', u} Gr
⊢ Adhesive D

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.118037, ?u.118036, v'', v, u'', u} Gr
⊢ ∀ {W X Y Z : D} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [inst : Mono f] (H : IsPushout f g h i), H.IsVanKampen

Tactic:
intro W X Y Z f g h i _ H

Result:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.118037, ?u.118036, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen

Proof state:
case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsColimit
    ((Cocones.precompose (isoWhiskerLeft (span f g) (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj
      (PushoutCocone.mk h i ⋯))

Tactic:
exact (IsColimit.precomposeHomEquiv _ _).symm H.isColimit

Result:
no goals

Proof state:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : ⋯.IsVanKampen
⊢ H.IsVanKampen

Tactic:
rw [IsPushout.isVanKampen_iff] at this ⊢

Result:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)
⊢ IsVanKampenColimit (PushoutCocone.mk h i ⋯)