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
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have h₁ : IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔
  IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
Tactic: conv_lhs => rw [← Category.comp_id (α.app j)]
-- 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
F : Functor.{u', v, v', u} J C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : Functor.{u', v, v', u} J C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j) ↔
    IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
have this₁ : IsIso e.inv.hom
Tactic: haveI : IsIso e.inv.hom := Functor.map_isIso (Cocone.forget _) e.inv
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
have refine : (∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)) ↔
  ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
Tactic: refine (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (.of_isIso _))).trans ?_
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
⊢ (∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)) ↔
    ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
have h : ∀ (a : J),
  IsPullback (c'.ι.app a) ((α' ≫ α).app a) f (c.ι.app a) ↔
    IsPullback (c'.ι.app a) (α'.app a) f (((Cocone.precompose α).obj c).ι.app a)
Tactic: apply forall_congr'
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
j : J
⊢ IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j) ↔
    IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
have h : IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔ IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)
Tactic: simp only [Functor.const_obj_obj, NatTrans.comp_app,
    Cocone.precompose_obj_pt, Cocone.precompose_obj_ι]
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔
    IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)
have this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (obj.{u', v, v', u} (obj (const J) c.pt) j)) (c.ι.app j)
Tactic: have : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 _) (c.ι.app j) :=
    IsPullback.of_vert_isIso ⟨Category.comp_id _⟩
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsVanKampenColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
j : J
this : IsPullback (α.app j ≫ c.ι.app j) (α.app j) (𝟙 (obj.{u', v, v', u} (obj (const J) c.pt) j)) (c.ι.app j)
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j) ↔
    IsPullback (c'.ι.app j) (α'.app j) f (α.app j ≫ c.ι.app j)
have rw : c'.ι.app j ≫ f = α'.app j ≫ α.app j ≫ c.ι.app j
Tactic: rw [← IsPullback.paste_vert_iff this _, Category.comp_id]
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
⊢ Nonempty (IsColimit c')
have apply : ∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)
Tactic: apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (.of_isIso _)))
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)
have simp : IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)
Tactic: simp only [Functor.const_obj_obj, NatTrans.comp_app]
-- 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
F G : Functor.{u', v, v', u} J C
α : F ⟶ G
inst_2 : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)
have rw : IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) (f ≫ 𝟙 ((Cocone.precompose α).obj c).pt) (c.ι.app j)
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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : PreservesLimitsOfShape WalkingCospan G
inst_4 : ReflectsColimitsOfShape.{u', v', v, v_2, u, u_2} J G
hc : IsUniversalColimit (G.mapCocone c)
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ whiskerRight α G ≫ (G.mapCocone c).ι = (G.mapCocone c').ι ≫ map (const J) (G.map f)
have w : ∀ (j : J), (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j
Tactic: ext 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst_4 : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst_5 : ReflectsLimitsOfShape WalkingCospan G
inst_6 : PreservesColimitsOfShape.{u', v', v, v_2, u, u_2} J G
inst_7 : ReflectsColimitsOfShape.{u', v', v, v_2, u, u_2} J G
H : IsVanKampenColimit (G.mapCocone c)
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ whiskerRight α G ≫ (G.mapCocone c).ι = (G.mapCocone c').ι ≫ map (const J) (G.map f)
have w : ∀ (j : J), (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j
Tactic: ext 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst_4 : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst_5 : ReflectsLimitsOfShape WalkingCospan G
inst_6 : PreservesColimitsOfShape.{u', v', v, v_2, u, u_2} J G
inst_7 : ReflectsColimitsOfShape.{u', v', v, v_2, u, u_2} J G
H : IsVanKampenColimit (G.mapCocone c)
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ 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 refine_1 : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (G.mapCocone c'))
Tactic: refine (Iff.trans ?_ (H (G.mapCocone c') (whiskerRight α G) (G.map f)
      (by ext j; simpa using G.congr_map (NatTrans.congr_app h j))
      (hα.whiskerRight G))).trans (forall_congr' fun 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : ∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), PreservesLimit (cospan f (F.map g)) G
inst_4 : ∀ (i : J) (X : C) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) G
inst_5 : ReflectsLimitsOfShape WalkingCospan G
inst_6 : PreservesColimitsOfShape.{u', v', v, v_2, u, u_2} J G
inst_7 : ReflectsColimitsOfShape.{u', v', v, v_2, u, u_2} J G
H : IsVanKampenColimit (G.mapCocone c)
F' : Functor.{u', v, v', u} J C
c' : Cocone F'
α : F' ⟶ F
f : c'.pt ⟶ c.pt
h : α ≫ c.ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
refine_1 : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (G.mapCocone c'))
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
have refine_2 : ∀ (j : J),
  IsPullback ((G.mapCocone c').ι.app j) ((whiskerRight α G).app j) (G.map f) ((G.mapCocone c).ι.app j) ↔
    IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
Tactic: refine (Iff.trans ?_ (H (G.mapCocone c') (whiskerRight α G) (G.map f)
      (by ext j; simpa using G.congr_map (NatTrans.congr_app h j))
      (hα.whiskerRight G))).trans (forall_congr' fun 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.mapCocone c)
have apply : IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))
Tactic: apply IsVanKampenColimit.of_mapCocone G.inv
-- 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
G : Functor.{v, v_2, u, u_2} C D
F : Functor.{u', v, v', u} J C
c : Cocone F
inst_3 : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))
have apply : IsVanKampenColimit ((Cocone.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))
Tactic: apply (IsVanKampenColimit.precompose_isIso_iff e.inv).mp
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
⊢ Nonempty (IsColimit c')
have a : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) ?_ using 1
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
a : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
⊢ Nonempty (IsColimit c')
have convert_1 : (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) ?_ using 1
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
a : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
convert_1 :
  (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
⊢ Nonempty (IsColimit c')
have convert_2 : ∀ (j : K),
  IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app j) f
    (c.ι.app j)
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) ?_ using 1
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
have h : (e.inverse ⋙ F' ⟶ obj (const K) c.pt) = (e.inverse ⋙ F' ⟶ e.inverse ⋙ obj (const J) (Cocone.whisker e.functor c).pt) →
  (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)
Tactic: convert! congr_arg (whiskerLeft e.inverse) e'
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
e_1 :
  (e.inverse ⋙ F' ⟶ obj (const K) c.pt) = (e.inverse ⋙ F' ⟶ e.inverse ⋙ obj (const J) (Cocone.whisker e.functor c).pt)
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)
have h : ∀ (x : K),
  ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app x =
    (e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)).app x
Tactic: ext
-- 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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)
have convert_2 : IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).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 : IsUniversalColimit 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 ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k)
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)
have convert_2 : IsPullback ((Cocone.whisker e.functor c).ι.app (e.inverse.obj k)) ((e.invFunIdAssoc F).hom.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 (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 α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
have h : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) using 1
-- 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 : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
have h₁ : (∀ (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)
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) using 1
-- 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 : Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
h₁ :
  (∀ (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)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
have hc₁ : (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
Tactic: convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) using 1