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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj (some WalkingPair.left)) ≫ c'.ι.app (some WalkingPair.left)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.left

Tactic:
simp only [c'.w, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.w, 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 : Y ⟶ Z
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj (some WalkingPair.right)) ≫ c'.ι.app (some WalkingPair.right)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.right

Tactic:
simp only [c'.w, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.w, 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 : Y ⟶ Z
H_1 : IsPushout f g h i
H : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h

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

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.NatTrans.congr_app, 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h

Tactic:
exact ⟨NatTrans.congr_app eα.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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

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

Premises used: CategoryTheory.CommSq.mk, CategoryTheory.NatTrans.congr_app, 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ CommSq (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Tactic:
exact ⟨NatTrans.congr_app eα.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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right

Tactic:
simp
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

Tactic:
exact ⟨by simp⟩
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
mp :
  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)
mp₁ :
  (∀ (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
⊢ 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
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
mp :
  IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
    ((PushoutCocone.mk h i ⋯).ι.app none)
⊢ IsPullback (P := F'.obj none) (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i ⋯).ι.app none)

Tactic:
rw [← c'.w WalkingSpan.Hom.fst]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingSpan.Hom.fst
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
    ((PushoutCocone.mk h i ⋯).ι.app none)

Tactic:
(hα WalkingSpan.Hom.fst).paste_horiz h₁

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.fst, CategoryTheory.IsPullback.paste_horiz
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
    ((PushoutCocone.mk h i ⋯).ι.app none)

Tactic:
exact (hα WalkingSpan.Hom.fst).paste_horiz h₁

Premises used: CategoryTheory.Limits.WalkingSpan.Hom.fst, CategoryTheory.IsPullback.paste_horiz
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (P := F'.obj (some WalkingPair.left)) (c'.ι.app (some WalkingPair.left)) (α.app (some WalkingPair.left)) fα
    ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.left))

Tactic:
h₁
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (P := F'.obj (some WalkingPair.right)) (c'.ι.app (some WalkingPair.right)) (α.app (some WalkingPair.right))
    fα ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.right))

Tactic:
h₂
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h₁ : IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h
h₂ : IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
⊢ IsPullback (P := F'.obj (some WalkingPair.left)) (c'.ι.app (some WalkingPair.left)) (α.app (some WalkingPair.left)) fα
    ((PushoutCocone.mk h i ⋯).ι.app (some WalkingPair.left))

Tactic:
exacts [h₁, h₂]
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h_1 i ⋯).pt
eα : α ≫ (PushoutCocone.mk h_1 i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h : ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h_1 i ⋯).ι.app j)
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h_1 ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Tactic:
⟨h _, h _⟩

Premises used: And.intro
-- 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 : H_1.IsVanKampen
F' : Functor.{0, v, 0, u} WalkingSpan C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h_1 i ⋯).pt
eα : α ≫ (PushoutCocone.mk h_1 i ⋯).ι = c'.ι ≫ Functor.map (Functor.const WalkingSpan) fα
hα : NatTrans.Equifibered α
h : ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h_1 i ⋯).ι.app j)
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h_1 ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i

Tactic:
exact ⟨h _, h _⟩
-- 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'
⊢ (span f' g').obj none ⟶ (span f g).obj none

Tactic:
exacts [αW, αX, αY]
-- 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 : IsPushout f' g' h' i' ↔ Nonempty (IsColimit w.cocone)
mpr₁ :
  ∀ ⦃X_1 Y_1 : WalkingSpan⦄ (f_1 : X_1 ⟶ Y_1),
    Eq (α := (span f' g').obj X_1 ⟶ (span f g).obj Y_1)
      ((span f' g').map f_1 ≫
        Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) Y_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)
      ((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) ≫
        (span f g).map f_1)
mpr₂ :
  {
        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
mpr₃ :
  NatTrans.Equifibered.{0, 0, v, u} (J := WalkingSpan) (C := C) (X := span f' g') (Y := span f g)
    {
      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 := ⋯ }
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
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)

Premises used: CategoryTheory.NatTrans.mk, CategoryTheory.CommSq.cocone, Iff.trans
-- 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 :
  Eq (α := (span f' g').obj i ⟶ (span f g).obj i)
    ((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))
⊢ Eq (α := (span f' g').obj i ⟶ (span f g).obj i)
    ((span f' g').map (WidePushoutShape.Hom.id i) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) i α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)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) i α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) ≫
      (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
⊢ Eq (α := (span f' g').obj i ⟶ (span f g).obj i)
    ((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 only [Functor.map_id, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_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 : 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 none ⟶ (span f g).obj (some WalkingPair.left))
    ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) (some WalkingPair.left)
        α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)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) none α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) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

Tactic:
hf.w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- 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 none ⟶ (span f g).obj (some WalkingPair.right))
    ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.right) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) (some WalkingPair.right)
        α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)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) none α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) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.right))

Tactic:
hg.w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- 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 none ⟶ (span f g).obj (some WalkingPair.left))
    ((span f' g').map (WidePushoutShape.Hom.init WalkingPair.left) ≫
      Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) (some WalkingPair.left)
        α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)
    ((Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f' g').obj x ⟶ (span f g).obj x) none α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) ≫
      (span f g).map (WidePushoutShape.Hom.init WalkingPair.left))

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

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w