awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} (WithInitial J) F
K : J ⥤ Under.{v₁, u₁} X
coconeK : Cocone K
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit
    (Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
      (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK)))
⊢ Eq (α :=
    (Functor.obj liftFromUnder (K ⋙ Under.post F)).obj WithInitial.star ⟶
      Cocone.pt (F := Functor.obj liftFromUnder (K ⋙ Under.post F))
        (Functor.obj (Equivalence.functor coconeEquiv) (Functor.mapCocone (Under.post F) coconeK)))
    ((Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
              (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK))).ι.app
        WithInitial.star ≫
      Iso.hom
        (Iso.refl
          (Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
              (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK))).pt))
    (NatTrans.app (Cocone.ι (Functor.obj (Equivalence.functor coconeEquiv) (Functor.mapCocone (Under.post F) coconeK)))
      WithInitial.star)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
X : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} (WithInitial J) F
K : J ⥤ Under.{v₁, u₁} X
coconeK : Cocone K
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit
    (Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
      (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK)))
a : J
⊢ Eq (α :=
    (Functor.obj liftFromUnder (K ⋙ Under.post F)).obj (of a) ⟶
      Cocone.pt (F := Functor.obj liftFromUnder (K ⋙ Under.post F))
        (Functor.obj (Equivalence.functor coconeEquiv) (Functor.mapCocone (Under.post F) coconeK)))
    ((Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
              (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK))).ι.app
        (of a) ≫
      Iso.hom
        (Iso.refl
          (Functor.obj (Cocone.precompose (Iso.hom liftFromUnderComp))
              (F.mapCocone (Functor.obj (Equivalence.functor coconeEquiv) coconeK))).pt))
    (NatTrans.app (Cocone.ι (Functor.obj (Equivalence.functor coconeEquiv) (Functor.mapCocone (Under.post F) coconeK)))
      (of a))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
J : Type w
inst_2 : LinearOrder J
G : Functor.{v, v', u, u'} C D
inst_3 : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G

Tactic:
PreservesWellOrderContinuousOfShape.preservesColimitsOfShape j hj

Premises used: CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
F : Functor.{w, v, w, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : F.IsWellOrderContinuous
inst_5 : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G

Tactic:
have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G j hj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
F : Functor.{w, v, w, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : F.IsWellOrderContinuous
inst_5 : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
this : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G
⊢ IsColimit (J := (↑(Set.Iio j) : Type w)) (F :=
    Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
              x1 < x2) (Set.principalSegIio j)) :
          (a : (↑(Set.Iio j) : Type w)) → J))
        ⋯ ⋙
      F ⋙ G)
    (PrincipalSeg.cocone (Set.principalSegIio j) (F ⋙ G))

Tactic:
exact isColimitOfPreserves G (F.isColimitOfIsWellOrderContinuous j hj)

Premises used: CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
G₁ : Functor.{v, v', u, u'} C D
G₂ : Functor.{v', v'', u', u''} D E
inst_4 : PreservesWellOrderContinuousOfShape J G₁
inst_5 : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G₁

Tactic:
have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₁ j hj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
G₁ : Functor.{v, v', u, u'} C D
G₂ : Functor.{v', v'', u', u''} D E
inst_4 : PreservesWellOrderContinuousOfShape J G₁
inst_5 : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
this : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G₁
⊢ PreservesColimitsOfShape.{w, w, v', v'', u', u''} (↑(Set.Iio j) : Type w) G₂

Tactic:
have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₂ j hj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
G₁ : Functor.{v, v', u, u'} C D
G₂ : Functor.{v', v'', u', u''} D E
inst_4 : PreservesWellOrderContinuousOfShape J G₁
inst_5 : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
this_1 : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G₁
this : PreservesColimitsOfShape.{w, w, v', v'', u', u''} (↑(Set.Iio j) : Type w) G₂
⊢ PreservesColimitsOfShape.{w, w, v, v'', u, u''} (↑(Set.Iio j) : Type w) (G₁ ⋙ G₂)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
K : Type u_1
inst_5 : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
K : Type u_1
inst_5 : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
⊢ PreservesColimitsOfShape (C := Functor.{v_1, v, u_1, u} K C) (↑(Set.Iio j) : Type w) (Functor.obj (evaluation K C) X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C

Tactic:
have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
⊢ PreservesColimitsOfShape (C := Arrow.{v, u} C) (↑(Set.Iio j) : Type w) Arrow.leftFunc

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
⊢ PreservesColimitsOfShape (C := Arrow.{v, u} C) (↑(Set.Iio j) : Type w) Arrow.rightFunc

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
refine_1 : Discrete.functor f ⋙ G ≅ Discrete.functor fun (j : J) ↦ G.obj (f j)
refine_2 :
  Iso (C := Cone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
    (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
      (G.mapCone (Fan.mk P g)))
    (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃
    IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))

Tactic:
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.trans, CategoryTheory.Limits.IsLimit.equivIsoLimit, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ Discrete.functor f ⋙ G ≅ Discrete.functor fun (j : J) ↦ G.obj (f j)

Tactic:
exact Discrete.natIso fun j => Iso.refl (G.obj (f j.as))

Premises used: CategoryTheory.Discrete.natIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
dsimp : G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)
⊢ NatTrans.app
      (Cone.π
        (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
          (G.mapCone (Fan.mk P g))))
      j =
    Iso.hom
        (Iso.refl
          (Cone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
            (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCone (Fan.mk P g))))) ≫
      NatTrans.app (Cone.π (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))) j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
