-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[ext (iff := false)]
lemma left_tensor_tensorObj₃_ext {j : I} {A : C} (Z : C)
    (f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A)
    [H : HasGoodTensorTensor₂₃ X₁ X₂ X₃]
    [hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j]
    (h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
      (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ f =
        (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ g) : f = g

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : (i₁, i₂, i₃) ∈ r₁₂₃ ⁻¹' {j}
⊢ (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      f =
    (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      g

Tactic:
exact h _ _ _ hi

Result:
no goals

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ f = g

Tactic:
refine (@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _
  (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext ?_

Result:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ ∀ (j_1 : Discrete ↑(r₁₂₃ ⁻¹' {j})),
    (((curriedTensor C).obj Z).mapCocone
                (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
          j_1 ≫
        f =
      (((curriedTensor C).obj Z).mapCocone
                (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
          j_1 ≫
        g

Proof state:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
⊢ ∀ (j_1 : Discrete ↑(r₁₂₃ ⁻¹' {j})),
    (((curriedTensor C).obj Z).mapCocone
                (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
          j_1 ≫
        f =
      (((curriedTensor C).obj Z).mapCocone
                (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
          j_1 ≫
        g

Tactic:
intro ⟨⟨i₁, i₂, i₃⟩, hi⟩

Result:
I : Type u
inst✝⁴ : AddMonoid I
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : MonoidalCategory C
X₁ X₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A Z : C
f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j
h :
  ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j),
    Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g
i₁ i₂ i₃ : I
hi : (i₁, i₂, i₃) ∈ r₁₂₃ ⁻¹' {j}
⊢ (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      f =
    (((curriedTensor C).obj Z).mapCocone
              (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app
        { as := ⟨(i₁, i₂, i₃), hi⟩ } ≫
      g