awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
⟨fun _ => preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda A,
   fun _ => isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A⟩

Premises used: CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits, CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ Eq (α := F.obj Y ⟶ cokernel (F.map f))
    (CategoryStruct.comp (Y := F.obj (cokernel f)) (F.map (cokernel.π f)) (Iso.hom (PreservesCokernel.iso F f)))
    (Iso.hom (Iso.refl (F.obj Y)) ≫ cokernel.π (F.map f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ Eq (α := F.obj (Abelian.image f) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := Abelian.image (F.map f)) (Iso.hom (iso F f)) (image.ι (F.map f))) (F.map (image.ι f))

Tactic:
simp [iso]

Premises used: CategoryTheory.Abelian.PreservesImage.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
      (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (Abelian.factorThruImage f)) (Iso.hom (iso F f)))
      (equalizer.ι (cokernel.π (F.map f)) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
      (Abelian.factorThruImage (F.map f)) (equalizer.ι (cokernel.π (F.map f)) 0)
⊢ Eq (α := F.obj X ⟶ Abelian.image (F.map f))
    (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (Abelian.factorThruImage f)) (Iso.hom (iso F f)))
    (Abelian.factorThruImage (F.map f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
      (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (Abelian.factorThruImage f)) (Iso.hom (iso F f)))
      (equalizer.ι (cokernel.π (F.map f)) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (F.map f)) (cokernel.π (F.map f)) 0)
      (Abelian.factorThruImage (F.map f)) (equalizer.ι (cokernel.π (F.map f)) 0)

Tactic:
simp [iso]

Premises used: CategoryTheory.Abelian.PreservesImage.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ Eq (α := Abelian.image (F.map f) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (Iso.inv (iso F f)) (F.map (image.ι f))) (image.ι (F.map f))

Tactic:
simp [iso]

Premises used: CategoryTheory.Abelian.PreservesImage.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_7 : PreservesColimit (parallelPair f 0) F
inst_8 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_9 : HasCokernel (F.map f)
inst_10 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
⊢ Eq (α := F.obj X ⟶ F.obj (Abelian.image f))
    (CategoryStruct.comp (Y := Abelian.image (F.map f)) (Abelian.factorThruImage (F.map f)) (Iso.inv (iso F f)))
    (F.map (Abelian.factorThruImage f))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := F.obj (kernel f) ⟶ F.obj X) (F.map (kernel.ι f) ≫ Iso.hom (Iso.refl (F.obj X)))
    (CategoryStruct.comp (Y := kernel (F.map f)) (Iso.hom (PreservesKernel.iso F f)) (kernel.ι (F.map f)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := F.obj X ⟶ Abelian.coimage (F.map f))
    (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (F.map (coimage.π f)) (Iso.hom (iso F f)))
    (coimage.π (F.map f))

Tactic:
simp [iso]

Premises used: CategoryTheory.Abelian.PreservesCoimage.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
h :
  CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
      (coequalizer.π (kernel.ι (F.map f)) 0)
      (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (Iso.inv (iso F f)) (F.map (Abelian.factorThruCoimage f))) =
    CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
      (coequalizer.π (kernel.ι (F.map f)) 0) (Abelian.factorThruCoimage (F.map f))
⊢ Eq (α := Abelian.coimage (F.map f) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (Iso.inv (iso F f)) (F.map (Abelian.factorThruCoimage f)))
    (Abelian.factorThruCoimage (F.map f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
      (coequalizer.π (kernel.ι (F.map f)) 0)
      (CategoryStruct.comp (Y := F.obj (Abelian.coimage f)) (Iso.inv (iso F f)) (F.map (Abelian.factorThruCoimage f))) =
    CategoryStruct.comp (Y := coequalizer (X := kernel (F.map f)) (kernel.ι (F.map f)) 0)
      (coequalizer.π (kernel.ι (F.map f)) 0) (Abelian.factorThruCoimage (F.map f))

Tactic:
simp [iso]

Premises used: CategoryTheory.Abelian.PreservesCoimage.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := F.obj (Abelian.coimage f) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := Abelian.coimage (F.map f)) (Iso.hom (iso F f)) (Abelian.factorThruCoimage (F.map f)))
    (F.map (Abelian.factorThruCoimage f))

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel (X := kernel f) (kernel.ι f)
inst_7 : PreservesLimit (parallelPair f 0) F
inst_8 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_9 : HasKernel (F.map f)
inst_10 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := F.obj X ⟶ F.obj (Abelian.coimage f))
    (CategoryStruct.comp (Y := Abelian.coimage (F.map f)) (coimage.π (F.map f)) (Iso.inv (iso F f)))
    (F.map (coimage.π f))

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasKernel f
inst_6 : HasCokernel f
inst_7 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_8 : HasCokernel (X := kernel f) (kernel.ι f)
inst_9 : PreservesLimit (parallelPair f 0) F
inst_10 : PreservesColimit (parallelPair f 0) F
inst_11 : PreservesLimit (parallelPair (Y := cokernel f) (cokernel.π f) 0) F
inst_12 : PreservesColimit (parallelPair (X := kernel f) (kernel.ι f) 0) F
inst_13 : HasKernel (Y := cokernel (F.map f)) (cokernel.π (F.map f))
inst_14 : HasCokernel (X := kernel (F.map f)) (kernel.ι (F.map f))
⊢ Eq (α := F.obj (Abelian.coimage f) ⟶ Abelian.image (F.map f))
    (CategoryStruct.comp (Y := Abelian.coimage (F.map f)) (Iso.hom (iso F f)) (coimageImageComparison (F.map f)))
    (CategoryStruct.comp (Y := F.obj (Abelian.image f)) (F.map (coimageImageComparison f))
      (Iso.hom (PreservesImage.iso F f)))

