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

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

Tactic:
simp only [id_tensor_comp, tensor_dite, 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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        if h : x = j✝ then (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ eqToHom ⋯)
        else (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ 0)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0

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

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

Tactic:
classical
ext
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom,
  asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum,
  id_tensor_comp, tensorIso_hom, leftDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map,
  biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero]
simp_rw [← id_tensorHom]
simp only [← id_tensor_comp, biproduct.ι_π]
simp only [id_tensor_comp, tensor_dite, comp_dite]
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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        if h : x = j✝ then (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ eqToHom ⋯)
        else (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ 0)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0

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

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

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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j => Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0

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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫
          (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ (𝟙 X ⊗ biproduct.π (fun j => Y ⊗ f j) j✝)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0

Tactic:
simp only [← id_tensor_comp, biproduct.ι_π]

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

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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j => Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0

Tactic:
simp_rw [← id_tensorHom]

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
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫
          (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ (𝟙 X ⊗ biproduct.π (fun j => Y ⊗ f j) j✝)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0