-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_assoc {J : Type} [Fintype J] (f : J → C) (X Y : C) :
    (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
      α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun _ => (α_ _ X Y).symm

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 Y : C
⊢ (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x => (α_ (f x) X Y).symm

Tactic:
classical
ext
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
  asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
  comp_tensor_id, tensorIso_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
  biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero,
  Finset.mem_univ, if_true]
simp_rw [← tensorHom_id]
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
simp

Result:
no goals

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 Y : C
⊢ (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x => (α_ (f x) X Y).symm

Tactic:
ext

Result:
case w.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 Y : C
j✝ : J
⊢ ((rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝ =
    (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x => (α_ (f x) X Y).symm).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝

Proof state:
case w.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 Y : C
j✝ : J
⊢ (∑ x : J, if h : x = j✝ then (biproduct.π f x ⊗ 𝟙 X) ≫ eqToHom ⋯ ⊗ 𝟙 Y else (biproduct.π f x ⊗ 𝟙 X) ≫ 0 ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv

Tactic:
simp

Result:
no goals

Proof state:
case w.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 Y : C
j✝ : J
⊢ ∑ x : J,
      (biproduct.π f x ▷ X ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ biproduct.π (fun j => f j ⊗ X) j✝ ▷ Y =
    (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv

Tactic:
simp_rw [← tensorHom_id]

Result:
case w.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 Y : C
j✝ : J
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => f j ⊗ X) j✝ ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv

Proof state:
case w.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 Y : C
j✝ : J
⊢ ((rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝ =
    (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun x => (α_ (f x) X Y).symm).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝

Tactic:
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
  asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
  comp_tensor_id, tensorIso_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
  biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero,
  Finset.mem_univ, if_true]

Result:
case w.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 Y : C
j✝ : J
⊢ ∑ x : J,
      (biproduct.π f x ▷ X ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ biproduct.π (fun j => f j ⊗ X) j✝ ▷ Y =
    (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv

Proof state:
case w.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 Y : C
j✝ : J
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => f j ⊗ X) j✝ ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv

Tactic:
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]

Result:
case w.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 Y : C
j✝ : J
⊢ (∑ x : J, if h : x = j✝ then (biproduct.π f x ⊗ 𝟙 X) ≫ eqToHom ⋯ ⊗ 𝟙 Y else (biproduct.π f x ⊗ 𝟙 X) ≫ 0 ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv