awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
mp :
  Nonempty (IsColimit (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this)) ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
⊢ Nonempty (IsColimit c') ↔
    IsPushout (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
      (c'.ι.app WalkingSpan.right)
have rw : (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
  PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
Tactic: rw [(IsColimit.equivOfNatIsoOfIso (diagramIsoSpan F') c' (PushoutCocone.mk _ _ this)
            _).nonempty_congr]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ (Cocone.precompose (diagramIsoSpan F').inv).obj c' ≅
    PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this
have refine : ∀ (j : WalkingSpan),
  ((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ Iso.hom (Iso.refl c'.pt) =
    (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j
Tactic: refine Cocone.ext (Iso.refl c'.pt) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj none ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app none ≫ Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app none)
have none : (𝟙 (F'.obj none) ≫ c'.ι.app none) ≫ 𝟙 c'.pt = F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj (some WalkingPair.left) ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app (some WalkingPair.left) ≫ Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app (some WalkingPair.left))
have some : (𝟙 (F'.obj (some WalkingPair.left)) ≫ c'.ι.app (some WalkingPair.left)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.left
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ Eq (α :=
    (span (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd)).obj (some WalkingPair.right) ⟶
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).pt)
    (((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app (some WalkingPair.right) ≫ Iso.hom (Iso.refl c'.pt))
    ((PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app (some WalkingPair.right))
have some : (𝟙 (F'.obj (some WalkingPair.right)) ≫ c'.ι.app (some WalkingPair.right)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.right
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 α
⊢ 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)
have 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 sorry).ι.app j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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)
⊢ 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)
have mp₁ : (∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i sorry).ι.app j)) →
  IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
    IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 none) (c'.ι.app none) (α.app none) fα ((PushoutCocone.mk h i ⋯).ι.app none)
have mp : IsPullback (F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left) (α.app none) fα
  ((PushoutCocone.mk h i sorry).ι.app none)
Tactic: rw [← c'.w WalkingSpan.Hom.fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have mpr : IsPushout f' g' h' i' ↔ Nonempty (IsColimit w.cocone)
Tactic: refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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)
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have 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)
Tactic: refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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)
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have 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 := sorry } ≫
    (PushoutCocone.mk h i sorry).ι =
  w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ
Tactic: refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have 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 := sorry }
Tactic: refine
      Iff.trans ?_ ((H w.cocone ⟨by rintro (_ | _ | _); exacts [αW, αX, αY], ?_⟩ αZ ?_ ?_).trans ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 := ⋯ }
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have 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 := sorry }
        j)
      αZ ((PushoutCocone.mk h i sorry).ι.app j)) ↔
  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 ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 (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))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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'
⊢ {
        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
have mpr : Eq (α :=
  (span f' g').obj none ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i sorry).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 := sorry } ≫
      (PushoutCocone.mk h i sorry).ι)
    none)
  ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app none)
Tactic: ext (_ | _ | _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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)
⊢ {
        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
have mpr₁ : Eq (α :=
  (span f' g').obj (some WalkingPair.left) ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i sorry).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 := sorry } ≫
      (PushoutCocone.mk h i sorry).ι)
    (some WalkingPair.left))
  ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.left))
Tactic: ext (_ | _ | _)