-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_hom {J : Type} [Fintype J] (f : J → C) (X : C) :
    (rightDistributor f X).hom =
      ∑ j : J, (biproduct.π f j ▷ X) ≫ biproduct.ι (fun j => f j ⊗ X) j

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.lift fun j => biproduct.π f j ▷ X) ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝

Tactic:
erw [biproduct.lift_π]

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.π f j✝ ▷ X =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j

Tactic:
classical
ext
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
erw [biproduct.lift_π]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.π f j✝ ▷ X =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝

Tactic:
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝

Tactic:
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.lift fun j => biproduct.π f j ▷ X) ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, biproduct.π f j ▷ X ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