-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.isVanKampen_iff (H : IsPushout f g h i) :
    H.IsVanKampen ↔ IsVanKampenColimit (PushoutCocone.mk h i H.w)

Proof state:
case mpr.refine_4.id
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.id i))
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app i)
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app i)
    ((span f g).map (WidePushoutShape.Hom.id i))

Tactic:
dsimp

Result:
case mpr.refine_4.id
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback ((span f' g').map (𝟙 i)) (Option.rec αW (fun val => WalkingPair.rec αX αY val) i)
    (Option.rec αW (fun val => WalkingPair.rec αX αY val) i) ((span f g).map (𝟙 i))

Proof state:
case mpr.refine_2.id
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ ((span f' g').map (WidePushoutShape.Hom.id i) ≫ Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn i αW fun val => WalkingPair.casesOn val αX αY) ≫ (span f g).map (WidePushoutShape.Hom.id i)

Tactic:
dsimp

Result:
case mpr.refine_2.id
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i✝ : Y ⟶ Z
H✝ : IsPushout f g h i✝
H : IsVanKampenColimit (PushoutCocone.mk h i✝ ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i✝
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ (span f' g').map (𝟙 i) ≫ Option.rec αW (fun val => WalkingPair.rec αX αY val) i =
    Option.rec αW (fun val => WalkingPair.rec αX αY val) i ≫ (span f g).map (𝟙 i)

Proof state:
case mpr.refine_5.mpr.intro.some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (w.cocone.ι.app (some WalkingPair.left))
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app
      (some WalkingPair.left))
    αZ ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.left))

case mpr.refine_5.mpr.intro.some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (w.cocone.ι.app (some WalkingPair.right))
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app
      (some WalkingPair.right))
    αZ ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.right))

Tactic:
exacts [h₁, h₂]

Result:
no goals