awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasBinaryProducts.{v₂, u₂} D
i : ∀ {X Y : C}, IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
⊢ PreservesLimit
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    G

Tactic:
have : PreservesLimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesLimitPair.of_iso_prod_comparison ..
-- 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
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasBinaryProducts.{v₂, u₂} D
i : ∀ {X Y : C}, IsIso (X := G.obj (prod.{v₁, u₁} X Y)) (Y := prod.{v₂, u₂} (G.obj X) (G.obj Y)) (prodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
this :
  PreservesLimit
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    G
⊢ PreservesLimit K G

Tactic:
apply preservesLimit_of_iso_diagram G (diagramIsoPair K).symm

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- 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 : X ⟶ P
g : Y ⟶ P
⊢ Eq (α :=
    Functor.obj.{0, v₂, 0, u₂}
        (pair ((pair X Y ⋙ G).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ G).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryCofan.mk (G.map f) (G.map g)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).pt))
    ((BinaryCofan.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 : X ⟶ P
g : Y ⟶ P
⊢ Eq (α :=
    Functor.obj.{0, v₂, 0, u₂}
        (pair ((pair X Y ⋙ G).obj { as := WalkingPair.left : Discrete WalkingPair })
          ((pair X Y ⋙ G).obj { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryCofan.mk (G.map f) (G.map g)).pt)
    (((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).pt))
    ((BinaryCofan.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
X Y : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} X Y
inst_3 : HasBinaryCoproduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesColimit (pair X Y) G
⊢ Eq (α := coprod.{v₂, u₂} (G.obj X) (G.obj Y) ⟶ G.obj (coprod.{v₁, u₁} X Y)) (Iso.hom (iso G X Y))
    (coprodComparison G X Y)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.coprodComparison, 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
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst_2 : HasBinaryCoproduct.{v₁, u₁} X Y
inst_3 : HasBinaryCoproduct.{v₂, u₂} (G.obj X) (G.obj Y)
inst_4 : PreservesColimit (pair X Y) G
⊢ IsIso (X := coprod.{v₂, u₂} (G.obj X) (G.obj Y)) (Y := G.obj (coprod.{v₁, u₁} X Y))
    (Iso.hom (PreservesColimitPair.iso G X Y))

Tactic:
infer_instance
-- 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
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₂, u₂} D
i :
  ∀ {X Y : C},
    IsIso (X := coprod.{v₂, u₂} (G.obj X) (G.obj Y)) (Y := G.obj (coprod.{v₁, u₁} X Y)) (coprodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
⊢ PreservesColimit
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    G

Tactic:
have : PreservesColimit (pair (K.obj ⟨WalkingPair.left⟩) (K.obj ⟨WalkingPair.right⟩)) G :=
      PreservesColimitPair.of_iso_coprod_comparison ..
-- 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
inst_2 : HasBinaryCoproducts.{v₁, u₁} C
inst_3 : HasBinaryCoproducts.{v₂, u₂} D
i :
  ∀ {X Y : C},
    IsIso (X := coprod.{v₂, u₂} (G.obj X) (G.obj Y)) (Y := G.obj (coprod.{v₁, u₁} X Y)) (coprodComparison G X Y)
K : Functor.{0, v₁, 0, u₁} (Discrete WalkingPair) C
this :
  PreservesColimit
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    G
⊢ PreservesColimit K G

Tactic:
apply preservesColimit_of_iso_diagram G (diagramIsoPair K).symm

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- 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
b : Bicone.{w₁, v₁, u₁} f
j j' : J
rw : F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
⊢ F.map (b.ι j) ≫ F.map (b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
rw [← F.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
inst_4 : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone.{w₁, v₁, u₁} f
j j' : J
pos : ∀ (h : j = j'), F.map (b.ι j ≫ b.π j') = eqToHom ⋯
neg : ∀ (h : ¬j = j'), F.map (b.ι j ≫ b.π j') = 0
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
split_ifs with h
-- 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
b : Bicone.{w₁, v₁, u₁} f
j j' : J
h : j = j'
pos : F.map (b.ι j ≫ b.π j) = eqToHom ⋯
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯

Tactic:
subst h
-- 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
b : Bicone.{w₁, v₁, u₁} f
j : J
pos : Eq.{v₂ + 1} (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j) (𝟙 (F.obj (f j))) (𝟙 ((F.obj ∘ f) j))
⊢ F.map (b.ι j ≫ b.π j) = eqToHom ⋯

Tactic:
simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Limits.bicone_ι_π_self, CategoryTheory.Functor.map_id
-- 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
b : Bicone.{w₁, v₁, u₁} f
j : J
⊢ Eq.{v₂ + 1} (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j) (𝟙 (F.obj (f j))) (𝟙 ((F.obj ∘ f) j))

Tactic:
dsimp
-- 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
b : Bicone.{w₁, v₁, u₁} f
j j' : J
h : ¬j = j'
neg : Eq (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j') (F.map 0) 0
neg₁ neg₂ : Eq.{v₂ + 1} (α := (F.obj ∘ f) j ⟶ (F.obj ∘ f) j') 0 0
⊢ F.map (b.ι j ≫ b.π j') = 0

Tactic:
rw [bicone_ι_π_ne _ h, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.bicone_ι_π_ne
-- 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₁
K : Type w₂
g : K ≃ J
f : J → C
c : Bicone.{w₁, v₁, u₁} f
⊢ Eq (α := Bicone.{w₂, v₂, u₂} (J := K) (F.obj ∘ f ∘ (⇑g : (a : K) → J))) (F.mapBicone (c.whisker g))
    (Bicone.whisker (F.mapBicone c) g)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Bicone.whisker, 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
inst_5 : PreservesBiproducts F
⊢ PreservesBiproducts F

Tactic:
⟨fun {_} =>
    ⟨fun {_} =>
      ⟨fun {b} ib =>
        ⟨((F.mapBicone b).whiskerIsBilimitIff _).toFun
          (isBilimitOfPreserves F ((b.whiskerIsBilimitIff Equiv.ulift.{w₂}).invFun ib))⟩⟩⟩⟩

Premises used: CategoryTheory.Limits.PreservesBiproduct.mk, CategoryTheory.Functor.mapBicone, Equiv.ulift, Equiv.toFun, Nonempty.intro, CategoryTheory.Limits.PreservesBiproductsOfShape.mk, CategoryTheory.Limits.PreservesBiproducts.mk, CategoryTheory.Limits.isBilimitOfPreserves, CategoryTheory.Limits.Bicone.whiskerIsBilimitIff, Equiv.invFun
-- 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
inst_5 : PreservesBiproducts F
J : Type
h : Finite J
this : PreservesBiproducts F := ⋯
⊢ PreservesBiproductsOfShape J F

Tactic:
infer_instance
-- 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
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v₂, 0, u₂}
        (obj (const (Discrete WalkingPair))
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair })
    ((obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).π.app
      { as := WalkingPair.left })
    (Iso.hom
        (Iso.refl
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.left })

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
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v₂, 0, u₂}
        (obj (const (Discrete WalkingPair))
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair })
    ((obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
            (Bicone.toCone (F.mapBicone b.toBicone))).π.app
      { as := WalkingPair.right })
    (Iso.hom
        (Iso.refl
          (obj (Cone.postcompose (Iso.hom (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCone (F.mapBicone b.toBicone))).pt) ≫
      (BinaryBicone.toCone (F.mapBinaryBicone b)).π.app { as := WalkingPair.right })

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
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })
right :
  Eq (α :=
    obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.right })
⊢ (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        j ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt) =
    (BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- 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
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.left })

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
inst_4 : F.PreservesZeroMorphisms
X Y : C
inst_5 : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone.{v₁, u₁} X Y
hb : b.IsBilimit
⊢ Eq (α :=
    obj.{0, v₂, 0, u₂}
        (pair
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.left : Discrete WalkingPair })
          (obj.{0, v₂, 0, u₂} (Discrete.functor (F.obj ∘ pairFunction X Y))
            { as := WalkingPair.right : Discrete WalkingPair }))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryBicone.toCocone (F.mapBinaryBicone b)).pt)
    ((obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).ι.app
        { as := WalkingPair.right : Discrete WalkingPair } ≫
      Iso.hom
        (Iso.refl
          (obj (Cocone.precompose (Iso.inv (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y)))))
              (Bicone.toCocone (F.mapBicone b.toBicone))).pt))
    ((BinaryBicone.toCocone (F.mapBinaryBicone b)).ι.app { as := WalkingPair.right })

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)
j : J
⊢ Eq (α := F.obj (biproduct.{w₁, v₁, u₁} f) ⟶ (F.obj ∘ f) j)
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (F.biproductComparison f)
      (biproduct.π (F.obj ∘ f) j))
    (F.map (biproduct.π f j))

Tactic:
biproduct.lift_π _ _

Premises used: CategoryTheory.Functor.biproductComparison, 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
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)
j : J
⊢ Eq (α := (F.obj ∘ f) j ⟶ F.obj (biproduct.{w₁, v₁, u₁} f))
    (CategoryStruct.comp (Y := biproduct.{w₁, v₂, u₂} (F.obj ∘ f)) (biproduct.ι (F.obj ∘ f) j)
      (F.biproductComparison' f))
    (F.map (biproduct.ι f j))

Tactic:
biproduct.ι_desc _ _

Premises used: CategoryTheory.Functor.biproductComparison', CategoryTheory.Limits.biproduct.ι_desc
-- 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:
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
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
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

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

Premises used: CategoryTheory.eqToHom_map, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Functor.map_comp