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 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)
⊢ IsPullback i' αY αZ i
have refine_2 : ∀ (hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))),
  IsPullback i' αY αZ i
Tactic: obtain ⟨hc₄⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
      (BinaryCofan.mk _ _) αW _ _ e₁.symm e₂.symm).mpr <| by
        constructor
        · apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄
        · apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst]; exact hc₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' αY αZ i
have refine_2 : IsPullback i' (cmp ≫ pullback.snd αZ i) (𝟙 Z' ≫ αZ) i
Tactic: rw [← Category.id_comp αZ, ← show cmp ≫ pullback.snd _ _ = αY from pullback.lift_snd _ _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' (cmp ≫ pullback.snd αZ i) (𝟙 Z' ≫ αZ) i
have apply : IsPullback i' cmp (𝟙 Z') (pullback.fst αZ i)
Tactic: apply IsPullback.paste_vert _ (IsPullback.of_hasPullback αZ i)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
have h₁ : Eq (α := Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.left : Discrete WalkingPair } ⟶ Y'')
  (BinaryCofan.inl (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ cmp)
  (BinaryCofan.inl (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ (hc₂.coconePointUniqueUpToIso hc₄).hom)
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
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
h₁ :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.left : Discrete WalkingPair } ⟶ Y'')
    (BinaryCofan.inl (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ cmp)
    (BinaryCofan.inl (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ (hc₂.coconePointUniqueUpToIso hc₄).hom)
⊢ cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
have h₂ : Eq (α :=
  Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair } ⟶ Y'')
  (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ cmp)
  (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ (hc₂.coconePointUniqueUpToIso hc₄).hom)
Tactic: apply BinaryCofan.IsColimit.hom_ext hc₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (hypothesis)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
⊢ IsPullback i' cmp (𝟙 Z') (pullback.fst αZ i)
have this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
Tactic: have : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom := by
      apply BinaryCofan.IsColimit.hom_ext hc₂
      exacts [(hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.left⟩).symm,
        (hc₂.comp_coconePointUniqueUpToIso_hom hc₄ ⟨WalkingPair.right⟩).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
⊢ IsPullback i' cmp (𝟙 Z') (pullback.fst αZ i)
have rw : IsPullback i' (hc₂.coconePointUniqueUpToIso hc₄).hom (𝟙 Z') (pullback.fst αZ i)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
⊢ i' ≫ 𝟙 Z' = (hc₂.coconePointUniqueUpToIso hc₄).hom ≫ pullback.fst αZ i
have rw : i' ≫ 𝟙 Z' = cmp ≫ pullback.fst αZ i
Tactic: rw [← this, Category.comp_id, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
rw : i' ≫ 𝟙 Z' = cmp ≫ pullback.fst αZ i
⊢ i' ≫ 𝟙 Z' = (hc₂.coconePointUniqueUpToIso hc₄).hom ≫ pullback.fst αZ i
have rw₁ : i' = cmp ≫ pullback.fst αZ i
Tactic: rw [← this, Category.comp_id, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
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₄_1 :
  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)
hc₄ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))
this : cmp = (hc₂.coconePointUniqueUpToIso hc₄).hom
rw : i' ≫ 𝟙 Z' = cmp ≫ pullback.fst αZ i
rw₁ : i' = cmp ≫ pullback.fst αZ i
⊢ i' ≫ 𝟙 Z' = (hc₂.coconePointUniqueUpToIso hc₄).hom ≫ pullback.fst αZ i
have rw₂ : i' = i'
Tactic: rw [← this, Category.comp_id, pullback.lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
⊢ f = g
have obtain : ∀ (w : C) (f' : w ⟶ pullback f u) (w_1 : w ⟶ pullback f v) (w_2 : w ⟶ pullback a b)
  (p₁ : IsPullback f' w_2 (snd f u) (fst a b)),
  IsPullback w_1 w_2 (snd f v) (snd a b) → ∀ (h₁ : IsPushout f' w_1 (fst f u) (fst f v)), f = g
Tactic: obtain ⟨_, f', _, _, p₁, _, h₁⟩ :=
      (van_kampen (of_hasPushout _ _)).exists_cube_filling sq_f_u sq_f_v
-- Lean 4 proof step from Mathlib.CategoryTheory.Adhesive.Basic (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
W X Y Z_1 : C
f_1 : W ⟶ X
g_1 : W ⟶ Y
h : X ⟶ Z_1
i : Y ⟶ Z_1
inst_2 : Adhesive.{v, u} C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst_3 : Mono a
inst_4 : Mono b
K : C
f g : K ⟶ pushout (X := pullback a b) (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (X := pullback a b) (fst a b) (snd a b) := inr (fst a b) (snd a b)
this_1 : Mono u := ⋯
this : Mono v := ⋯
sq_f_u : IsPullback (P := pullback f u) (fst f u) (snd f u) f u := ⋯
sq_f_v : IsPullback (P := pullback f v) (fst f v) (snd f v) f v := ⋯
sq_g_u : IsPullback (P := pullback g u) (fst g u) (snd g u) g u := ⋯
sq_g_v : IsPullback (P := pullback g v) (fst g v) (snd g v) g v := ⋯
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
w_1 : C
f' : w_1 ⟶ pullback f u
w_2 : w_1 ⟶ pullback f v
w_3 : w_1 ⟶ pullback a b
p₁ : IsPullback f' w_3 (snd f u) (fst a b)
left : IsPullback w_2 w_3 (snd f v) (snd a b)
h₁ : IsPushout f' w_2 (fst f u) (fst f v)
⊢ Mono f'
have rw : Mono
  (CategoryStruct.comp (Y := pullback (X := pullback f u) (Y := pullback a b) (snd f u) (fst a b))
    (Iso.hom p₁.isoPullback) (fst (snd f u) (fst a b)))
Tactic: rw [← p₁.isoPullback_hom_fst]