-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[ext]
lemma tensorObj_ext {A : C} {j : I} (f g : tensorObj X₁ X₂ j ⟶ A)
    (h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
      ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g) : f = g

Proof state:
case hfg.mk
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
i₁ i₂ : I
hi :
  (match (i₁, i₂) with
    | (i, j) => i + j) =
    j
⊢ (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
        (fun x =>
          match x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      f =
    (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
        (fun x =>
          match x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      g

Tactic:
exact h i₁ i₂ hi

Result:
no goals

Proof state:
case hfg
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
⊢ ∀ (i : I × I)
    (hij :
      (match i with
        | (i, j) => i + j) =
        j),
    (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
          (fun x =>
            match x with
            | (i, j) => i + j)
          i j hij ≫
        f =
      (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
          (fun x =>
            match x with
            | (i, j) => i + j)
          i j hij ≫
        g

Tactic:
rintro ⟨i₁, i₂⟩ hi

Result:
case hfg.mk
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
i₁ i₂ : I
hi :
  (match (i₁, i₂) with
    | (i, j) => i + j) =
    j
⊢ (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
        (fun x =>
          match x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      f =
    (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
        (fun x =>
          match x with
          | (i, j) => i + j)
        (i₁, i₂) j hi ≫
      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₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
⊢ f = g

Tactic:
apply mapObj_ext

Result:
case hfg
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
X₁ X₂ : GradedObject I C
inst✝ : X₁.HasTensor X₂
A : C
j : I
f g : tensorObj X₁ X₂ j ⟶ A
h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ f = ιTensorObj X₁ X₂ i₁ i₂ j hi ≫ g
⊢ ∀ (i : I × I)
    (hij :
      (match i with
        | (i, j) => i + j) =
        j),
    (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
          (fun x =>
            match x with
            | (i, j) => i + j)
          i j hij ≫
        f =
      (((mapBifunctor (curriedTensor C) I I).obj X₁).obj X₂).ιMapObj
          (fun x =>
            match x with
            | (i, j) => i + j)
          i j hij ≫
        g