awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  H.cocone.inl ≫ m =
    H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
mpr₁ :
  H.cocone.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
⊢ m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) =
    H.cocone.inl ≫ m
⊢ H.cocone.inl ≫ m =
    H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) =
    H.cocone.inl ≫ m

Tactic:
(H.isColimit.fac _ WalkingSpan.left).trans e₂.symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair, CategoryTheory.IsPushout.isColimit, Eq.symm, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape, Eq.trans
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) =
    H.cocone.inl ≫ m

Tactic:
exact (H.isColimit.fac _ WalkingSpan.left).trans e₂.symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.IsPushout.isColimit, Eq.trans
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  H.cocone.inr ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
⊢ H.cocone.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
rw [H.isColimit.fac _ WalkingSpan.right]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.right, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
mpr₁ :
  c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
⊢ H.cocone.inr ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right

Tactic:
apply BinaryCofan.IsColimit.hom_ext hc

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr : c.inl ≫ H.cocone.inr ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
⊢ c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right

Tactic:
erw [hc.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr : f ≫ iY ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
⊢ c.inl ≫ H.cocone.inr ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Tactic:
erw [← H.w_assoc]

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr : f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
⊢ f ≫ iY ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Tactic:
rw [e₂]
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right

Tactic:
((Category.assoc _ _ _).symm.trans e₁).trans ?_

Premises used: CategoryTheory.Category.assoc, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  s.inl =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right

Tactic:
refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_

Premises used: CategoryTheory.Category.assoc, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl
⊢ s.inl =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl

Tactic:
hc.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E Y YE : C
c : BinaryCofan.{v, u} X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl

Tactic:
exact hc.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac
-- 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
obtain : ∀ (hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)), H.IsVanKampen
⊢ H.IsVanKampen

Tactic:
obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H

Premises used: Iff.mpr, CategoryTheory.is_coprod_iff_isPushout, CategoryTheory.IsPushout.toCommSq
-- 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'
obtain :
  ∀ (hc₂ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk g' (pullback.fst αY c.inr))),
    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

Tactic:
obtain ⟨hc₂⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
    (BinaryCofan.mk _ (pullback.fst _ _)) _ _ _ hg.w.symm pullback.condition.symm).mpr
    ⟨hg, IsPullback.of_hasPullback αY c.inr⟩

Premises used: Iff.mpr, CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.BinaryCofan.isVanKampen_iff, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.BinaryCofan.mk, And.intro, CategoryTheory.Limits.pullback.fst, CategoryTheory.IsPullback.of_hasPullback, Iff.mp, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, CategoryTheory.Limits.pullback.condition, Eq.symm
-- 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))
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
(is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_

Premises used: CategoryTheory.is_coprod_iff_isPushout, Iff.trans, Iff.symm
-- 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))
refine :
  Nonempty
      (IsColimit (F :=
        pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
          X')
        (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
    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 (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_

Premises used: CategoryTheory.is_coprod_iff_isPushout, Iff.trans, Iff.symm
-- 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))
⊢ Nonempty
      (IsColimit (F :=
        pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
          X')
        (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_

Premises used: CategoryTheory.BinaryCofan.isVanKampen_iff, CategoryTheory.Limits.pullback.snd, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.limit, CategoryTheory.Limits.BinaryCofan.mk, Iff.mp, Iff.trans, CategoryTheory.CommSq.w, Eq.symm
-- 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))
refine_1 :
  Eq (α :=
    pullback αY c.inr ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryCofan.mk (c.inr ≫ i) h).pt)
        { as := WalkingPair.left : Discrete WalkingPair })
    (pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl)
    (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h') ≫ αZ)
refine_2 :
  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 ∧
      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 ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
⊢ Nonempty
      (IsColimit (F :=
        pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
          X')
        (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
refine ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_

Premises used: CategoryTheory.BinaryCofan.isVanKampen_iff, CategoryTheory.Limits.pullback.snd, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.BinaryCofan.mk, Iff.mp, Iff.trans, CategoryTheory.CommSq.w, Eq.symm
-- 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))
refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
⊢ Eq (α :=
    pullback αY c.inr ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryCofan.mk (c.inr ≫ i) h).pt)
        { as := WalkingPair.left : Discrete WalkingPair })
    (pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl)
    (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h') ≫ αZ)

Tactic:
dsimp
-- 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))
refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
refine_1₁ : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) (pullback.fst αY c.inr ≫ i' ≫ αZ)
refine_1₂ refine_1₃ : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) (pullback.fst αY c.inr ≫ αY ≫ i)
⊢ Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)

Tactic:
rw [← pullback.condition_assoc, Category.assoc, hi.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.CommSq.w