mk :
  ∀ (as : J),
    G.map (g { as := as : Discrete J }.as) ≫ 𝟙 (G.obj (f { as := as : Discrete J }.as)) =
      𝟙 (G.obj P) ≫ G.map (g { as := as }.as)
⊢ G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
as : J
⊢ G.map (g { as := as : Discrete J }.as) ≫ 𝟙 (G.obj (f { as := as : Discrete J }.as)) =
    𝟙 (G.obj P) ≫ G.map (g { as := as }.as)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ Iso (C := Cone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
    (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
      (G.mapCone (Fan.mk P g)))
    (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))

Tactic:
exact Cone.ext (Iso.refl _) fun j ↦ by dsimp; cases j; simp

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
apply : IsLimit (G.mapCone (Fan.mk (piObj.{w, v₁, u₁} f) (Pi.π f)))
⊢ PreservesLimit (Discrete.functor f) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (productIsProduct f)

Premises used: CategoryTheory.Limits.productIsProduct, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
apply :
  IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
    (Fan.mk (G.obj (piObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Pi.π f j))
⊢ IsLimit (G.mapCone (Fan.mk (piObj.{w, v₁, u₁} f) (Pi.π f)))

Tactic:
apply (isLimitMapConeFanMkEquiv _ _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConeFanMkEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
⊢ IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
    (Fan.mk (G.obj (piObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Pi.π f j))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _
    (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
j : J
⊢ Eq (α := (piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) ⟶ G.obj (f j))
    (CategoryStruct.comp (Y := G.obj (piObj.{w, v₁, u₁} f)) (inv (piComparison G f)) (G.map (Pi.π f j)))
    (Pi.π (fun (x : J) ↦ G.obj (f x)) j)

Tactic:
simp only [IsIso.inv_comp_eq, piComparison_comp_π]

Premises used: CategoryTheory.Limits.piComparison_comp_π, CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : PreservesLimit (Discrete.functor f) G
⊢ Eq (α := G.obj (piObj.{w, v₁, u₁} f) ⟶ piObj.{w, v₂, u₂} fun (j : J) ↦ G.obj (f j)) (Iso.hom (iso G f))
    (piComparison G f)

Tactic:
rfl

Premises used: CategoryTheory.Limits.piComparison, CategoryTheory.Limits.limit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : PreservesLimit (Discrete.functor f) G
⊢ IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b))
    (Iso.hom (PreservesProduct.iso G f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
inst_4 : PreservesLimit (Discrete.functor f) G
I : Type u_1
inst_5 : Category.{v_1, u_1} I
inst_6 : IsGroupoid.{v_1, u_1} I
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : PreservesLimitsOfShape.{v_1, u_1, v₁, v₂, u₁, u₂} I F
⊢ PreservesLimitsOfShape.{v_1, u_1, v₁, v₂, u₁, u₂} Iᵒᵖ F

Tactic:
letI : Groupoid I := Groupoid.ofIsGroupoid
  preservesLimitsOfShape_of_equiv (Groupoid.invEquivalence I) F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.Groupoid.invEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
refine_1 : (Discrete.functor fun (j : J) ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G
refine_2 :
  Iso (C := Cocone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
    (Functor.obj (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
      (G.mapCocone (Cofan.mk P g)))
    (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃
    IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))

Tactic:
refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)

Premises used: Equiv.trans, CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ (Discrete.functor fun (j : J) ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G

Tactic:
refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))

Premises used: CategoryTheory.Discrete.natIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
dsimp : (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
        (Functor.obj (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
          (G.mapCocone (Cofan.mk P g))))
      (NatTrans.app
          (Cocone.ι
            (Functor.obj
              (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCocone (Cofan.mk P g))))
          j :
        Functor.obj.{w, v₂, w, u₂} (Discrete.functor fun (j : J) ↦ G.obj (f j)) j ⟶
          Functor.obj.{w, v₂, w, u₂}
            (Functor.obj (Functor.const (Discrete J))
              (Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
                (Functor.obj
                  (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
                  (G.mapCocone (Cofan.mk P g)))))
            j)
      (Iso.hom
        (Iso.refl
          (Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
            (Functor.obj
              (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCocone (Cofan.mk P g)))))) =
    NatTrans.app (Cocone.ι (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))) j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
mk :
  ∀ (as : J),
    (𝟙 (G.obj (f { as := as : Discrete J }.as)) ≫ G.map (g { as := as : Discrete J }.as)) ≫ 𝟙 (G.obj P) =
      G.map (g { as := as }.as)
⊢ (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
as : J
⊢ (𝟙 (G.obj (f { as := as : Discrete J }.as)) ≫ G.map (g { as := as : Discrete J }.as)) ≫ 𝟙 (G.obj P) =
    G.map (g { as := as }.as)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ Iso (C := Cocone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
    (Functor.obj (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
      (G.mapCocone (Cofan.mk P g)))
    (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))

Tactic:
refine Cocone.ext (Iso.refl _) fun j => by dsimp; cases j; simp

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
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
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
apply : IsColimit (G.mapCocone (Cofan.mk (sigmaObj.{w, v₁, u₁} f) (Sigma.ι f)))
⊢ PreservesColimit (Discrete.functor f) G

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coproductIsCoproduct f)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone