awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
H : Type u₂
inst_1 : Category.{v₂, u₂} H
J : Type u₃
inst_2 : Category.{v₃, u₃} J
F : C ⥤ Cat
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_6 : PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} C H) J colim
inst_7 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := limit ((K ⋙ fiberwiseColim F H) ⋙ colim))
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (limit (K ⋙ fiberwiseColim F H)))
      (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (fiberwiseColimit (limit K)))
          (Trans.trans (r := Eq) (s := Iso) (t := Iso) ⋯ (Iso.symm (colimitFiberwiseColimitIso (limit K))) :
            colimit (limit K) ≅ colimit (fiberwiseColimit (limit K)))
          (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K) :
            colimit (fiberwiseColimit (limit K)) ≅ colimit (limit (K ⋙ fiberwiseColim F H))) :
        colimit (limit K) ≅ colimit (limit (K ⋙ fiberwiseColim F H)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H) :
        obj colim (limit (K ⋙ fiberwiseColim F H)) ≅ limit ((K ⋙ fiberwiseColim F H) ⋙ colim)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
⊢ IsIso (X := obj colim (limit K)) (Y := limit (K ⋙ colim)) (limit.post K colim)
have h : obj colim (limit K) = colimit (limit K) → limit.post K colim = i₂.hom
Tactic: convert! Iso.isIso_hom i₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
H : Type u₂
inst_1 : Category.{v₂, u₂} H
J : Type u₃
inst_2 : Category.{v₃, u₃} J
F : C ⥤ Cat
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_6 : PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} C H) J colim
inst_7 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := limit ((K ⋙ fiberwiseColim F H) ⋙ colim))
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (limit (K ⋙ fiberwiseColim F H)))
      (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (fiberwiseColimit (limit K)))
          (Trans.trans (r := Eq) (s := Iso) (t := Iso) ⋯ (Iso.symm (colimitFiberwiseColimitIso (limit K))) :
            colimit (limit K) ≅ colimit (fiberwiseColimit (limit K)))
          (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K) :
            colimit (fiberwiseColimit (limit K)) ≅ colimit (limit (K ⋙ fiberwiseColim F H))) :
        colimit (limit K) ≅ colimit (limit (K ⋙ fiberwiseColim F H)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H) :
        obj colim (limit (K ⋙ fiberwiseColim F H)) ≅ limit ((K ⋙ fiberwiseColim F H) ⋙ colim)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3 : obj colim (limit K) = colimit (limit K)
⊢ limit.post K colim = i₂.hom
have h : ∀ (j : J),
  CategoryStruct.comp (Y := limit (K ⋙ colim)) (limit.post K colim) (limit.π (K ⋙ colim) j) =
    i₂.hom ≫ limit.π (K ⋙ colim) j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Grothendieck (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
H : Type u₂
inst_1 : Category.{v₂, u₂} H
J : Type u₃
inst_2 : Category.{v₃, u₃} J
F : C ⥤ Cat
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_6 : PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} C H) J colim
inst_7 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := limit ((K ⋙ fiberwiseColim F H) ⋙ colim))
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (limit (K ⋙ fiberwiseColim F H)))
      (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (fiberwiseColimit (limit K)))
          (Trans.trans (r := Eq) (s := Iso) (t := Iso) ⋯ (Iso.symm (colimitFiberwiseColimitIso (limit K))) :
            colimit (limit K) ≅ colimit (fiberwiseColimit (limit K)))
          (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K) :
            colimit (fiberwiseColimit (limit K)) ≅ colimit (limit (K ⋙ fiberwiseColim F H))) :
        colimit (limit K) ≅ colimit (limit (K ⋙ fiberwiseColim F H)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H) :
        obj colim (limit (K ⋙ fiberwiseColim F H)) ≅ limit ((K ⋙ fiberwiseColim F H) ⋙ colim)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
