awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ mapPair αX αY ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
have w : Eq (α :=
  obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair } ⟶
    obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
  (NatTrans.app (mapPair αX αY ≫ c.ι) { as := WalkingPair.left })
  ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.left })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
w :
  Eq (α :=
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair αX αY ≫ c.ι) { as := WalkingPair.left })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.left })
⊢ mapPair αX αY ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
have w₁ : Eq (α :=
  obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.right : Discrete WalkingPair } ⟶
    obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
  (NatTrans.app (mapPair αX αY ≫ c.ι) { as := WalkingPair.right })
  ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.right })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair αX αY ≫ c.ι) { as := WalkingPair.left })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.left })
have w : Eq (α := X' ⟶ c.pt) (αX ≫ c.ι.app { as := WalkingPair.left }) (c'.ι.app { as := WalkingPair.left } ≫ f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair αX αY ≫ c.ι) { as := WalkingPair.right })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.right })
have w : Eq (α := Y' ⟶ c.pt) (αY ≫ c.ι.app { as := WalkingPair.right }) (c'.ι.app { as := WalkingPair.right } ≫ f)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp : (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) ↔
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: rw [H c' (mapPair αX αY) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> assumption) (.of_discrete _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp : (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) →
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
mp :
  (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) →
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp₁ : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr →
  ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F' = pair X' Y'
have h_obj : ∀ (X : Discrete WalkingPair), F'.obj X = obj.{0, v, 0, u} (pair X' Y') X
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
h_obj : ∀ (X : Discrete WalkingPair), F'.obj X = obj.{0, v, 0, u} (pair X' Y') X
⊢ F' = pair X' Y'
have h_map : ∀ (X Y : Discrete WalkingPair) (f : X ⟶ Y),
  HEq (F'.map f) (β := obj.{0, v, 0, u} (pair X' Y') X ⟶ obj.{0, v, 0, u} (pair X' Y') Y) (map (pair X' Y') f)
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have this : F' = pair X' Y'
Tactic: have : F' = pair X' Y' := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X', Y']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : ∀ (X' Y' : C) (this : F' = pair X' Y'),
  Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: clear_value X' Y'
Cleared hypotheses: X', Y', this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' Y' : C
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : ∀ (c' : Cocone.{0, v, 0, u} (pair X' Y'))
  (α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)) (f : c'.pt ⟶ c.pt)
  (hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f) (h : NatTrans.Equifibered α),
  Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: subst this
Cleared hypotheses: F', c', α, f, hα, h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
c' : Cocone.{0, v, 0, u} (pair X' Y')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : ∀ (c' : BinaryCofan.{v, u} X' Y') (f : c'.pt ⟶ c.pt) (hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f),
  Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: change BinaryCofan X' Y' at c'
Cleared hypotheses: c', f, hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr ↔
  ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
        (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr →
  ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
mpr :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr₁ : (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
  IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
⊢ IsVanKampenColimit c
have rw : ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
  αX ≫ c.inl = c'.inl ≫ f →
    αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
Tactic: rw [BinaryCofan.isVanKampen_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp : Nonempty (IsColimit c') → IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
mp : Nonempty (IsColimit c') → IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mpr : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr → Nonempty (IsColimit c')
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp : IsPullback c'.inl αX f c.inl
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
mp : IsPullback c'.inl αX f c.inl
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have mp₁ : IsPullback c'.inr αY f c.inr
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl αX f c.inl
have mp : IsPullback c'.inl (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) c.inl
Tactic: rw [← Category.id_comp αX, ← Iso.hom_inv_id_assoc e f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
h : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inl (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) c.inl
have this : IsIso.{v, u} (𝟙 X')
Tactic: haveI : IsIso (𝟙 X') := inferInstance