Tactic:
simp [← Functor.map_comp, ← Iso.eq_inv_comp, ← cancel_epi (Abelian.coimage.π (F.map f)),
    ← cancel_mono (Abelian.image.ι (F.map f))]

Premises used: CategoryTheory.Abelian.coimage.π, CategoryTheory.Abelian.image.ι, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.eq_inv_comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ Eq (α :=
    Functor.obj.{0, v₂, 0, u₂}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₂, 0, u₂}
        (pair ((pair X Y ⋙ G).obj { as := WalkingPair.left }) ((pair X Y ⋙ G).obj { as := WalkingPair.right }))
        { as := WalkingPair.left : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app
      { as := WalkingPair.left })
    (Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt) ≫
      (BinaryFan.mk (G.map f) (G.map g)).π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ Eq (α :=
    Functor.obj.{0, v₂, 0, u₂}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v₂, 0, u₂}
        (pair ((pair X Y ⋙ G).obj { as := WalkingPair.left }) ((pair X Y ⋙ G).obj { as := WalkingPair.right }))
        { as := WalkingPair.right : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app
      { as := WalkingPair.right })
    (Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt) ≫
      (BinaryFan.mk (G.map f) (G.map g)).π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : PreservesLimit (pair X Y) G
⊢ HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)

Tactic:
⟨_, isLimitOfHasBinaryProductOfPreservesLimit G X Y⟩

Premises used: CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
apply : IsLimit (F := pair X Y ⋙ G) (G.mapCone (BinaryFan.mk (P := prod.{v₁, u₁} X Y) prod.fst prod.snd))
⊢ PreservesLimit (pair X Y) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)

Premises used: CategoryTheory.Limits.prodIsProd, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
apply :
  IsLimit (F := pair (G.obj X) (G.obj Y))
    (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd))
⊢ IsLimit (F := pair X Y ⋙ G) (G.mapCone (BinaryFan.mk (P := prod.{v₁, u₁} X Y) prod.fst prod.snd))

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

Premises used: CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
refine :
  IsIso (X :=
    Cone.pt (F := pair (G.obj X) (G.obj Y))
      (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))
    (Y := Cone.pt.{0, v₂, 0, u₂} (F := pair (G.obj X) (G.obj Y)) (limit.cone (pair (G.obj X) (G.obj Y))))
    (IsLimit.lift (limit.isLimit (pair (G.obj X) (G.obj Y)))
      (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))
⊢ IsLimit (F := pair (G.obj X) (G.obj Y))
    (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd))

Tactic:
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.pair, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.ofPointIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
i : IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
⊢ IsIso (X :=
    Cone.pt (F := pair (G.obj X) (G.obj Y))
      (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))
    (Y := Cone.pt.{0, v₂, 0, u₂} (F := pair (G.obj X) (G.obj Y)) (limit.cone (pair (G.obj X) (G.obj Y))))
    (IsLimit.lift (limit.isLimit (pair (G.obj X) (G.obj Y)))
      (BinaryFan.mk (P := G.obj (prod.{v₁, u₁} X Y)) (G.map prod.fst) (G.map prod.snd)))

Tactic:
apply i
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ Eq (α := G.obj (prod.{v₁, u₁} X Y) ⟶ prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) (prodComparison G X Y)

Tactic:
rfl

Premises used: CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.prodComparison, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
rw :
  𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.fst =
    CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.fst
⊢ Eq (α := prod.{v₂, u₂} (G.obj X) (G.obj Y) ⟶ G.obj X)
    (CategoryStruct.comp (Y := G.obj (prod.{v₁, u₁} X Y)) (Iso.inv (iso G X Y)) (G.map prod.fst)) prod.fst

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PreservesLimitPair.iso, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.cancel_iso_hom_left
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.fst =
    CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
rw :
  𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.snd =
    CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.snd
⊢ Eq (α := prod.{v₂, u₂} (G.obj X) (G.obj Y) ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (prod.{v₁, u₁} X Y)) (Iso.inv (iso G X Y)) (G.map prod.snd)) prod.snd

Tactic:
rw [← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y), ← Category.assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PreservesLimitPair.iso, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.cancel_iso_hom_left
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
X Y : C
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (prod.{v₁, u₁} X Y)) ≫ G.map prod.snd =
    CategoryStruct.comp (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (Iso.hom (iso G X Y)) prod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst_2 : HasBinaryProduct.{v₁, u₁} X Y
inst_3 : HasBinaryProduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesLimit (pair X Y) G
⊢ IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y))
    (Iso.hom (PreservesLimitPair.iso G X Y))

Tactic:
infer_instance