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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
h :
  ∀ (j : J),
    Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
      (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
          (Pi.π (fun (b : J) ↦ F.obj (f b)) j) :
        F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
      (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
          (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
              (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
                (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
            F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
          (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
        F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))

Tactic:
ext j
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
j : J
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
      (Pi.π (fun (b : J) ↦ F.obj (f b)) j))
    (F.map (Pi.π f j))

Tactic:
piComparison_comp_π F f j

Premises used: CategoryTheory.Limits.piComparison_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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
j : J
h :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
        (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
            (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
              (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
          F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (F.map (Pi.π f j) : F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
        (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
            (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
              (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
          F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))

Tactic:
convert! piComparison_comp_π F f j

Premises used: CategoryTheory.Limits.piComparison_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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
j : J
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (CategoryStruct.comp (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
        (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
            (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
              (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
          F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
        (Pi.π (fun (b : J) ↦ F.obj (f b)) j : (piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) ⟶ F.obj (f j)) :
      F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))
    (F.map (Pi.π f j) : F.obj (piObj.{u_1, v, u} f) ⟶ F.obj (f j))

Tactic:
simp [← Function.comp_def, ← Functor.map_comp]

Premises used: Function.comp_def, 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
⊢ Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))

Tactic:
have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert! piComparison_comp_π F f j; simp [← Function.comp_def, ← 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
⊢ IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)

Tactic:
haveI : IsIso (biproductComparison F f) := 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
rw :
  IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)

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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))

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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)

Tactic:
haveI : IsIso (piComparison F f) := 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this_2 :
  IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this : IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
⊢ PreservesLimit (Discrete.functor f) F

Tactic:
haveI := PreservesProduct.of_iso_comparison F f
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_1 : HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)
that :
  Eq (α := F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (piComparison F f : F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b))
    (CategoryStruct.comp (Y := F.obj (biproduct.{u_1, v, u} f)) (Iso.inv (F.mapIso (biproduct.isoProduct f)))
        (CategoryStruct.comp (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
          (Iso.hom (biproduct.isoProduct (F.obj ∘ f)))) :
      F.obj (piObj.{u_1, v, u} f) ⟶ piObj.{u_1, v', u'} (F.obj ∘ f))
this_2 :
  IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
this_3 :
  IsIso (X := F.obj (piObj.{u_1, v, u} f)) (Y := piObj.{u_1, v', u'} fun (b : J) ↦ F.obj (f b)) (piComparison F f)
this : PreservesLimit (Discrete.functor f) F
⊢ PreservesBiproduct f F

Tactic:
apply preservesBiproduct_of_preservesProduct

Premises used: CategoryTheory.Limits.preservesBiproduct_of_preservesProduct
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
⊢ Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
    (SplitEpi.section_ (F.splitEpiBiproductComparison f))

Tactic:
simpa
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
⊢ Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
    (SplitEpi.section_ (F.splitEpiBiproductComparison f))

Tactic:
haveI : Epi (splitEpiBiproductComparison F f).section_ := by simpa
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
this :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
    (SplitEpi.section_ (F.splitEpiBiproductComparison f))
⊢ IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)

Tactic:
haveI : IsIso (biproductComparison F f) :=
    IsIso.of_epi_section' (splitEpiBiproductComparison F f)
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f)) (F.biproductComparison' f)
this_1 :
  Epi (X := biproduct.{u_1, v', u'} (F.obj ∘ f)) (Y := F.obj (biproduct.{u_1, v, u} f))
    (SplitEpi.section_ (F.splitEpiBiproductComparison f))
this : IsIso (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
apply preservesBiproduct_of_mono_biproductComparison

Premises used: CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison
-- 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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : PreservesBiproduct f F
c : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
hc : IsColimit c
val : Fintype J
as : J
⊢ Eq (α := (Discrete.functor f ⋙ F).obj { as := as : Discrete J } ⟶ (F.mapCocone c).pt)
    (((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (Bicone.toCocone (F.mapBicone (Bicone.ofColimitCocone hc)))).ι.app
        { as := as : Discrete J } ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).hom).obj
              (Bicone.toCocone (F.mapBicone (Bicone.ofColimitCocone hc)))).pt))
    ((F.mapCocone c).ι.app { as := as })

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
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : PreservesColimit (Discrete.functor f) F
b : Bicone.{u_1, v, u} f
hb : b.IsBilimit
val : Fintype J
as : J
⊢ Eq (α :=
    obj.{u_1, v', u_1, u'} (Discrete.functor (F.obj ∘ f)) { as := as : Discrete J } ⟶
      (Bicone.toCocone (F.mapBicone b)).pt)
    (((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := as : Discrete J } ≫
      Iso.hom (Iso.refl ((Cocone.precompose (Discrete.compNatIsoDiscrete f F).inv).obj (F.mapCocone b.toCocone)).pt))
    ((Bicone.toCocone (F.mapBicone b)).ι.app { as := as })

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
dsimp : F.obj c.pt ≅ F.obj c.pt
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj
        (BinaryBicone.toCone (F.mapBinaryBicone (BinaryBicone.ofLimitCone hc)))).pt ≅
    (F.mapCone c).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 : PreservesBinaryBiproduct X Y F
c : Cone.{0, v, 0, u} (pair X Y)
hc : IsLimit c
⊢ F.obj c.pt ≅ F.obj c.pt

Tactic:
rfl