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
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'))
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)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : 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 => ?_)

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.map, CategoryTheory.Functor.whiskerRight, CategoryTheory.NatTrans.Equifibered.whiskerRight, forall_congr', Iff.trans
-- 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 α
⊢ Nonempty (IsColimit c') ↔ Nonempty (IsColimit (G.mapCocone c'))

Tactic:
⟨fun h => ⟨isColimitOfPreserves G h.some⟩, fun h => ⟨isColimitOfReflects G h.some⟩⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects, Iff.intro, CategoryTheory.Limits.isColimitOfPreserves
-- 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 α
⊢ Nonempty (IsColimit c') ↔ Nonempty (IsColimit (G.mapCocone c'))

Tactic:
exact ⟨fun h => ⟨isColimitOfPreserves G h.some⟩, fun h => ⟨isColimitOfReflects G h.some⟩⟩
-- 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
⊢ 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:
IsPullback.map_iff G (NatTrans.congr_app h.symm j)

Premises used: CategoryTheory.NatTrans.congr_app, CategoryTheory.IsPullback.map_iff, 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
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
⊢ 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:
exact IsPullback.map_iff G (NatTrans.congr_app h.symm 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 : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
apply : IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))
⊢ IsVanKampenColimit (G.mapCocone c)

Tactic:
apply IsVanKampenColimit.of_mapCocone G.inv

Premises used: CategoryTheory.Functor.inv, CategoryTheory.IsVanKampenColimit.of_mapCocone
-- 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 : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
apply : IsVanKampenColimit ((Cocone.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))
⊢ IsVanKampenColimit (G.inv.mapCocone (G.mapCocone c))

Tactic:
apply (IsVanKampenColimit.precompose_isIso_iff e.inv).mp

Premises used: CategoryTheory.IsVanKampenColimit.precompose_isIso_iff, Iff.mp, 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
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
j : J
⊢ c.ι.app j ≫ Iso.hom (G.asEquivalence.unitIso.app c.pt) =
    ((Cocone.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c))).ι.app j

Tactic:
simp [e]
-- 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 : G.IsEquivalence
hc : IsVanKampenColimit c
e : F ⋙ G ⋙ G.inv ≅ F := NatIso.hcomp (Iso.refl F) G.asEquivalence.unitIso.symm
⊢ IsVanKampenColimit ((Cocone.precompose e.inv).obj (G.inv.mapCocone (G.mapCocone c)))

Tactic:
exact hc.of_iso (Cocone.ext (G.asEquivalence.unitIso.app c.pt) (fun j => (by simp [e])))
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 (Cocone.whisker e.inverse c'))

Tactic:
hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) ?_

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.NatTrans.Equifibered.whiskerLeft, CategoryTheory.CategoryStruct.comp, CategoryTheory.Equivalence.invFunIdAssoc, CategoryTheory.Iso.hom, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
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)
⊢ Nonempty (IsColimit c')

Tactic:
convert!
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _)) ?_ using 1

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.NatTrans.Equifibered.whiskerLeft, CategoryTheory.CategoryStruct.comp, CategoryTheory.Equivalence.invFunIdAssoc, CategoryTheory.Iso.hom, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))

Tactic:
(IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr

Premises used: Equiv.nonempty_congr, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr

Premises used: Equiv.nonempty_congr, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 (α ≫ (Cocone.whisker e.functor c).ι) = e.inverse.whiskerLeft (c'.ι ≫ map (const J) f)

Tactic:
congr_arg (whiskerLeft e.inverse) e'

Premises used: CategoryTheory.Functor.whiskerLeft, congr_arg, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
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).ι)
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f

Tactic:
convert! congr_arg (whiskerLeft e.inverse) e'

Premises used: CategoryTheory.Functor.whiskerLeft, congr_arg, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
h :
  ∀ (x : K),
    ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app x =
      (e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)).app x
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
x : K
⊢ ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app x =
    (e.inverse.whiskerLeft (α ≫ (Cocone.whisker e.functor c).ι)).app x

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
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
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)
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)

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
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)

Tactic:
(H (e.inverse.obj k)).paste_vert ?_

Premises used: CategoryTheory.Functor.comp, CategoryTheory.IsPullback.paste_vert, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
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)
⊢ 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:
refine (H (e.inverse.obj k)).paste_vert ?_

Premises used: CategoryTheory.IsPullback.paste_vert, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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
⊢ (Cocone.whisker e.functor c).ι.app (e.inverse.obj k) ≫ 𝟙 (Cocone.whisker e.functor c).pt =
    (e.invFunIdAssoc F).hom.app k ≫ c.ι.app k

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
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.functor c).ι.app (e.inverse.obj k)) ((e.invFunIdAssoc F).hom.app k)
    (𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)

Tactic:
exact IsPullback.of_vert_isIso ⟨by simp⟩

Premises used: CategoryTheory.IsPullback.of_vert_isIso, CategoryTheory.CommSq.mk
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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 (Cocone.whisker e.functor c)
⊢ ∀ (j : K),
    ((Cocone.precompose (e.invFunIdAssoc F).inv).obj (Cocone.whisker e.symm.functor (Cocone.whisker e.functor c))).ι.app
          j ≫
        Iso.hom
          (Iso.refl
            ((Cocone.precompose (e.invFunIdAssoc F).inv).obj
                (Cocone.whisker e.symm.functor (Cocone.whisker e.functor 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
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 (Cocone.whisker e.inverse c')) ↔
    ∀ (j : K),
      IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app j) f
        (c.ι.app j)

Tactic:
hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (.of_isIso _))

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.NatTrans.Equifibered.whiskerLeft, CategoryTheory.CategoryStruct.comp, CategoryTheory.Equivalence.invFunIdAssoc, CategoryTheory.Iso.hom, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
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)
hc₁ : (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor 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

Premises used: CategoryTheory.NatTrans.Equifibered.of_isIso, CategoryTheory.NatTrans.Equifibered.comp, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.NatTrans.Equifibered.whiskerLeft, CategoryTheory.CategoryStruct.comp, CategoryTheory.Equivalence.invFunIdAssoc, CategoryTheory.Iso.hom, CategoryTheory.Equivalence.inverse