[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ (fun j => F.map (Bicone.ι b j)) j ≫ (fun j => F.map (Bicone.π b j)) j' =
    if h : j = j' then eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j') else 0
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = if h : j = j' then eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j') else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : j = j'
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j')
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j) = eqToHom (_ : (F.obj ∘ f) j = (F.obj ∘ f) j)
[PROOFSTEP]
simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]
[GOAL]
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ 𝟙 (F.obj (f j)) = 𝟙 ((F.obj ∘ f) j)
[PROOFSTEP]
dsimp
[GOAL]
case neg
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : ¬j = j'
⊢ F.map (Bicone.ι b j ≫ Bicone.π b j') = 0
[PROOFSTEP]
rw [bicone_ι_π_ne _ h, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inl ≫ F.map b.fst = 𝟙 (F.obj X)
[PROOFSTEP]
rw [← F.map_comp, b.inl_fst, F.map_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inl ≫ F.map b.snd = 0
[PROOFSTEP]
rw [← F.map_comp, b.inl_snd, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inr ≫ F.map b.fst = 0
[PROOFSTEP]
rw [← F.map_comp, b.inr_fst, F.map_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
X Y : C
b : BinaryBicone X Y
⊢ F.map b.inr ≫ F.map b.snd = 𝟙 (F.obj Y)
[PROOFSTEP]
rw [← F.map_comp, b.inr_snd, F.map_id]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBiproducts F
J : Type
x✝ : Fintype J
⊢ PreservesBiproductsOfShape J F
[PROOFSTEP]
letI := preservesBiproductsShrink.{0} F
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : PreservesBiproducts F
J : Type
x✝ : Fintype J
this : PreservesBiproducts F := preservesBiproductsShrink F
⊢ PreservesBiproductsOfShape J F
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      j =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      { as := WalkingPair.left } =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
      ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
          (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).π
      { as := WalkingPair.right } =
    (Iso.refl
          ((Cones.postcompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).hom).obj
              (Bicone.toCone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom ≫
      NatTrans.app (BinaryBicone.toCone (mapBinaryBicone F b)).π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
j : Discrete WalkingPair
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι j
[PROOFSTEP]
rcases j with ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
X Y : C
inst✝ : PreservesBiproduct (pairFunction X Y) F
b : BinaryBicone X Y
hb : BinaryBicone.IsBilimit b
⊢ NatTrans.app
        ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
            (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).ι
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (Discrete.functor (F.obj ∘ pairFunction X Y))).inv).obj
              (Bicone.toCocone (mapBicone F (BinaryBicone.toBicone b)))).pt).hom =
    NatTrans.app (BinaryBicone.toCocone (mapBinaryBicone F b)).ι { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
classical
ext
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
j✝¹ j✝ : J
⊢ biproduct.ι (F.obj ∘ f) j✝ ≫ (biproductComparison' F f ≫ biproductComparison F f) ≫ biproduct.π (F.obj ∘ f) j✝¹ =
    biproduct.ι (F.obj ∘ f) j✝ ≫ 𝟙 (⨁ F.obj ∘ f) ≫ biproduct.π (F.obj ∘ f) j✝¹
[PROOFSTEP]
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : PreservesZeroMorphisms F
⊢ biproductComparison' F f ≫ biproductComparison F f = 𝟙 (⨁ F.obj ∘ f)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
ext
[GOAL]
case h₀.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inl ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.fst =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₀.h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inl ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.snd =
    (biprod.inl ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₁.h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inr ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.fst =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.fst
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
case h₁.h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ (biprod.inr ≫ biprodComparison' F X Y ≫ biprodComparison F X Y) ≫ biprod.snd =
    (biprod.inr ≫ 𝟙 (F.obj X ⊞ F.obj Y)) ≫ biprod.snd
[PROOFSTEP]
simp [← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : PreservesZeroMorphisms F
⊢ biprodComparison' F X Y ≫ biprodComparison F X Y = 𝟙 (F.obj X ⊞ F.obj Y)
[PROOFSTEP]
aesop
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
⊢ F.map (lift g) ≫ (mapBiproduct F f).hom = lift fun j => F.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (F.obj ∘ f) j = (lift fun j => F.map (g j)) ≫ π (F.obj ∘ f) j
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
[PROOFSTEP]
haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ (F.map (lift g) ≫ (mapBiproduct F f).hom) ≫ π (fun x => F.obj (f x)) j =
    (lift fun j => F.map (g j)) ≫ π (fun x => F.obj (f x)) j
[PROOFSTEP]
simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ (mapBiproduct F f).inv ≫ F.map (desc g) = desc fun j => F.map (g j)
[PROOFSTEP]
ext j
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (F.obj ∘ f) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
dsimp only [Function.comp]
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
[GOAL]
case w
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
this : HasBiproduct fun j => F.obj (f j)
⊢ ι (fun x => F.obj (f x)) j ≫ (mapBiproduct F f).inv ≫ F.map (desc g) =
    ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
[PROOFSTEP]
simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((mapBiproduct F f).hom ≫ desc fun j => F.map (g j)) = F.map (desc g)
[PROOFSTEP]
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ F.map (lift f g) ≫ (mapBiprod F X Y).hom = lift (F.map f) (F.map g)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ (F.map (lift f g) ≫ (mapBiprod F X Y).hom) ≫ fst = lift (F.map f) (F.map g) ≫ fst
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ (F.map (lift f g) ≫ (mapBiprod F X Y).hom) ≫ snd = lift (F.map f) (F.map g) ≫ snd
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : W ⟶ X
g : W ⟶ Y
⊢ lift (F.map f) (F.map g) ≫ (mapBiprod F X Y).inv = F.map (lift f g)
[PROOFSTEP]
rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (mapBiprod F X Y).inv ≫ F.map (desc f g) = desc (F.map f) (F.map g)
[PROOFSTEP]
ext
[GOAL]
case h₀
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ inl ≫ (mapBiprod F X Y).inv ≫ F.map (desc f g) = inl ≫ desc (F.map f) (F.map g)
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
case h₁
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ inr ≫ (mapBiprod F X Y).inv ≫ F.map (desc f g) = inr ≫ desc (F.map f) (F.map g)
[PROOFSTEP]
simp [mapBiprod, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : PreservesZeroMorphisms F
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (mapBiprod F X Y).hom ≫ desc (F.map f) (F.map g) = F.map (desc f g)
[PROOFSTEP]
rw [← biprod.mapBiprod_inv_map_desc, Iso.hom_inv_id_assoc]
