-- 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:
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').obj 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).obj i)

Tactic:
rw [Category.comp_id, Category.id_comp]

Result:
no goals

Proof state:
case mp.refine_3
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Tactic:
exact ⟨NatTrans.congr_app eα.symm _⟩

Result:
no goals

Proof state:
case mpr.refine_2.init.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'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      Option.casesOn (some WalkingPair.left) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.left)

case mpr.refine_2.init.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'
⊢ ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      Option.casesOn (some WalkingPair.right) αW fun val => WalkingPair.casesOn val αX αY) =
    (Option.casesOn none αW fun val => WalkingPair.casesOn val αX αY) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.right)

Tactic:
exacts [hf.w, hg.w]

Result:
no goals

Proof state:
case mp.refine_5
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)

Tactic:
constructor

Result:
case mp.refine_5.mp
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i →
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)

case mp.refine_5.mpr
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ (∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)) →
    IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Proof state:
case mpr.refine_4.init.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'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left))
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app none)
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app
      (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

case mpr.refine_4.init.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'
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right))
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app none)
    ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ }.app
      (some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))

Tactic:
exacts [hf, hg]

Result:
no goals

Proof state:
case mpr.refine_3.w.h.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'
⊢ ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ } ≫
          (PushoutCocone.mk h i ⋯).ι).app
      (some WalkingPair.left) =
    (w.cocone.ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.left)

case mpr.refine_3.w.h.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'
⊢ ({ app := fun X_1 => Option.casesOn X_1 αW fun val => WalkingPair.casesOn val αX αY, naturality := ⋯ } ≫
          (PushoutCocone.mk h i ⋯).ι).app
      (some WalkingPair.right) =
    (w.cocone.ι ≫ (Functor.const WalkingSpan).map αZ).app (some WalkingPair.right)

Tactic:
exacts [hh.w.symm, hi.w.symm]

Result:
no goals