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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
have refine : Nonempty (IsColimit c') → ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
Tactic: refine ⟨?_, H.isUniversal.map_reflective adj c' α f h hα⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
have hα' : NatTrans.Equifibered α'
Tactic: have hα' : NatTrans.Equifibered α' := 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
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j_1 : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
⊢ Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
have rw : Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
Tactic: rw [← cancel_mono (adj.counit.app <| F.obj j)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j_1 : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
j : J
⊢ Gl.map (Gr.map (α'.app j)) ≫ adj.counit.app (F.obj j) = (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
have dsimp : Gl.map (Gr.map (α.app j ≫ 𝟙 (Gl.obj (Gr.obj (F.obj j))) ≫ adj.counit.app (F.obj j) ≫ 𝟙 (F.obj j))) ≫
    adj.counit.app (F.obj j) =
  (adj.counit.app (F'.1 j) ≫ α.app j) ≫ adj.counit.app (F.obj j)
Tactic: dsimp [α']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
have hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
Tactic: have hα'' : ∀ j, Gl.map (Gr.map <| α'.app j) = adj.counit.app _ ≫ α.app j := by
    intro j
    rw [← cancel_mono (adj.counit.app <| F.obj j)]
    dsimp [α']
    simp only [Category.comp_id, Adjunction.counit_naturality_assoc, Category.id_comp,
      Adjunction.counit_naturality, Category.assoc, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
⊢ α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
have rw : α.app j = β.inv.app j ≫ adj.counit.app (F'.1 j) ≫ α.app j
Tactic: rw [hα'']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
have this₁ : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
Tactic: have : α.app j = β.inv.app _ ≫ Gl.map (Gr.map <| α'.app j) := by
    rw [hα'']
    simp [β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
have rw : IsPullback (c'.ι.app j) (β.inv.app j ≫ Gl.map (Gr.map (α'.app j))) f ((Gl.mapCocone c).ι.app j)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
⊢ f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
have symm : (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }) = f
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
⊢ (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }) =
    f
have h₁ : (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶
      (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt) →
  Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt =
      (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt →
    Eq (α :=
      (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))).pt ⟶
        Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt)
      (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
      (hr.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
Tactic: convert!
      @IsColimit.coconePointUniqueUpToIso_hom_desc _ _ _ _ ((F' ⋙ Gr) ⋙ Gl)
        (Gl.mapCocone ⟨_, (whiskerRight α' Gr ≫ c.2 :)⟩) _ _ hl hr using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
h₁ :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
      (((Cocone.precompose β.hom).obj c').pt ⟶
        (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt) →
    Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt =
        (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt →
      Eq (α :=
        (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))).pt ⟶
          Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt)
        (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
        (hr.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
⊢ (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }) =
    f
have h₂ : (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶
      (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt) →
  f = hl.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
Tactic: convert!
      @IsColimit.coconePointUniqueUpToIso_hom_desc _ _ _ _ ((F' ⋙ Gr) ⋙ Gl)
        (Gl.mapCocone ⟨_, (whiskerRight α' Gr ≫ c.2 :)⟩) _ _ hl hr using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
e_1 :
  (c'.pt ⟶ (Gl.mapCocone c).pt) =
    (((Cocone.precompose β.hom).obj c').pt ⟶
      (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt)
e_5 :
  Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt =
    (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }).pt
⊢ Eq (α :=
    (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))).pt ⟶
      Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt)
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
    (hr.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
have h₁ : ∀ (j : J),
  Eq (α := ((F' ⋙ Gr) ⋙ Gl).obj j ⟶ Gl.obj { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι : Cocone (F' ⋙ Gr) }.pt)
    ((Gl.mapCocone (colimit.cocone (F' ⋙ Gr))).ι.app j ≫
      Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
    ((Gl.mapCocone (colimit.cocone (F' ⋙ Gr))).ι.app j ≫
      hr.desc (Gl.mapCocone { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
Tactic: apply hr.hom_ext