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 : 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))
⊢ {
        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.right) ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingSpan) (PushoutCocone.mk h i sorry).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 := sorry } ≫
      (PushoutCocone.mk h i sorry).ι)
    (some WalkingPair.right))
  ((w.cocone.ι ≫ Functor.map (Functor.const WalkingSpan) αZ).app (some WalkingPair.right))
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_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 ((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))
have 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))
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_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 ((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))
have 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))
Tactic: simp_rw [Functor.map_id]
-- 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.{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))
have 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)
Tactic: rw [Category.comp_id, Category.id_comp]
-- 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
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)
⊢ 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))
have 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)
Tactic: rw [Category.comp_id, Category.id_comp]
-- 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'
⊢ (∀ (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
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: 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 : 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
⊢ (∀ (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
have 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 := sorry }
        j)
      αZ ((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 : 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'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (P := (span f' g').obj none) (w.cocone.ι.app 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 := ⋯ }
      none)
    αZ ((PushoutCocone.mk h i ⋯).ι.app none)
have mpr : IsPullback (w.cocone.ι.app none) αW αZ (f ≫ h)
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'
h₁ : IsPullback h' αX αZ h
h₂ : IsPullback i' αY αZ i
⊢ IsPullback (w.cocone.ι.app none) αW αZ (f ≫ h)
have mpr : IsPullback (f' ≫ w.cocone.inl) αW αZ (f ≫ h)
Tactic: rw [PushoutCocone.condition_zero]
-- 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 : IsPushout f g h i
⊢ H.IsVanKampen ↔
    ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
      CommSq h' αX αZ h →
        CommSq i' αY αZ i →
          ∀ [HasPullback αX f],
            IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
              ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
                IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
have mp : H.IsVanKampen →
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
              IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' 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 : IsPushout f g h i
mp :
  H.IsVanKampen →
    ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
      CommSq h' αX αZ h →
        CommSq i' αY αZ i →
          ∀ [HasPullback αX f],
            IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
              ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
                IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
⊢ H.IsVanKampen ↔
    ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
      CommSq h' αX αZ h →
        CommSq i' αY αZ i →
          ∀ [HasPullback αX f],
            IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
              ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
                IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
have mpr : (∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
              IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i') →
  H.IsVanKampen
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 : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst_1 : HasPullback αX f
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
    ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
      IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
have mp : IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
  ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
    IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' 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 : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst_1 : HasPullback αX f
mp :
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
      IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
    ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
      IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
have mp₁ : (∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
    IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i') →
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ 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 : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
              IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' 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
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have mpr : IsPushout f' g' h' i' → IsPullback h' αX αZ h ∧ IsPullback i' αY αZ 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 : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
              IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' 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
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
mpr : IsPushout f' g' h' i' → 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
have mpr₁ : IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i → IsPushout f' g' h' 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 : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
              IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' 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
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := ⋯
H'' : IsPushout f' g' h' i'
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have mpr : ∃ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W),
  IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Tactic: rw [H' h' i' αX αY αZ sq_h sq_i]