awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) ↔
    ∀ (j : K),
      IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app j) f
        (c.ι.app j)
have h : (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) ↔
  ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
Tactic: simp only [Functor.const_obj_obj, Functor.comp_obj, Cocone.whisker_pt, Cocone.whisker_ι,
      whiskerLeft_app, NatTrans.comp_app, Equivalence.invFunIdAssoc_hom_app, Functor.id_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) ↔
    ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
have h : (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) →
  ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
h :
  (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) →
    ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
⊢ (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))) ↔
    ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
have h₁ : (∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)) →
  ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
⊢ IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.app k)) f (c.ι.app k)
have h : IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.app k))
  (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)
Tactic: rw [← Category.comp_id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
⊢ IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.app k))
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)
have h : IsPullback (c.ι.app (e.functor.obj (e.inverse.obj k))) (F.map (e.counit.app k)) (𝟙 (Cocone.whisker e.functor c).pt)
  (c.ι.app k)
Tactic: refine (H (e.inverse.obj k)).paste_vert ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
⊢ IsPullback (c.ι.app (e.functor.obj (e.inverse.obj k))) (F.map (e.counit.app k)) (𝟙 (Cocone.whisker e.functor c).pt)
    (c.ι.app k)
have this : IsIso.{v, u} (𝟙 (Cocone.whisker e.functor c).pt)
Tactic: have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
have this : α.app j = F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))
Tactic: have : α.app j
          = F'.map (e.unit.app _) ≫ α.app _ ≫ F.map (e.counit.app (e.functor.obj j)) := by
        simp [← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
this : α.app j = F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
have h : IsPullback (c'.ι.app j)
  (F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))) (𝟙 c'.pt ≫ f)
  (c.ι.app (e.functor.obj j))
Tactic: rw [← Category.id_comp f, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
this : α.app j = F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))
⊢ IsPullback (c'.ι.app j)
    (F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j)))
    (𝟙 c'.pt ≫ f) (c.ι.app (e.functor.obj j))
have h : IsPullback (c'.ι.app j) (F'.map (e.unit.app j)) (𝟙 c'.pt) (c'.ι.app (e.inverse.obj (e.functor.obj j)))
Tactic: refine IsPullback.paste_vert ?_ (H (e.functor.obj j))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u_3
inst_2 : Category.{v_3, u_3} K
e : Equivalence.{u', v_3, v', u_3} J K
F : Functor.{v_3, v, u_3, u} K C
c : Cocone F
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
have w : ∀ (k : K),
  ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app k =
    ((Cocone.whisker e.inverse c').ι ≫ map (const K) f).app k
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
x : C
⊢ Eq (α :=
    F' ⋙ obj (evaluation C D) x ⟶
      obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)))
    (whiskerRight α (obj (evaluation C D) x) ≫ Cocone.ι (mapCocone (obj (evaluation C D) x) c))
    (CategoryStruct.comp (Y :=
      obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')))
      (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) (map (const J) (map (obj (evaluation C D) x) f)))
have w : ∀ (y : J),
  Eq (α :=
    (F' ⋙ obj (evaluation C D) x).obj y ⟶
      obj.{u', v_2, v', u_2}
        (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) y)
    (NatTrans.app (whiskerRight α (obj (evaluation C D) x) ≫ Cocone.ι (mapCocone (obj (evaluation C D) x) c)) y)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')))
        (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) (map (const J) (map (obj (evaluation C D) x) f)))
      y)
Tactic: ext y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
x : C
y : J
⊢ Eq (α :=
    (F' ⋙ obj (evaluation C D) x).obj y ⟶
      obj.{u', v_2, v', u_2}
        (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) y)
    (NatTrans.app (whiskerRight α (obj (evaluation C D) x) ≫ Cocone.ι (mapCocone (obj (evaluation C D) x) c)) y)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')))
        (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) (map (const J) (map (obj (evaluation C D) x) f)))
      y)
have w : (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have this : ∀ (x : C),
  Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
    ∀ (j : J),
      IsPullback (X :=
        obj.{u', v_2, v', u_2}
          (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
        (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
        (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
        ((whiskerRight α (obj (evaluation C D) x)).app j)
        (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
        (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
          (F ⋙ obj (evaluation C D) x).obj j ⟶
            obj.{u', v_2, v', u_2}
              (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
Tactic: have := fun x => hc x (((evaluation C D).obj x).mapCocone c') (whiskerRight α _)
      (((evaluation C D).obj x).map f)
      (by
        ext y
        dsimp
        exact NatTrans.congr_app (NatTrans.congr_app e y) x)
      (hα.whiskerRight _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mp : Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
mp : Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mpr : (∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → Nonempty (IsColimit c')
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have mp : (k : C) →
  IsLimit (F := cospan f (c.ι.app j) ⋙ obj (evaluation C D) k)
    (mapCone (obj (evaluation C D) k) (PullbackCone.mk (c'.ι.app j) (α.app j) sorry))
Tactic: refine ⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasPullbacks.{v_2, u_2} D
inst_4 : HasColimitsOfShape.{u', v', v_2, u_2} J D
F : J ⥤ Functor.{v, v_2, u, u_2} C D
c : Cocone F
hc : ∀ (x : C), IsVanKampenColimit (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c)
F' : J ⥤ Functor.{v, v_2, u, u_2} C D
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
e : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this :
  ∀ (x : C),
    Nonempty (IsColimit (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c')) ↔
      ∀ (j : J),
        IsPullback (X :=
          obj.{u', v_2, v', u_2}
            (obj (const J) (Cocone.pt (F := F' ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c'))) j)
          (Z := Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c')) j)
          ((whiskerRight α (obj (evaluation C D) x)).app j)
          (map (obj (evaluation C D) x) f : obj (obj (evaluation C D) x) c'.pt ⟶ obj (obj (evaluation C D) x) c.pt)
          (NatTrans.app (Cocone.ι (mapCocone (obj (evaluation C D) x) c)) j :
            (F ⋙ obj (evaluation C D) x).obj j ⟶
              obj.{u', v_2, v', u_2}
                (obj (const J) (Cocone.pt (F := F ⋙ obj (evaluation C D) x) (mapCocone (obj (evaluation C D) x) c))) j)
hc' : IsColimit c'
j : J
⊢ (k : C) →
    IsLimit (F := cospan f (c.ι.app j) ⋙ obj (evaluation C D) k)
      (mapCone (obj (evaluation C D) k) (PullbackCone.mk (c'.ι.app j) (α.app j) ⋯))
have mp : (x : C) →
  IsLimit (F :=
    cospan (X := obj (obj (evaluation C D) x) (obj (obj (const J) c'.pt) j)) (map (obj (evaluation C D) x) f)
      (map (obj (evaluation C D) x) (c.ι.app j)))
    (PullbackCone.mk (map (obj (evaluation C D) x) (c'.ι.app j)) (map (obj (evaluation C D) x) (α.app j)) sorry)
Tactic: refine fun x => (isLimitMapConePullbackConeEquiv _ _).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
⊢ IsVanKampenColimit (Gl.mapCocone c)
have this : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
Tactic: have := adj.rightAdjoint_preservesLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
⊢ IsVanKampenColimit (Gl.mapCocone c)
have this₁ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
Tactic: have : PreservesColimitsOfSize.{u', v'} Gl := adj.leftAdjoint_preservesColimits