⊢ PreservesLimit K colim
have this : IsIso (X := obj colim (limit K)) (Y := limit (K ⋙ colim)) (limit.post K colim)
Tactic: haveI : IsIso (limit.post K colim) := by
    convert! Iso.isIso_hom i₂
    ext
    simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.trans_def,
      Iso.trans_assoc, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π,
      fiberwiseColim_obj, isoWhiskerLeft_hom, NatTrans.comp_app, Functor.associator_hom_app,
      whiskerLeft_app, fiberwiseColimCompColimIso_hom_app, Category.id_comp,
      preservesLimitIso_hom_π_assoc, i₂]
    ext
    simp only [ι_colimMap, Trans.trans, Iso.symm_hom, ι_colimitFiberwiseColimitIso_inv_assoc,
      HasColimit.isoOfNatIso_ι_hom_assoc, fiberwiseColimit_obj, fiberwiseColimitLimitIso_hom_app,
      ι_colimMap_assoc, Category.assoc, limitObjIsoLimitCompEvaluation_inv_π_app_assoc,
      Functor.comp_obj, fiberwiseColim_obj, HasLimit.isoOfNatIso_hom_π_assoc,
      whiskeringLeft_obj_obj, colim_obj, evaluation_obj_obj, Iso.trans_hom, isoWhiskerLeft_hom,
      NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      fiberwiseColimCompEvaluationIso_inv_app, Functor.associator_inv_app, Category.comp_id,
      Category.id_comp, preservesLimitIso_hom_π_assoc, colim_map, Grothendieck.ι_obj,
      ι_colimitFiberwiseColimitIso_hom]
    simp [← Category.assoc, ← NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesLimit F G
inst_4 : HasLimit F
t : Cone F
⊢ Eq (α := G.obj t.pt ⟶ limit (F ⋙ G))
    (CategoryStruct.comp (Y := G.obj (limit F)) (G.map (limit.lift F t)) (Iso.hom (preservesLimitIso G F)) :
      G.obj t.pt ⟶ limit (F ⋙ G))
    (limit.lift (F ⋙ G) (G.mapCone t) : (G.mapCone t).pt ⟶ limit (F ⋙ G))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := limit (F ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit F)) (G.map (limit.lift F t)) (Iso.hom (preservesLimitIso G F)) :
        G.obj t.pt ⟶ limit (F ⋙ G))
      (limit.π (F ⋙ G) j : limit (F ⋙ G) ⟶ (F ⋙ G).obj j) =
    CategoryStruct.comp (Y := limit (F ⋙ G)) (limit.lift (F ⋙ G) (G.mapCone t)) (limit.π (F ⋙ G) j)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesLimit F G
inst_4 : HasLimit F
inst_5 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasLimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasLimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
⊢ Eq (α := Functor.obj (lim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) Y)
    (Functor.map (lim ⋙ G) f ≫
      Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) Y))
    (Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) X) ≫
      Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) f)
have w : ∀ (j : J),
  Eq (α := Functor.obj (lim ⋙ G) X ⟶ (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y).obj j)
    (CategoryStruct.comp (Y := limit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y))
      (Functor.map (lim ⋙ G) f ≫
        Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) Y))
      (limit.π (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y) j))
    (CategoryStruct.comp (Y := limit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y))
      (Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) X) ≫
          Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) f :
        Functor.obj (lim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) Y)
      (limit.π (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y) j))
Tactic: apply limit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesLimit F G
inst_4 : HasLimit F
inst_5 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasLimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasLimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := Functor.obj (lim ⋙ G) X ⟶ (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y).obj j)
    (CategoryStruct.comp (Y := limit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y))
      (Functor.map (lim ⋙ G) f ≫
        Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) Y))
      (limit.π (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y) j))
    (CategoryStruct.comp (Y := limit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y))
      (Iso.hom ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesLimitIso G F : G.obj (limit F) ≅ limit (F ⋙ G))) X) ≫
          Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) f :
        Functor.obj (lim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ lim) Y)
      (limit.π (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) Y) j))
