-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_ext_left {J : Type} [Fintype J]
    {f : J → C} {X Y : C} {g h : (⨁ f) ⊗ X ⟶ Y}
    (w : ∀ j, (biproduct.ι f j ▷ X) ≫ g = (biproduct.ι f j ▷ X) ≫ h) : g = h

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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ (rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h

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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ g = h

Tactic:
classical
apply (cancel_epi (rightDistributor f X).inv).mp
ext
simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
  simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, ↓reduceIte, eqToHom_refl, Category.id_comp]
apply w

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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ g = h

Tactic:
apply (cancel_epi (rightDistributor f X).inv).mp

Result:
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
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
⊢ (rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h

Tactic:
simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp,
  zero_comp, Finset.sum_dite_eq, Finset.mem_univ, ↓reduceIte, eqToHom_refl, Category.id_comp]

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ X ≫ g = biproduct.ι f j✝ ▷ X ≫ h

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ X ≫ g = biproduct.ι f j✝ ▷ X ≫ h

Tactic:
apply w

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h

Tactic:
simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
  simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, ↓reduceIte, eqToHom_refl, Category.id_comp]

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 Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), biproduct.ι f j ▷ X ≫ g = biproduct.ι f j ▷ X ≫ h
j✝ : J
⊢ biproduct.ι f j✝ ▷ X ≫ g = biproduct.ι f j✝ ▷ X ≫ h