awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
w :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (biproduct.ι (F.obj ∘ f) j_1)
        (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
          (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f)
            (F.biproductComparison f))
          (biproduct.π (F.obj ∘ f) j)) =
      biproduct.ι (F.obj ∘ f) j_1 ≫ 𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) ≫ biproduct.π (F.obj ∘ f) j
⊢ CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f) (F.biproductComparison f) =
    𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f))

Tactic:
classical
    ext
    simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.biproductComparison' f) (F.biproductComparison f) =
    𝟙 (biproduct.{w₁, v₂, u₂} (F.obj ∘ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
⊢ IsSplitEpi (X := F.obj (biproduct.{w₁, v₁, u₁} f)) (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (F.biproductComparison f)

Tactic:
IsSplitEpi.mk' (splitEpiBiproductComparison F f)

Premises used: CategoryTheory.Functor.splitEpiBiproductComparison, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)
inst_6 : F.PreservesZeroMorphisms
⊢ IsSplitMono (X := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (Y := F.obj (biproduct.{w₁, v₁, u₁} f))
    (F.biproductComparison' f)

Tactic:
IsSplitMono.mk' (splitMonoBiproductComparison' F f)

Premises used: CategoryTheory.Functor.splitMonoBiproductComparison', CategoryTheory.IsSplitMono.mk'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBiproduct f F
⊢ HasBiproduct.{w₁, v₂, u₂} (F.obj ∘ f)

Tactic:
HasBiproduct.mk
    { bicone := F.mapBicone (biproduct.bicone f)
      isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.biproduct.isBilimit, CategoryTheory.Functor.mapBicone, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.LimitBicone.mk, CategoryTheory.Limits.isBilimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBiproduct f F
⊢ HasBiproduct.{w₁, v₂, u₂} (C := D) fun (i : J) ↦ F.obj (f i)

Tactic:
HasBiproduct.mk
    { bicone := F.mapBicone (biproduct.bicone f)
      isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.biproduct.isBilimit, CategoryTheory.Functor.mapBicone, CategoryTheory.Limits.HasBiproduct.mk, CategoryTheory.Limits.LimitBicone.mk, CategoryTheory.Limits.isBilimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBiproduct f F
⊢ Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (Iso.hom (F.mapBiproduct f) : F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (biproduct.lift fun (j : J) ↦ F.map (biproduct.π f j) :
      F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
J : Type w₁
F : Functor.{v₁, v₂, u₁, u₂} C D
f : J → C
inst_4 : HasBiproduct.{w₁, v₁, u₁} f
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBiproduct f F
⊢ Eq (α := biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj (biproduct.{w₁, v₁, u₁} f))
    (Iso.inv (F.mapBiproduct f) : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj (biproduct.{w₁, v₁, u₁} f))
    (biproduct.desc fun (j : J) ↦ F.map (biproduct.ι f j) :
      (biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j)) ⟶ F.obj (biproduct.{w₁, v₁, u₁} f))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (F.biprodComparison X Y) biprod.fst)
    (F.map biprod.fst)

Tactic:
biprod.lift_fst _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.biprod.lift_fst, CategoryTheory.Functor.biprodComparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (F.biprodComparison X Y) biprod.snd)
    (F.map biprod.snd)

Tactic:
biprod.lift_snd _ _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.biprod.lift_snd, CategoryTheory.Functor.biprodComparison
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj X ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl (F.biprodComparison' X Y))
    (F.map biprod.inl)

Tactic:
biprod.inl_desc _ _

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.biprod.inl_desc, CategoryTheory.Functor.biprodComparison'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
⊢ Eq (α := F.obj Y ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr (F.biprodComparison' X Y))
    (F.map biprod.inr)

Tactic:
biprod.inr_desc _ _

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.biprod.inr_desc, CategoryTheory.Functor.biprodComparison'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
h₀ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst
h₃ :
  CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inl
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inl ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.fst =
    (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.fst

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y))
      (CategoryStruct.comp (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) biprod.inr
        (CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y)))
      biprod.snd =
    (biprod.inr ≫ 𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))) ≫ biprod.snd

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ CategoryStruct.comp (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y) (F.biprodComparison X Y) =
    𝟙 (biprod.{v₂, u₂} (F.obj X) (F.obj Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ IsSplitEpi (X := F.obj (biprod.{v₁, u₁} X Y)) (Y := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (F.biprodComparison X Y)

Tactic:
IsSplitEpi.mk' (splitEpiBiprodComparison F X Y)

Premises used: CategoryTheory.Functor.splitEpiBiprodComparison, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)
inst_6 : F.PreservesZeroMorphisms
⊢ IsSplitMono (X := biprod.{v₂, u₂} (F.obj X) (F.obj Y)) (Y := F.obj (biprod.{v₁, u₁} X Y)) (F.biprodComparison' X Y)

Tactic:
IsSplitMono.mk' (splitMonoBiprodComparison' F X Y)

Premises used: CategoryTheory.IsSplitMono.mk', CategoryTheory.Functor.splitMonoBiprodComparison'
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproduct X Y F
⊢ HasBinaryBiproduct.{v₂, u₂} (F.obj X) (F.obj Y)

Tactic:
HasBinaryBiproduct.mk
    { bicone := F.mapBinaryBicone (BinaryBiproduct.bicone X Y)
      isBilimit := isBinaryBilimitOfPreserves F (BinaryBiproduct.isBilimit _ _) }

Premises used: CategoryTheory.Functor.mapBinaryBicone, CategoryTheory.Limits.BinaryBiproduct.bicone, CategoryTheory.Limits.HasBinaryBiproduct.mk, CategoryTheory.Limits.BinaryBiproductData.mk, CategoryTheory.Limits.BinaryBiproduct.isBilimit, CategoryTheory.Limits.isBinaryBilimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproduct X Y F
⊢ Eq (α := F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (Iso.hom (F.mapBiprod X Y) : F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))
    (biprod.lift (F.map biprod.fst) (F.map biprod.snd) :
      F.obj (biprod.{v₁, u₁} X Y) ⟶ biprod.{v₂, u₂} (F.obj X) (F.obj Y))

Tactic:
rfl

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_4 : HasBinaryBiproduct.{v₁, u₁} X Y
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesBinaryBiproduct X Y F
⊢ Eq (α := biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (Iso.inv (F.mapBiprod X Y) : biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))
    (biprod.desc (F.map biprod.inl) (F.map biprod.inr) :
      biprod.{v₂, u₂} (F.obj X) (F.obj Y) ⟶ F.obj (biprod.{v₁, u₁} X Y))

Tactic:
rfl

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
          F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (π (F.obj ∘ f) j : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ (F.obj ∘ f) j) =
      CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (lift fun (j : J) ↦ F.map (g j)) (π (F.obj ∘ f) j)
⊢ Eq (α := F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
      F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
    (lift fun (j : J) ↦ F.map (g j) : F.obj W ⟶ biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
w :
  CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
        F.obj W ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (π (fun (x : J) ↦ F.obj (f x)) j : (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj (f j)) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) (lift fun (j : J) ↦ F.map (g j))
      (π (fun (x : J) ↦ F.obj (f x)) j)
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
        F.obj W ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
      (π (F.obj ∘ f) j : biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ (F.obj ∘ f) j) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (lift fun (j : J) ↦ F.map (g j)) (π (F.obj ∘ f) j)

Tactic:
dsimp only [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (F.map (lift g)) (Iso.hom (F.mapBiproduct f)) :
        F.obj W ⟶ biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x))
      (π (fun (x : J) ↦ F.obj (f x)) j : (biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) ⟶ F.obj (f j)) =
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} fun (x : J) ↦ F.obj (f x)) (lift fun (j : J) ↦ F.map (g j))
      (π (fun (x : J) ↦ F.obj (f x)) j)

Tactic:
simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapBiproduct_hom, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biproduct.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst_5 : HasBiproduct.{w₁, v₁, u₁} f
inst_6 : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (ι (F.obj ∘ f) j : (F.obj ∘ f) j ⟶ biproduct.{w₁, v₂, u₂} (F.obj ∘ f))
        (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
          biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W) =
      CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (ι (F.obj ∘ f) j) (desc fun (j : J) ↦ F.map (g j))
⊢ Eq (α := biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W)
    (CategoryStruct.comp (Y := F.obj (biproduct.{w₁, v₁, u₁} f)) (Iso.inv (F.mapBiproduct f)) (F.map (desc g)) :
      biproduct.{w₁, v₂, u₂} (F.obj ∘ f) ⟶ F.obj W)
    (desc fun (j : J) ↦ F.map (g j) : (biproduct.{w₁, v₂, u₂} fun (j : J) ↦ F.obj (f j)) ⟶ F.obj W)

Tactic:
ext j