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 ⋯
⊢ (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
have rw : g' ≫ cmp ≫ pullback.snd αZ i = αW ≫ c.inl
Tactic: rw [Category.assoc, pullback.lift_snd, hg.w]
-- 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 ⋯
rw : g' ≫ cmp ≫ pullback.snd αZ i = αW ≫ c.inl
⊢ (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
have rw₁ : g' ≫ αY = αW ≫ c.inl
Tactic: rw [Category.assoc, pullback.lift_snd, hg.w]
-- 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 ⋯
rw : g' ≫ cmp ≫ pullback.snd αZ i = αW ≫ c.inl
rw₁ : g' ≫ αY = αW ≫ c.inl
⊢ (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
have rw₂ : αW ≫ c.inl = αW ≫ c.inl
Tactic: rw [Category.assoc, pullback.lift_snd, hg.w]
-- 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₄ :
  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 ⋯
⊢ IsPullback i' αY αZ i
have e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
Tactic: have e₁ : (g' ≫ cmp) ≫ pullback.snd _ _ = αW ≫ c.inl := by
      rw [Category.assoc, pullback.lift_snd, hg.w]
-- 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
⊢ Eq (α := pullback αY c.inr ⟶ c.pt) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
have rw : Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.fst αY c.inr ≫ cmp ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
Tactic: rw [Category.assoc, pullback.lift_snd, pullback.condition]
-- 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
rw :
  Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.fst αY c.inr ≫ cmp ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
⊢ Eq (α := pullback αY c.inr ⟶ c.pt) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
have rw₁ : Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.fst αY c.inr ≫ αY) (pullback.snd αY c.inr ≫ c.inr)
Tactic: rw [Category.assoc, pullback.lift_snd, pullback.condition]
-- 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
rw :
  Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.fst αY c.inr ≫ cmp ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
rw₁ : Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.fst αY c.inr ≫ αY) (pullback.snd αY c.inr ≫ c.inr)
⊢ Eq (α := pullback αY c.inr ⟶ c.pt) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i) (pullback.snd αY c.inr ≫ c.inr)
have rw₂ : Eq (α := pullback αY c.inr ⟶ c.pt) (pullback.snd αY c.inr ≫ c.inr) (pullback.snd αY c.inr ≫ c.inr)
Tactic: rw [Category.assoc, pullback.lift_snd, pullback.condition]
-- 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₄ :
  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
⊢ IsPullback i' αY αZ i
have 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)
Tactic: have e₂ : (pullback.fst _ _ ≫ cmp : pullback αY c.inr ⟶ _) ≫ pullback.snd _ _ =
        pullback.snd _ _ ≫ c.inr := by
      rw [Category.assoc, pullback.lift_snd, pullback.condition]
-- 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 (X :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) αW (pullback.snd αZ i) c.inl ∧
    IsPullback (P :=
      Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair }) (X :=
      Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) (pullback.snd αY c.inr)
      (pullback.snd αZ i) c.inr
have left : IsPullback (X :=
  Functor.obj.{0, v, 0, u}
    (Functor.obj (Functor.const (Discrete WalkingPair))
      (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
    { as := WalkingPair.left : Discrete WalkingPair })
  (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) αW (pullback.snd αZ i) c.inl
Tactic: constructor
-- 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 (X :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (BinaryCofan.inl (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) αW (pullback.snd αZ i) c.inl
have apply : IsPullback ((g' ≫ cmp) ≫ pullback.fst αZ i) αW αZ (c.inl ≫ i)
Tactic: apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
-- 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 ((g' ≫ cmp) ≫ pullback.fst αZ i) αW αZ (c.inl ≫ i)
have rw : IsPullback (f' ≫ h') αW αZ (f ≫ h)
Tactic: rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]
-- 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 (P :=
    Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair }) (X :=
    Functor.obj.{0, v, 0, u}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp))) (pullback.snd αY c.inr)
    (pullback.snd αZ i) c.inr
have apply : IsPullback (P := pullback αY c.inr) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.fst αZ i) (pullback.snd αY c.inr) αZ
  (c.inr ≫ i)
Tactic: apply IsPullback.of_right _ e₂ (IsPullback.of_hasPullback _ _)
-- 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 (P := pullback αY c.inr) ((pullback.fst αY c.inr ≫ cmp) ≫ pullback.fst αZ i) (pullback.snd αY c.inr) αZ
    (c.inr ≫ i)
have rw : IsPullback (P := pullback αY c.inr) (pullback.fst αY c.inr ≫ i') (pullback.snd αY c.inr) αZ (c.inr ≫ i)
Tactic: rw [Category.assoc, pullback.lift_fst]