-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.map_eq_map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
    biproduct.map p = biproduct.map' p

Proof state:
case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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

Tactic:
simp

Result:
no goals

Proof state:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ π f j✝¹ ≫ p j✝¹ = p j✝ ≫ ι g j✝ ≫ π g j✝¹

Tactic:
rw [biproduct.ι_π_assoc, biproduct.ι_π]

Result:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 ⋯ else 0) ≫ p j✝¹ = p j✝ ≫ if h : j✝ = j✝¹ then eqToHom ⋯ else 0

Proof state:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 ⋯ ≫ p j✝¹ = p j✝ ≫ eqToHom ⋯

Tactic:
subst h

Result:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝ : J
⊢ eqToHom ⋯ ≫ p j✝ = p j✝ ≫ eqToHom ⋯

Proof state:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝ : J
⊢ eqToHom ⋯ ≫ p j✝ = p j✝ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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

Tactic:
ext

Result:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map p ≫ π g j✝¹ = ι f j✝ ≫ map' p ≫ π g j✝¹

Proof state:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 ⋯ else 0) ≫ p j✝¹ = p j✝ ≫ if h : j✝ = j✝¹ then eqToHom ⋯ else 0

Tactic:
split_ifs with h

Result:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 ⋯ ≫ p j✝¹ = p j✝ ≫ eqToHom ⋯

case neg
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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

Proof state:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 f).toCocone.ι.app { as := j✝ } ≫ (bicone f).toCone.π.app { as := j✝¹ } ≫ p j✝¹ =
    p j✝ ≫ (bicone g).toCocone.ι.app { as := j✝ } ≫ (bicone g).toCone.π.app { as := j✝¹ }

Tactic:
dsimp

Result:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ π f j✝¹ ≫ p j✝¹ = p j✝ ≫ ι g j✝ ≫ π g j✝¹

Proof state:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ map p ≫ π g j✝¹ = ι f j✝ ≫ map' p ≫ π g j✝¹

Tactic:
simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
  Category.assoc, ← Bicone.toCone_π_app_mk, ← biproduct.bicone_π, ← Bicone.toCocone_ι_app_mk,
  ← biproduct.bicone_ι]

Result:
case w.w
J : Type w
C : Type u
inst✝³ : Category.{v, u} 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 f).toCocone.ι.app { as := j✝ } ≫ (bicone f).toCone.π.app { as := j✝¹ } ≫ p j✝¹ =
    p j✝ ≫ (bicone g).toCocone.ι.app { as := j✝ } ≫ (bicone g).toCone.π.app { as := j✝¹ }