awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
hc : IsUniversalColimit 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 α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
rw : IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
rw [← Category.comp_id (α.app j)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
hc : IsUniversalColimit 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 α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
hc : IsUniversalColimit 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 α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
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)

Tactic:
exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨by simp⟩)

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk, CategoryTheory.IsPullback.paste_vert
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
w : ∀ (j : J), (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j
⊢ c'.ι ≫ map (const J) e.inv.hom = c.ι

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
j : J
⊢ (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j

Tactic:
e.inv.2 j

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
j : J
⊢ (c'.ι ≫ map (const J) e.inv.hom).app j = c.ι.app j

Tactic:
exact e.inv.2 j

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
⊢ c'.ι ≫ map (const J) e.inv.hom = c.ι

Tactic:
have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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.ι
rw : α ≫ c.ι = c''.ι ≫ map (const J) f ≫ map (const J) e.inv.hom
rw₁ : α ≫ c.ι = α ≫ c'.ι ≫ map (const J) e.inv.hom
rw₂ rw₃ : α ≫ c.ι = α ≫ c.ι
⊢ α ≫ c.ι = c''.ι ≫ map (const J) (f ≫ e.inv.hom)

Tactic:
rw [Functor.map_comp, ← reassoc_of% h, this]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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.ι
rw :
  (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)) ↔
    ∀ (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)

Tactic:
rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]

Premises used: CategoryTheory.Limits.CoconeMorphism.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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.ι
h₁ :
  ∀ (a : J),
    IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)
⊢ (∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)) ↔
    ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
rw : IsPullback (c''.ι.app j) (α.app j ≫ 𝟙 (F.obj j)) (f ≫ e.inv.hom) (c.ι.app j)
| IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
rw [← Category.comp_id (α.app j)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
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)
⊢ IsPullback (c''.ι.app j) (α.app 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)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
⊢ IsIso e.inv.hom

Tactic:
haveI : IsIso e.inv.hom := Functor.map_isIso (Cocone.forget _) e.inv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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_1 : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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_1 : c'.ι ≫ map (const J) e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ 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:
exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.CommSq.mk, CategoryTheory.NatTrans.congr_app, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)

Tactic:
(hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (.of_isIso _))).trans ?_

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.CategoryStruct.comp, Iff.trans, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α'
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)
⊢ Nonempty (IsColimit c') ↔ ∀ (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 ?_

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.CategoryStruct.comp, Iff.trans, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α'
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)
⊢ (∀ (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:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
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)
⊢ IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j) ↔
    IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)

Tactic:
simp only [Functor.const_obj_obj, NatTrans.comp_app,
    Cocone.precompose_obj_pt, Cocone.precompose_obj_ι]

Premises used: CategoryTheory.Limits.Cocone.precompose_obj_ι, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.Cocone.precompose_obj_pt
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 (α.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 _⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
rw : c'.ι.app j ≫ f = α'.app j ≫ α.app 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)

Tactic:
rw [← IsPullback.paste_vert_iff this _, Category.comp_id]

Premises used: CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
⊢ c'.ι.app j ≫ f = α'.app j ≫ α.app j ≫ c.ι.app j

Tactic:
(congr_app e j).symm

Premises used: Eq.symm, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
⊢ c'.ι.app j ≫ f = α'.app j ≫ α.app j ≫ c.ι.app j

Tactic:
exact (congr_app e j).symm

Premises used: Eq.symm, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
apply : ∀ (j : J), IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c')

Tactic:
apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) (hα.comp (.of_isIso _)))

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.CategoryStruct.comp, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
simp : IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)
⊢ IsPullback (c'.ι.app j) ((α' ≫ α).app j) f (c.ι.app j)

Tactic:
simp only [Functor.const_obj_obj, NatTrans.comp_app]

Premises used: CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
rw : IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) (f ≫ 𝟙 ((Cocone.precompose α).obj c).pt) (c.ι.app j)
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)

Tactic:
rw [← Category.comp_id f]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 ((Cocone.precompose α).obj c)
⊢ ∀ (j : J),
    ((Cocone.precompose (inv α)).obj ((Cocone.precompose α).obj c)).ι.app j ≫
        Iso.hom (Iso.refl ((Cocone.precompose (inv α)).obj ((Cocone.precompose α).obj c)).pt) =
      c.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
w : ∀ (j : J), (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j
⊢ whiskerRight α G ≫ (G.mapCocone c).ι = (G.mapCocone c').ι ≫ map (const J) (G.map f)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j

Tactic:
simpa using G.congr_map (NatTrans.congr_app h j)

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
w : ∀ (j : J), (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j
⊢ whiskerRight α G ≫ (G.mapCocone c).ι = (G.mapCocone c').ι ≫ map (const J) (G.map f)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 α
j : J
⊢ (whiskerRight α G ≫ (G.mapCocone c).ι).app j = ((G.mapCocone c').ι ≫ map (const J) (G.map f)).app j

Tactic:
simpa using G.congr_map (NatTrans.congr_app h j)

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.Functor.congr_map