have w : Eq (α := G.obj (limit X) ⟶ G.obj (Y.obj j))
  (CategoryStruct.comp (Y := limit (Y ⋙ G))
    (CategoryStruct.comp (Y := G.obj (limit Y)) (G.map (limMap f)) (Iso.hom (preservesLimitIso G Y)) :
      G.obj (limit X) ⟶ limit (Y ⋙ G))
    (limit.π (Y ⋙ G) j : limit (Y ⋙ G) ⟶ (Y ⋙ G).obj j))
  (CategoryStruct.comp (Y := limit (Y ⋙ G))
    (CategoryStruct.comp (Y := limit (X ⋙ G)) (Iso.hom (preservesLimitIso G X) : G.obj (limit X) ⟶ limit (X ⋙ G))
      (limMap (Functor.whiskerRight f G) : limit (X ⋙ G) ⟶ limit (Y ⋙ G)))
    (limit.π (Y ⋙ G) j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasLimit F
inst_4 : HasLimit (F ⋙ G)
inst_5 : IsIso (X := G.obj (limit F)) (Y := limit (F ⋙ G)) (limit.post F G)
⊢ IsLimit (G.mapCone (limit.cone F))
have convert_2 : IsIso (X := (G.mapCone (limit.cone F)).pt) (Y := (limit.cone (F ⋙ G)).pt)
  (IsLimit.lift (limit.isLimit (F ⋙ G)) (G.mapCone (limit.cone F)))
Tactic: convert! IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
t : Cocone F
⊢ Eq (α := colimit (F ⋙ G) ⟶ G.obj t.pt)
    (CategoryStruct.comp (Y := G.obj (colimit F)) (Iso.inv (preservesColimitIso G F)) (G.map (colimit.desc F t)) :
      colimit (F ⋙ G) ⟶ G.obj t.pt)
    (colimit.desc (F ⋙ G) (G.mapCocone t) : colimit (F ⋙ G) ⟶ (G.mapCocone t).pt)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j : (F ⋙ G).obj j ⟶ colimit (F ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit F)) (Iso.inv (preservesColimitIso G F)) (G.map (colimit.desc F t)) :
        colimit (F ⋙ G) ⟶ G.obj t.pt) =
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j) (colimit.desc (F ⋙ G) (G.mapCocone t))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
⊢ Eq (α := Functor.obj (colim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) Y)
    (Functor.map (colim ⋙ G) f ≫
      Iso.hom
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
    (Iso.hom
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
      Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f)
have rw : Eq (α := Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) X ⟶ Functor.obj (colim ⋙ G) Y)
  (Iso.inv
      ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
    Functor.map (colim ⋙ G) f)
  (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
    Iso.inv
      ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
Tactic: rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
⊢ Eq (α := Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) X ⟶ Functor.obj (colim ⋙ G) Y)
    (Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
      Functor.map (colim ⋙ G) f)
    (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
      Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
have w : ∀ (j : J),
  Eq (α := (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X).obj j ⟶ Functor.obj (colim ⋙ G) Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            X) ≫
        Functor.map (colim ⋙ G) f))
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
        Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            Y)))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X).obj j ⟶ Functor.obj (colim ⋙ G) Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            X) ≫
        Functor.map (colim ⋙ G) f))
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
        Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            Y)))
have w : Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
  (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
    (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
      colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
  (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j)
    (CategoryStruct.comp (Y := colimit (Y ⋙ G))
      (colimMap (Functor.whiskerRight f G) : colimit (X ⋙ G) ⟶ colimit (Y ⋙ G))
      (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (Y ⋙ G))
        (colimMap (Functor.whiskerRight f G) : colimit (X ⋙ G) ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y))))
have w : Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
  (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
    (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
      colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
  ((Functor.whiskerRight f G).app j ≫
    CategoryStruct.comp (Y := colimit (Y ⋙ G)) (colimit.ι (Y ⋙ G) j : (Y ⋙ G).obj j ⟶ colimit (Y ⋙ G))
      (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y)))
Tactic: rw [ι_colimMap_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    ((Functor.whiskerRight f G).app j ≫
      CategoryStruct.comp (Y := colimit (Y ⋙ G)) (colimit.ι (Y ⋙ G) j : (Y ⋙ G).obj j ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y)))
have w : Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
  (G.map (CategoryStruct.comp (Y := colimit X) (colimit.ι X j) (colimMap f))) (G.map (f.app j ≫ colimit.ι Y j))
Tactic: simp only [ι_preservesColimitIso_inv, Functor.whiskerRight_app,
        ι_preservesColimitIso_inv_assoc, ← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (G.map (CategoryStruct.comp (Y := colimit X) (colimit.ι X j) (colimMap f))) (G.map (f.app j ≫ colimit.ι Y j))
have w : Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y)) (G.map (f.app j ≫ colimit.ι Y j)) (G.map (f.app j ≫ colimit.ι Y j))
Tactic: rw [ι_colimMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Limits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasColimit F
inst_4 : HasColimit (F ⋙ G)
inst_5 : IsIso (X := colimit (F ⋙ G)) (Y := G.obj (colimit F)) (colimit.post F G)
⊢ IsColimit (G.mapCocone (colimit.cocone F))
have convert_2 : IsIso (X := (colimit.cocone (F ⋙ G)).pt) (Y := (G.mapCocone (colimit.cocone F)).pt)
  (IsColimit.desc (colimit.isColimit (F ⋙ G)) (G.mapCocone (colimit.cocone F)))
Tactic: convert! IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F.op
have inst : PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesLimitsOfShape_op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_2 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.leftOp
have inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
Tactic: apply +allowSynthFailures preservesLimitsOfShape_leftOp