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
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 =
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
have mpr : c.inl ≫ H.cocone.inr ≫ m =
  c.inl ≫
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)) WalkingSpan.right
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_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
mpr :
  c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
⊢ H.cocone.inr ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
have mpr₁ : c.inr ≫ H.cocone.inr ≫ m =
  c.inr ≫
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)) WalkingSpan.right
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_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
have mpr : c.inl ≫ H.cocone.inr ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
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
⊢ c.inl ≫ H.cocone.inr ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
have mpr : f ≫ iY ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
Tactic: erw [← 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_1 : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan.{v, u} (Functor.obj.{0, v, 0, u} (pair X E) { as := WalkingPair.right : Discrete WalkingPair }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ f ≫ iY ≫ m = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
have mpr : f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }
Tactic: rw [e₂]
-- 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
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
have mpr : s.inl =
  c.inr ≫
    NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) sorry)) WalkingSpan.right
Tactic: refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_
-- 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
⊢ s.inl =
    c.inr ≫
      NatTrans.app (Cocone.ι (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)) WalkingSpan.right
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: 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
⊢ H.IsVanKampen
have obtain : ∀ (hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)), H.IsVanKampen
Tactic: obtain ⟨hc₁⟩ := (is_coprod_iff_isPushout c hc H.1).mpr H
-- 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'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have obtain : ∀ (hc₂ : IsColimit (F := pair W' (pullback αY c.inr)) (BinaryCofan.mk g' (pullback.fst αY c.inr))),
  IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Tactic: obtain ⟨hc₂⟩ := ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen c hc)
    (BinaryCofan.mk _ (pullback.fst _ _)) _ _ _ hg.w.symm pullback.condition.symm).mpr
    ⟨hg, IsPullback.of_hasPullback αY c.inr⟩
-- 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))
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine : Nonempty
    (IsColimit (F :=
      pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
        X')
      (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Tactic: refine (is_coprod_iff_isPushout _ hc₂ w).symm.trans ?_
-- 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))
⊢ Nonempty
      (IsColimit (F :=
        pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
          X')
        (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine_1 : Eq (α :=
  pullback αY c.inr ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryCofan.mk (c.inr ≫ i) h).pt)
      { as := WalkingPair.left : Discrete WalkingPair })
  (pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl)
  (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h') ≫ αZ)
Tactic: refine ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_
-- 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))
refine_1 :
  Eq (α :=
    pullback αY c.inr ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryCofan.mk (c.inr ≫ i) h).pt)
        { as := WalkingPair.left : Discrete WalkingPair })
    (pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl)
    (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h') ≫ αZ)
⊢ Nonempty
      (IsColimit (F :=
        pair (Functor.obj.{0, v, 0, u} (pair W' (pullback αY c.inr)) { as := WalkingPair.right : Discrete WalkingPair })
          X')
        (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine_2 : IsPullback (P :=
      Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      αX αZ (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Tactic: refine ((BinaryCofan.isVanKampen_iff _).mp (FinitaryExtensive.vanKampen _ hc₁)
    (BinaryCofan.mk _ _) (pullback.snd _ _) _ _ ?_ hh.w.symm).trans ?_
-- 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))
⊢ Eq (α :=
    pullback αY c.inr ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) (BinaryCofan.mk (c.inr ≫ i) h).pt)
        { as := WalkingPair.left : Discrete WalkingPair })
    (pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl)
    (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h') ≫ αZ)
have refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
Tactic: dsimp
-- 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))
⊢ Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
have refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
Tactic: rw [← pullback.condition_assoc, Category.assoc, hi.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))
refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
⊢ Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
have refine_1₁ : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) (pullback.fst αY c.inr ≫ i' ≫ αZ)
Tactic: rw [← pullback.condition_assoc, Category.assoc, hi.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))
refine_1 : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
refine_1₁ : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) (pullback.fst αY c.inr ≫ i' ≫ αZ)
⊢ Eq (α := pullback αY c.inr ⟶ Z) (pullback.snd αY c.inr ≫ c.inr ≫ i) ((pullback.fst αY c.inr ≫ i') ≫ αZ)
have refine_1₂ : Eq (α := pullback αY c.inr ⟶ Z) (pullback.fst αY c.inr ≫ αY ≫ i) (pullback.fst αY c.inr ≫ αY ≫ i)
Tactic: rw [← pullback.condition_assoc, Category.assoc, hi.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))
⊢ IsPullback (P :=
        Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
        (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
        (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine_2 : IsPullback (P :=
      Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      αX αZ (BinaryCofan.mk (c.inr ≫ i) h).inr →
  IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
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))
refine_2 :
  IsPullback (P :=
        Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
        (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
        (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
⊢ IsPullback (P :=
        Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
        (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
        (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback
        (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h')) αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine_2₁ : IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
  IsPullback (P :=
      Functor.obj.{0, v, 0, u} (pair (pullback αY c.inr) X') { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      (pullback.snd αY c.inr) αZ (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr (BinaryCofan.mk g' (pullback.fst αY c.inr)) ≫ i') h'))
      αX αZ (BinaryCofan.mk (c.inr ≫ i) h).inr
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
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
have refine_2 : IsPullback i' αY αZ i
Tactic: refine ⟨hc₄, ?_⟩