Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.refine_3.none
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
      none =
    (w.cocone.ι ≫ (Functor.const WalkingSpan).map αZ).app none

pp: case mpr.refine_3.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)

pp: case mpr.refine_3.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:
· simp [hh.w, hf.w_assoc]

Goal state after:
case mpr.refine_3.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.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)