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 : 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
⊢ IsPushout f' g' h' i'
have mpr : ∀ (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'), IsPushout f' g' h' i'
Tactic: obtain ⟨W'', f'', g'', αW', hf', hg', hP⟩ := (H' h' i' αX αY αZ sq_h sq_i).1 ⟨hh, hi⟩
-- 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 := ⋯
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'
⊢ IsPushout f' g' h' i'
have mpr : g'' ≫ Iso.hom (Iso.refl Y') = (IsPullback.isoIsPullback X' W hf' hf).hom ≫ g'
Tactic: refine hP.of_iso (IsPullback.isoIsPullback _ _ hf' hf)
        (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) ?_ (by simp) (by simp)
-- 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 := ⋯
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') = (IsPullback.isoIsPullback X' W hf' hf).hom ≫ g'
have mpr : (g'' ≫ Iso.hom (Iso.refl Y')) ≫ i' = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ i'
Tactic: apply hi.hom_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 : 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'
mpr : (g'' ≫ Iso.hom (Iso.refl Y')) ≫ i' = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ i'
⊢ g'' ≫ Iso.hom (Iso.refl Y') = (IsPullback.isoIsPullback X' W hf' hf).hom ≫ g'
have mpr₁ : (g'' ≫ Iso.hom (Iso.refl Y')) ≫ αY = ((IsPullback.isoIsPullback X' W hf' hf).hom ≫ g') ≫ αY
Tactic: apply hi.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₂
⊢ f₁ = f₂
have 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₂
Tactic: obtain ⟨W', f', g', αW, _, _, H''⟩ := H'.exists_cube_filling hh hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE
have mp : Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE
have mpr : IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
have mp : (s : PushoutCocone f c.inl) →
  { l : (PushoutCocone.mk iY fE sorry).pt ⟶ s.pt //
    (PushoutCocone.mk iY fE sorry).inl ≫ l = s.inl ∧
      (PushoutCocone.mk iY fE sorry).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk iY fE sorry).pt ⟶ s.pt},
          (PushoutCocone.mk iY fE sorry).inl ≫ m = s.inl → (PushoutCocone.mk iY fE sorry).inr ≫ m = s.inr → m = l }
Tactic: refine ⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ { 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 }
have 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 }
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ { 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 }
have mp : fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr
Tactic: refine ⟨BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl,
        BinaryCofan.IsColimit.inr_desc h _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ { 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 }
have mp₁ : ∀ {m : YE ⟶ s.pt}, iY ≫ m = s.inl → fE ≫ m = s.inr → m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Tactic: refine ⟨BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl,
        BinaryCofan.IsColimit.inr_desc h _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr
have mp : c.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
Tactic: apply BinaryCofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inr
have mp₁ : c.inr ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
Tactic: apply BinaryCofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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.inl ≫ fE ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
have mp : f ≫ iY ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
Tactic: rw [← H.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 ≫ iY ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inl ≫ s.inr
have mp : f ≫ (BinaryCofan.mk (c.inr ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = c.inl ≫ s.inr
Tactic: erw [h.fac _ ⟨WalkingPair.right⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
have mp : (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
have 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
Tactic: apply BinaryCofan.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ m = BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
have 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
Tactic: apply BinaryCofan.IsColimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
have mp : (c.inr ≫ fE) ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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) ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
have mp : (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = c.inr ≫ s.inr
Tactic: rw [Category.assoc, e₂, eq_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
have mp : (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inl
Tactic: refine e₁.trans (Eq.symm ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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))
have mpr : (H : IsPushout f c.inl iY fE) → IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
Tactic: refine fun H => ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
have mpr : (s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y) →
  YE ⟶ s.pt
Tactic: fapply Limits.BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
have 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)) sorry) = s.inl
Tactic: fapply Limits.BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
have 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)) sorry) = s.inr
Tactic: fapply Limits.BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
have 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)) sorry)
Tactic: fapply Limits.BinaryCofan.isColimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl
have mpr : c.inr ≫ fE ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry) = s.inl
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ c.inr ≫ fE ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl
have mpr : c.inr ≫
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)) WalkingSpan.right =
  s.inl
Tactic: erw [H.isColimit.fac _ WalkingSpan.right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯))
        WalkingSpan.right =
    s.inl
have mpr : (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = s.inl
Tactic: erw [hc.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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
⊢ m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
have mpr : H.cocone.inl ≫ m =
  H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)
Tactic: apply PushoutCocone.IsColimit.hom_ext H.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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)) ⋯)
⊢ m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
have mpr₁ : H.cocone.inr ≫ m =
  H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)
Tactic: apply PushoutCocone.IsColimit.hom_ext H.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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 ≫ m =
    H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
have mpr : H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry) =
  H.cocone.inl ≫ m
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)
have mpr : H.cocone.inr ≫ m =
  NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)) WalkingSpan.right
Tactic: rw [H.isColimit.fac _ WalkingSpan.right]