-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W E X Z : C
c : BinaryCofan.{v, u} W E
inst_1 : FinitaryExtensive.{v, u} C
inst_2 : HasPullbacks.{v, u} C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (P :=
    Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
    (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
    (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) αX
    αZ (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ :
  Eq (α := pullback αY c.inr ⟶ c.pt) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
left :
  IsPullback (X :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) αW (pullback.snd αZ i) c.inl
right :
  IsPullback (P :=
    Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair }) (X :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) (pullback.snd αY c.inr)
    (pullback.snd αZ i) c.inr
⊢ IsPullback (X :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) αW (pullback.snd αZ i) c.inl ∧
    IsPullback (P :=
      Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair }) (X :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) (pullback.snd αY c.inr)
      (pullback.snd αZ i) c.inr

Tactic:
constructor