awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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'
mpr :
  Eq (α :=
    (span f' g').obj none ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt) none)
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      none)
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app none)
mpr₁ :
  Eq (α :=
    (span f' g').obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt)
        (some WalkingPair.left))
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      (some WalkingPair.left))
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.left))
mpr₂ :
  Eq (α :=
    (span f' g').obj (some WalkingPair.right) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt)
        (some WalkingPair.right))
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      (some WalkingPair.right))
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.right))
⊢ {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ } ≫
      (PushoutCocone.mk h i ⋯).ι =
    w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ

Tactic:
ext (_ | _ | _)
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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'
⊢ Eq (α :=
    (span f' g').obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt)
        (some WalkingPair.left))
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      (some WalkingPair.left))
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.left))

Tactic:
hh.w.symm

Premises used: CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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'
⊢ Eq (α :=
    (span f' g').obj (some WalkingPair.right) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt)
        (some WalkingPair.right))
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      (some WalkingPair.right))
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.right))

Tactic:
hi.w.symm

Premises used: CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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'
⊢ Eq (α :=
    (span f' g').obj (some WalkingPair.left) ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i ⋯).pt)
        (some WalkingPair.left))
    (NatTrans.app
      ({
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ } ≫
        (PushoutCocone.mk h i ⋯).ι)
      (some WalkingPair.left))
    ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.left))

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

Premises used: CategoryTheory.CommSq.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i_1 : Y ⟶ Z
H_1 : IsPushout f g h i_1
H : IsVanKampenColimit (PushoutCocone.mk h i_1 ⋯)
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_1
w : CommSq f' g' h' i'
i : WalkingSpan
mpr :
  IsPullback ((span f' g').map (𝟙 i))
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    ((span f g).map (𝟙 i))
⊢ IsPullback ((span f' g').map (WidePushoutShape.Hom.id i))
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      i)
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      i)
    ((span f g).map (WidePushoutShape.Hom.id i))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i_1 : Y ⟶ Z
H_1 : IsPushout f g h i_1
H : IsVanKampenColimit (PushoutCocone.mk h i_1 ⋯)
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_1
w : CommSq f' g' h' i'
i : WalkingSpan
mpr :
  IsPullback.{v, u} (𝟙 ((span f' g').obj i))
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (𝟙 ((span f g).obj i))
⊢ IsPullback ((span f' g').map (𝟙 i))
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    ((span f g).map (𝟙 i))

Tactic:
simp_rw [Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i_1 : Y ⟶ Z
H_1 : IsPushout f g h i_1
H : IsVanKampenColimit (PushoutCocone.mk h i_1 ⋯)
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_1
w : CommSq f' g' h' i'
i : WalkingSpan
rw :
  Eq.{v + 1} (α := (span f' g').obj i ⟶ (span f g).obj i)
    (𝟙 ((span f' g').obj i) ≫
      Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
        (fun (val : WalkingPair) ↦
          WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
            val)
        i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
rw₁ rw₂ :
  Eq.{v + 1} (α := (span f' g').obj i ⟶ (span f g).obj i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
        (fun (val : WalkingPair) ↦
          WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
            val)
        i :
      (span f' g').obj i ⟶ (span f g).obj i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
        (fun (val : WalkingPair) ↦
          WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
            val)
        i :
      (span f' g').obj i ⟶ (span f g).obj i)
⊢ Eq.{v + 1} (α := (span f' g').obj i ⟶ (span f g).obj i)
    (𝟙 ((span f' g').obj i) ≫
      Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
        (fun (val : WalkingPair) ↦
          WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
            val)
        i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
        (fun (val : WalkingPair) ↦
          WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
            val)
        i ≫
      𝟙 ((span f g).obj i))

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i_1 : Y ⟶ Z
H_1 : IsPushout f g h i_1
H : IsVanKampenColimit (PushoutCocone.mk h i_1 ⋯)
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_1
w : CommSq f' g' h' i'
i : WalkingSpan
⊢ IsPullback.{v, u} (𝟙 ((span f' g').obj i))
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (Option.rec (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) αW
      (fun (val : WalkingPair) ↦
        WalkingPair.rec (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x)) αX αY
          val)
      i)
    (𝟙 ((span f g).obj i))

Tactic:
exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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))
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      none)
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

Tactic:
hf
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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))
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      none)
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      (some WalkingPair.right))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.right))

Tactic:
hg
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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))
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      none)
    (NatTrans.app
      {
        app := fun (X_1 : WalkingSpan) ↦
          Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
            fun (val : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ (span f' g').obj (some x) ⟶ (span f g).obj (some x))
              val αX αY,
        naturality := ⋯ }
      (some WalkingPair.left))
    ((span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

Tactic:
exacts [hf, hg]
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
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_1 : 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'
mpr :
  (∀ (j : WalkingSpan),
      IsPullback (w.cocone.ι.app j)
        (NatTrans.app
          {
            app := fun (X_1 : WalkingSpan) ↦
              Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
                fun (val : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
            naturality := ⋯ }
          j)
        αZ ((PushoutCocone.mk h i ⋯).ι.app j)) →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
mpr₁ :
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    ∀ (j : WalkingSpan),
      IsPullback (w.cocone.ι.app j)
        (NatTrans.app
          {
            app := fun (X_1 : WalkingSpan) ↦
              Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
                fun (val : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
            naturality := ⋯ }
          j)
        αZ ((PushoutCocone.mk h i ⋯).ι.app j)
⊢ (∀ (j : WalkingSpan),
      IsPullback (w.cocone.ι.app j)
        (NatTrans.app
          {
            app := fun (X_1 : WalkingSpan) ↦
              Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
                fun (val : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
            naturality := ⋯ }
          j)
        αZ ((PushoutCocone.mk h i ⋯).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h_1 : X ⟶ Z
i : Y ⟶ Z
H_1 : IsPushout f g h_1 i
H : IsVanKampenColimit (PushoutCocone.mk h_1 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_1
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h :
  ∀ (j : WalkingSpan),
    IsPullback (w.cocone.ι.app j)
      (NatTrans.app
        {
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ }
        j)
      αZ ((PushoutCocone.mk h_1 i ⋯).ι.app j)
⊢ IsPullback h' αX αZ h_1 ∧ IsPullback i' αY αZ i

Tactic:
⟨h WalkingCospan.left, h WalkingCospan.right⟩

Premises used: CategoryTheory.Limits.WalkingCospan.right, And.intro, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h_1 : X ⟶ Z
i : Y ⟶ Z
H_1 : IsPushout f g h_1 i
H : IsVanKampenColimit (PushoutCocone.mk h_1 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_1
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
h :
  ∀ (j : WalkingSpan),
    IsPullback (w.cocone.ι.app j)
      (NatTrans.app
        {
          app := fun (X_1 : WalkingSpan) ↦
            Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) X_1 αW
              fun (val : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                (span f' g').obj (some x) ⟶ (span f g).obj (some x)) val αX αY,
          naturality := ⋯ }
        j)
      αZ ((PushoutCocone.mk h_1 i ⋯).ι.app j)
⊢ IsPullback h' αX αZ h_1 ∧ IsPullback i' αY αZ i

Tactic:
exact ⟨h WalkingCospan.left, h WalkingCospan.right⟩