awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ c.inl ≫ d
⊢ (αX ≫ HT.from X) ≫ c₀.inl = c'.inl ≫ f ≫ d
have rw₁ : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ HT.from X ≫ c₀.inl
Tactic: rw [← reassoc_of% hX, hd, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ c.inl ≫ d
rw₁ : (αX ≫ HT.from X) ≫ c₀.inl = αX ≫ HT.from X ≫ c₀.inl
⊢ (αX ≫ HT.from X) ≫ c₀.inl = c'.inl ≫ f ≫ d
have rw₂ : αX ≫ HT.from X ≫ c₀.inl = αX ≫ HT.from X ≫ c₀.inl
Tactic: rw [← reassoc_of% hX, hd, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d
have rw : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ c.inr ≫ d
Tactic: rw [← reassoc_of% hY, hd', Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ c.inr ≫ d
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d
have rw₁ : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ HT.from Y ≫ c₀.inr
Tactic: rw [← reassoc_of% hY, hd', Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
rw : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ c.inr ≫ d
rw₁ : (αY ≫ HT.from Y) ≫ c₀.inr = αY ≫ HT.from Y ≫ c₀.inr
⊢ (αY ≫ HT.from Y) ≫ c₀.inr = c'.inr ≫ f ≫ d
have rw₂ : αY ≫ HT.from Y ≫ c₀.inr = αY ≫ HT.from Y ≫ c₀.inr
Tactic: rw [← reassoc_of% hY, hd', Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have van_kampen' : IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: rw [H c' (αX ≫ HT.from _) (αY ≫ HT.from _) (f ≫ d) (by rw [← reassoc_of% hX, hd, Category.assoc])
      (by rw [← reassoc_of% hY, hd', Category.assoc])]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have hl : IsPullback c.inl (HT.from X) d c₀.inl
Tactic: obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have hr : IsPullback c.inr (HT.from Y) d c₀.inr
Tactic: obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
hr : IsPullback c.inr (HT.from Y) d c₀.inr
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have van_kampen' : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: rw [hl.paste_vert_iff hX.symm, hr.paste_vert_iff hY.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
inst_2 : HasPullbacksOfInclusions.{v, u} C
T : C
HT : IsTerminal.{v, u} T
c₀ : BinaryCofan.{v, u} T T
hc₀ : IsColimit c₀
H :
  ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ T) (αY : Y' ⟶ T) (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 : BinaryCofan.{v, u} X Y
hc : IsColimit c
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
d :
  c.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c₀.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
hd : c.inl ≫ d = HT.from X ≫ c₀.inl
hd' : c.inr ≫ d = HT.from Y ≫ c₀.inr
hl : IsPullback c.inl (HT.from X) d c₀.inl
hr : IsPullback c.inr (HT.from Y) d c₀.inr
van_kampen' :
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ IsPullback c'.inl (αX ≫ HT.from X) (f ≫ d) c₀.inl ∧ IsPullback c'.inr (αY ≫ HT.from Y) (f ≫ d) c₀.inr ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
have van_kampen'₁ : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr ↔
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
Tactic: rw [hl.paste_vert_iff hX.symm, hr.paste_vert_iff hY.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
⊢ FinitaryExtensive (Type u)
have rw : IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})
Tactic: rw [finitaryExtensive_iff_of_isTerminal (Type u) PUnit Types.isTerminalPUnit _
      (Types.binaryCoproductColimit _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
⊢ IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})
have h₁ : ∀ {X' Y' : Type u} (αX : X' ⟶ PUnit.{u + 1}) (αY : Y' ⟶ PUnit.{u + 1})
  (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
      BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
    αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
      IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
          (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
        IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
          (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Tactic: apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => Types.binaryCoproductColimit X Y) _
      fun f g => (Limits.Types.pullbackLimitCone f g).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
h₁ :
  ∀ {X' Y' : Type u} (αX : X' ⟶ PUnit.{u + 1}) (αY : Y' ⟶ PUnit.{u + 1})
    (f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt),
    αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
        BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f →
      αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
          BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f →
        IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
            (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
          IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
            (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ IsVanKampenColimit (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})
have h₂ : {Z : Type u} →
  (f : Z ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt) →
    IsColimit
      (BinaryCofan.mk
        (PullbackCone.fst
          (Types.pullbackLimitCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone)
        (PullbackCone.fst
          (Types.pullbackLimitCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))).cone))
Tactic: apply BinaryCofan.isVanKampen_mk _ _ (fun X Y => Types.binaryCoproductColimit X Y) _
      fun f g => (Limits.Types.pullbackLimitCone f g).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
      (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
    IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
      (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
have h₁ : IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
  (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
h₁ :
  IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
      (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1})) ∧
    IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
      (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
have h₂ : IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
  (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
⊢ IsPullback (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX f
    (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
have h₁ : (s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))) →
  { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).snd = s.snd → m = l }
Tactic: refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
⊢ ∃! y : X',
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.left }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }))
      (Sum.inl y : X' ⊕ Y')
have inl : ∀ (val : X')
  (h :
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.left }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }))
      (Sum.inl val : X' ⊕ Y')),
  ∃! y : X',
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
      (Sum.inl val) (Sum.inl y)
Tactic: rcases h : s.fst x with val | val