case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
⊢ ∀ (j : J), ι (fun b => f b) j ≫ map p = ι (fun b => f b) j ≫ map' p
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
⊢ map p = map' p
apply biproduct.hom_ext'
case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ ι (fun b => f b) j ≫ map p = ι (fun b => f b) j ≫ map' p
case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
⊢ ∀ (j : J), ι (fun b => f b) j ≫ map p = ι (fun b => f b) j ≫ map' p
intro j
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ ∀ (j_1 : J),
    (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j_1 = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j_1
case w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ ι (fun b => f b) j ≫ map p = ι (fun b => f b) j ≫ map' p
apply biproduct.hom_ext
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j' = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j'
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ ∀ (j_1 : J),
    (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j_1 = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j_1
intro j'
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j' = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j'
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j' = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j'
dsimp
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (Bicone.toCocone (bicone fun b => f b)).ι.app { as := j } ≫
      (Bicone.toCone (bicone fun b => f b)).π.app { as := j' } ≫ p j' =
    p j ≫
      (Bicone.toCocone (bicone fun b => g b)).ι.app { as := j } ≫
        (Bicone.toCone (bicone fun b => g b)).π.app { as := j' }
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (ι (fun b => f b) j ≫ map p) ≫ π (fun b => g b) j' = (ι (fun b => f b) j ≫ map' p) ≫ π (fun b => g b) j'
simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map, Limits.IsLimit.map_π, Category.assoc,
  ← Bicone.toCone_π_app_mk, ← biproduct.bicone_π, ← Bicone.toCocone_ι_app_mk, ←
  biproduct.bicone_ι]
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ ι (fun b => f b) j ≫ π (fun b => f b) j' ≫ p j' = p j ≫ ι (fun b => g b) j ≫ π (fun b => g b) j'
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (Bicone.toCocone (bicone fun b => f b)).ι.app { as := j } ≫
      (Bicone.toCone (bicone fun b => f b)).π.app { as := j' } ≫ p j' =
    p j ≫
      (Bicone.toCocone (bicone fun b => g b)).ι.app { as := j } ≫
        (Bicone.toCone (bicone fun b => g b)).π.app { as := j' }
dsimp
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (if h : j = j' then eqToHom (_ : f j = f j') else 0) ≫ p j' = p j ≫ if h : j = j' then eqToHom (_ : g j = g j') else 0
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ ι (fun b => f b) j ≫ π (fun b => f b) j' ≫ p j' = p j ≫ ι (fun b => g b) j ≫ π (fun b => g b) j'
rw [biproduct.ι_π_assoc, biproduct.ι_π]
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
h : j = j'
⊢ eqToHom (_ : f j = f j') ≫ p j' = p j ≫ eqToHom (_ : g j = g j')

case w.w.inr
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
h : ¬j = j'
⊢ 0 ≫ p j' = p j ≫ 0
case w.w
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
⊢ (if h : j = j' then eqToHom (_ : f j = f j') else 0) ≫ p j' = p j ≫ if h : j = j' then eqToHom (_ : g j = g j') else 0
split_ifs with h
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ eqToHom (_ : f j = f j) ≫ p j = p j ≫ eqToHom (_ : g j = g j)
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
h : j = j'
⊢ eqToHom (_ : f j = f j') ≫ p j' = p j ≫ eqToHom (_ : g j = g j')
subst h
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ p j = p j ≫ eqToHom (_ : g j = g j)
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ eqToHom (_ : f j = f j) ≫ p j = p j ≫ eqToHom (_ : g j = g j)
rw [eqToHom_refl, Category.id_comp]
no goals
case w.w.inl
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j : J
⊢ p j = p j ≫ eqToHom (_ : g j = g j)
erw [Category.comp_id]
no goals
case w.w.inr
J : Type w
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j j' : J
h : ¬j = j'
⊢ 0 ≫ p j' = p j ≫ 0
simp