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 : 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 := ⋯
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ (g'' ≫ Iso.hom (Iso.refl Y')) ≫ i' = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ i'

Tactic:
simp [← cs.w, hP.w]

Premises used: CategoryTheory.IsPushout.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 : 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 := ⋯
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ (g'' ≫ Iso.hom (Iso.refl Y')) ≫ αY = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ αY

Tactic:
simp [hg.w, 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_1 X Y Z : C
f : W_1 ⟶ X
g : W_1 ⟶ 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
inst_1 : HasPullback αX f
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
W : C
f₁ f₂ : Z' ⟶ W
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
h'_w : h' ≫ f₁ = h' ≫ f₂
i'_w : i' ≫ f₁ = i' ≫ f₂
obtain :
  ∀ (W' : C) (f' : W' ⟶ X') (g' : W' ⟶ Y') (αW : W' ⟶ W_1),
    IsPullback f' αW αX f → IsPullback g' αW αY g → ∀ (H'' : IsPushout f' g' h' i'), f₁ = f₂
⊢ f₁ = f₂

Tactic:
obtain ⟨W', f', g', αW, _, _, H''⟩ := H'.exists_cube_filling hh hi

Premises used: CategoryTheory.IsPushout.IsVanKampen.exists_cube_filling
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : W_1 ⟶ X
g : W_1 ⟶ 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
inst_1 : HasPullback αX f
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
W : C
f₁ f₂ : Z' ⟶ W
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
h'_w : h' ≫ f₁ = h' ≫ f₂
i'_w : i' ≫ f₁ = i' ≫ f₂
W' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
αW : W' ⟶ W_1
left : IsPullback f' αW αX f
left_1 : IsPullback g' αW αY g
H'' : IsPushout f' g' h' i'
⊢ f₁ = f₂

Tactic:
H''.hom_ext h'_w i'_w

Premises used: CategoryTheory.IsPushout.hom_ext
-- Module: Mathlib.CategoryTheory.Adhesive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X Y Z : C
f : W_1 ⟶ X
g : W_1 ⟶ 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
inst_1 : HasPullback αX f
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
W : C
f₁ f₂ : Z' ⟶ W
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
h'_w : h' ≫ f₁ = h' ≫ f₂
i'_w : i' ≫ f₁ = i' ≫ f₂
W' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
αW : W' ⟶ W_1
left : IsPullback f' αW αX f
left_1 : IsPullback g' αW αY g
H'' : IsPushout f' g' h' i'
⊢ f₁ = f₂

Tactic:
exact H''.hom_ext h'_w i'_w

Premises used: CategoryTheory.IsPushout.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 : CommSq f c.inl iY fE
mp : Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE
mpr : IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE

Tactic:
constructor
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
⊢ IsPushout f c.inl iY fE

Tactic:
⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ ?_⟩⟩

Premises used: CategoryTheory.IsPushout.mk, Nonempty.intro, CategoryTheory.Limits.PushoutCocone.isColimitAux'
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
mp :
  (s : PushoutCocone f c.inl) →
    { l : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt //
      (PushoutCocone.mk iY fE ⋯).inl ≫ l = s.inl ∧
        (PushoutCocone.mk iY fE ⋯).inr ≫ l = s.inr ∧
          ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
            (PushoutCocone.mk iY fE ⋯).inl ≫ m = s.inl → (PushoutCocone.mk iY fE ⋯).inr ≫ m = s.inr → m = l }
⊢ IsPushout f c.inl iY fE

Tactic:
refine ⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ ?_⟩⟩
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : { l : YE ⟶ s.pt // iY ≫ l = s.inl ∧ fE ≫ l = s.inr ∧ ∀ {m : YE ⟶ s.pt}, iY ≫ m = s.inl → fE ≫ m = s.inr → m = l }
⊢ { l : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt //
    (PushoutCocone.mk iY fE ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk iY fE ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk iY fE ⋯).inl ≫ m = s.inl → (PushoutCocone.mk iY fE ⋯).inr ≫ m = s.inr → m = l }

Tactic:
dsimp
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr
mp₁ : ∀ {m : YE ⟶ s.pt}, iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
⊢ { l : YE ⟶ s.pt // iY ≫ l = s.inl ∧ fE ≫ l = s.inr ∧ ∀ {m : YE ⟶ s.pt}, iY ≫ m = s.inl → fE ≫ m = s.inr → m = l }

Tactic:
refine ⟨BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl,
        BinaryCofan.IsColimit.inr_desc h _ _, ?_, ?_⟩
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : c.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
mp₁ : c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr

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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : f ≫ iY ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
⊢ c.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr

Tactic:
rw [← H.w_assoc]

Premises used: 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : f ≫ (BinaryCofan.mk (c.inr ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = c.inl ≫ s.inr
⊢ f ≫ iY ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr

Tactic:
erw [h.fac _ ⟨WalkingPair.right⟩]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ f ≫ (BinaryCofan.mk (c.inr ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = c.inl ≫ s.inr

Tactic:
s.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ f ≫ (BinaryCofan.mk (c.inr ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = c.inl ≫ s.inr

Tactic:
exact s.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
mp : (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
⊢ c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
h.fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
exact h.fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
mp :
  (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
mp₁ :
  (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
⊢ m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
apply BinaryCofan.IsColimit.hom_ext h

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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
mp : (c.inr ≫ fE) ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
dsimp
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
mp : (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
⊢ (c.inr ≫ fE) ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
rw [Category.assoc, e₂, eq_comm]

Premises used: CategoryTheory.Category.assoc, eq_comm
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
h.fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr

Tactic:
exact h.fac _ ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
e₁.trans (Eq.symm ?_)

Premises used: 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
mp : (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inl
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

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

Premises used: 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inl

Tactic:
h.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Discrete.functor, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- 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 : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : YE ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inl

Tactic:
exact h.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 : CommSq f c.inl iY fE
⊢ IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))

Tactic:
fun H => ⟨?_⟩

Premises used: Nonempty.intro
-- 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 : CommSq f c.inl iY fE
mpr : (H : IsPushout f c.inl iY fE) → IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
⊢ IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))

Tactic:
refine fun H => ⟨?_⟩
-- 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
mpr :
  (s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y) →
    YE ⟶ s.pt
mpr₁ :
  ∀ (s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y),
    (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl
mpr₂ :
  ∀ (s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y),
    iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr
mpr₃ :
  ∀ (s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y)
    (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl →
      iY ≫ m = s.inr → m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)

Tactic:
fapply Limits.BinaryCofan.isColimitMk

Premises used: CategoryTheory.Limits.BinaryCofan.isColimitMk
-- 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) →
    YE ⟶ s.pt

Tactic:
exact fun s => H.isColimit.desc (PushoutCocone.mk s.inr _ <|
        (hc.fac (BinaryCofan.mk (f ≫ s.inr) s.inl) ⟨WalkingPair.left⟩).symm)

Premises used: CategoryTheory.Limits.IsColimit.desc, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.PushoutCocone.mk
-- 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
mpr : c.inr ≫ fE ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl
⊢ (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.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
mpr :
  c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl
⊢ c.inr ≫ fE ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl

Tactic:
erw [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
mpr : (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = s.inl
⊢ c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl

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
⊢ (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = s.inl

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
⊢ iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr

Tactic:
H.isColimit.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair, CategoryTheory.IsPushout.isColimit, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- 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
⊢ iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr

Tactic:
exact H.isColimit.fac _ WalkingSpan.left

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.IsPushout.isColimit