awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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
preservesLimit :
  autoParam (∀ {K : J ⥤ Grothendieck F ⥤ H}, PreservesLimit K colim) PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape (C := Grothendieck F ⥤ H) J colim

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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 i₂.hom

Tactic:
Iso.isIso_hom i₂

Premises used: CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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))
h : obj colim (limit K) = colimit (limit K) → limit.post K colim = i₂.hom
⊢ IsIso (X := obj colim (limit K)) (Y := limit (K ⋙ colim)) (limit.post K colim)

Tactic:
convert! Iso.isIso_hom i₂

Premises used: CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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)
h :
  ∀ (j : J),
    CategoryStruct.comp (Y := limit (K ⋙ colim)) (limit.post K colim) (limit.π (K ⋙ colim) j) =
      i₂.hom ≫ limit.π (K ⋙ colim) j
⊢ limit.post K colim = i₂.hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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)
j : J
j_1 : Grothendieck F
⊢ Eq (α := (limit K).obj j_1 ⟶ colimit (K.obj j)) (NatTrans.app (limit.π K j) j_1 ≫ colimit.ι (K.obj j) j_1)
    (CategoryStruct.comp (Y :=
      obj
        (limit (K ⋙ obj (whiskeringLeft (↑(F.obj j_1.base) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F j_1.base)))
        j_1.fiber)
      (NatTrans.app (Iso.inv (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F j_1.base))) j_1.fiber)
      (NatTrans.app
          (limit.π
            (K ⋙ obj (whiskeringLeft (↑(F.obj j_1.base) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F j_1.base)) j)
          j_1.fiber ≫
        colimit.ι (K.obj j) { base := j_1.base, fiber := j_1.fiber }))

Tactic:
simp [← Category.assoc, ← NatTrans.comp_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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)

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]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
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))
this : IsIso (X := obj colim (limit K)) (Y := limit (K ⋙ colim)) (limit.post K colim)
⊢ PreservesLimit K colim

Tactic:
apply preservesLimit_of_isIso_post

Premises used: CategoryTheory.preservesLimit_of_isIso_post
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (t.lift c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
j : J
⊢ Eq (α := G.obj (limit F) ⟶ (F ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (Iso.hom (preservesLimitIso G F) : G.obj (limit F) ⟶ limit (F ⋙ G))
      (limit.π (F ⋙ G) j : limit (F ⋙ G) ⟶ (F ⋙ G).obj j))
    (G.map (limit.π F j))

Tactic:
IsLimit.conePointUniqueUpToIso_hom_comp _ _ j

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.limit
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
j : J
⊢ Eq (α := limit (F ⋙ G) ⟶ G.obj (F.obj j))
    (CategoryStruct.comp (Y := G.obj (limit F)) (Iso.inv (preservesLimitIso G F)) (G.map (limit.π F j)) :
      limit (F ⋙ G) ⟶ G.obj (F.obj j))
    (limit.π (F ⋙ G) j : limit (F ⋙ G) ⟶ (F ⋙ G).obj j)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ j

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
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:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
⊢ IsIso (X := G.obj (limit F)) (Y := limit (F ⋙ G)) (limit.post F G)

Tactic:
show IsIso (preservesLimitIso G F).hom from inferInstance

Premises used: CategoryTheory.Limits.limit.post, inferInstance, CategoryTheory.Limits.limit.lift
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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 : Functor.{w', v₁, w, u₁} J C
_ :
  ∀ {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)
⊢ ∀ {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)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
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))
⊢ 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)

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
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
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))
⊢ 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:
dsimp