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
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') ↔ 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 : 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') ↔ 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 : 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 ((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:
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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.Cocone.whisker_pt, CategoryTheory.Limits.Cocone.whisker_ι, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Equivalence.invFunIdAssoc_hom_app, CategoryTheory.Functor.id_obj, 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
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)
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))
⊢ (∀ (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
-- 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 : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
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)
⊢ IsPullback (c'.ι.app (e.inverse.obj k)) (α.app (e.inverse.obj k) ≫ F.map (e.counit.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 : 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)

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 : 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
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)
⊢ 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:
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 : 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
⊢ IsIso.{v, u} (𝟙 (Cocone.whisker e.functor c).pt)

Tactic:
have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance
-- 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 : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))
k : K
this : IsIso.{v, u} (𝟙 (Cocone.whisker e.functor c).pt)
⊢ c.ι.app (e.functor.obj (e.inverse.obj k)) ≫ 𝟙 (Cocone.whisker e.functor c).pt = F.map (e.counit.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 : 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
this : IsIso.{v, u} (𝟙 (Cocone.whisker e.functor c).pt)
⊢ 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:
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 : 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
⊢ α.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:
simp [← Functor.map_comp]

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
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
⊢ α.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]
-- 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 : ∀ (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))
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))
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))

Tactic:
rw [← Category.id_comp f, this]

Premises used: CategoryTheory.Category.id_comp
-- 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 : ∀ (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))

Tactic:
IsPullback.paste_vert ?_ (H (e.functor.obj j))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.IsPullback.paste_vert, CategoryTheory.Functor.obj
-- 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 : ∀ (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))
h : IsPullback (c'.ι.app j) (F'.map (e.unit.app j)) (𝟙 c'.pt) (c'.ι.app (e.inverse.obj (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))

Tactic:
refine IsPullback.paste_vert ?_ (H (e.functor.obj j))

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.IsPullback.paste_vert, CategoryTheory.Functor.obj
-- 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 : ∀ (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))
⊢ c'.ι.app j ≫ 𝟙 c'.pt = F'.map (e.unit.app j) ≫ c'.ι.app (e.inverse.obj (e.functor.obj 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 α
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)) (𝟙 c'.pt) (c'.ι.app (e.inverse.obj (e.functor.obj j)))

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 : 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 α
w :
  ∀ (k : K),
    ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app k =
      ((Cocone.whisker e.inverse c').ι ≫ map (const K) f).app k
⊢ (e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ map (const K) f

Tactic:
ext k
-- 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 α
k : K
⊢ ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι).app k =
    ((Cocone.whisker e.inverse c').ι ≫ map (const K) f).app k

Tactic:
simpa using congr_app e' (e.inverse.obj k)

Premises used: CategoryTheory.congr_app, 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 : IsVanKampenColimit (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
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
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)
⊢ 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)))

Tactic:
ext y
-- 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
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
w : (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x
⊢ 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:
dsimp
-- 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
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
⊢ (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x

Tactic:
NatTrans.congr_app (NatTrans.congr_app e y) x

Premises used: CategoryTheory.NatTrans.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
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
⊢ (α.app y).app x ≫ (c.ι.app y).app x = (c'.ι.app y).app x ≫ f.app x

Tactic:
exact NatTrans.congr_app (NatTrans.congr_app e y) x

Premises used: CategoryTheory.NatTrans.congr_app