awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
              (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (pair X Y ⋙ F).obj { as := WalkingPair.left })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
              (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (pair X Y ⋙ F).obj { as := WalkingPair.right })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      { as := WalkingPair.right })
    (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.right })
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      j =
    Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
              (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (pair X Y ⋙ F).obj { as := WalkingPair.left })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
              (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (pair X Y ⋙ F).obj { as := WalkingPair.right })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
            (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).π.app
      { as := WalkingPair.right })
    (Iso.hom (id (Iso.refl (F.obj c.pt))) ≫ (F.mapCone c).π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
dsimp : F.obj b.pt ≅ F.obj b.pt
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt ≅
    (BinaryBicone.toCone (F.mapBinaryBicone b)).pt

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ F.obj b.pt ≅ F.obj b.pt

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
        { as := WalkingPair.left : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
        { as := WalkingPair.right : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app
      { as := WalkingPair.right })
    (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.right })
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app j =
    Iso.hom (id (Iso.refl (F.obj b.pt))) ≫ (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
        { as := WalkingPair.left : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.left })
    (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesLimit (pair X Y) F
b : BinaryBicone.{v, u} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v', 0, u'}
        (obj (const (Discrete WalkingPair))
          ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v', 0, u'}
        (pair ((pair X Y ⋙ F).obj { as := WalkingPair.left }) ((pair X Y ⋙ F).obj { as := WalkingPair.right }))
        { as := WalkingPair.right : Discrete WalkingPair })
    (((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app
      { as := WalkingPair.right })
    (Iso.hom (id (Iso.refl (F.obj b.pt))) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
h₁ :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.fst :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
        (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
            (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
              (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
          F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
        (prod.fst : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj X) :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)
h₂ :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.snd :
      F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
        (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
            (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
              (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
          F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
        (prod.snd : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj Y) :
      F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.fst :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
        (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
            (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
              (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
          F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
        (prod.fst : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj X) :
      F.obj (prod.{v, u} X Y) ⟶ F.obj X)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y) prod.snd :
      F.obj (prod.{v, u} X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := prod.{v', u'} (F.obj X) (F.obj Y))
        (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
            (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
              (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
          F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
        (prod.snd : prod.{v', u'} (F.obj X) (F.obj Y) ⟶ F.obj Y) :
      F.obj (prod.{v, u} X Y) ⟶ F.obj Y)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))

Tactic:
have that :
    prodComparison F X Y =
      (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom := by
    ext <;> simp [← Functor.map_comp]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
⊢ IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)

Tactic:
haveI : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
rw :
  IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
⊢ IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)

Tactic:
rw [that]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
⊢ IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)

Tactic:
haveI : IsIso (prodComparison F X Y) := by
    rw [that]
    infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this_1 : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
this : IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)
⊢ PreservesLimit (pair X Y) F

Tactic:
haveI := PreservesLimitPair.of_iso_prod_comparison F X Y
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Mono (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
that :
  Eq (α := F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (prodComparison F X Y : F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
    (CategoryStruct.comp (Y := F.obj (biprod.{v, u} X Y)) (Iso.inv (F.mapIso (biprod.isoProd X Y)))
        (CategoryStruct.comp (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
          (Iso.hom (biprod.isoProd (F.obj X) (F.obj Y)))) :
      F.obj (prod.{v, u} X Y) ⟶ prod.{v', u'} (F.obj X) (F.obj Y))
this_1 : IsIso (X := F.obj (biprod.{v, u} X Y)) (Y := biprod.{v', u'} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)
this_2 : IsIso (X := F.obj (prod.{v, u} X Y)) (Y := prod.{v', u'} (F.obj X) (F.obj Y)) (prodComparison F X Y)
this : PreservesLimit (pair X Y) F
⊢ PreservesBinaryBiproduct X Y F

Tactic:
apply preservesBinaryBiproduct_of_preservesBinaryProduct

Premises used: CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : HasBinaryBiproduct.{v, u} X Y
inst_6 : HasBinaryBiproduct.{v', u'} (F.obj X) (F.obj Y)
inst_7 : Epi (X := biprod.{v', u'} (F.obj X) (F.obj Y)) (Y := F.obj (biprod.{v, u} X Y)) (F.biprodComparison' X Y)
⊢ Epi (X := biprod.{v', u'} (F.obj X) (F.obj Y)) (Y := F.obj (biprod.{v, u} X Y))
    (SplitEpi.section_ (F.splitEpiBiprodComparison X Y))

Tactic:
simpa