-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[ext (iff := false)]
lemma tensorObj₃_ext {j : I} {A : C} (f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A)
    [H : HasGoodTensorTensor₂₃ X₁ X₂ X₃]
    (h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
      ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ 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 : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
⊢ f = g

Tactic:
apply mapBifunctorBifunctor₂₃MapObj_ext (H := H)

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 : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
⊢ ∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ 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 : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
⊢ ∀ (i₁ i₂ i₃ : I) (h : r₁₂₃ (i₁, i₂, i₃) = j),
    ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
      ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ 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 : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
i₁ i₂ i₃ : I
hi : r₁₂₃ (i₁, i₂, i₃) = j
⊢ ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f =
    ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ 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₂ X₃ : GradedObject I C
inst✝¹ : X₂.HasTensor X₃
inst✝ : X₁.HasTensor (tensorObj X₂ X₃)
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A
H : X₁.HasGoodTensorTensor₂₃ X₂ X₃
h :
  ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j),
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f = ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g
i₁ i₂ i₃ : I
hi : r₁₂₃ (i₁, i₂, i₃) = j
⊢ ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ f =
    ιMapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi ≫ g

Tactic:
exact h i₁ i₂ i₃ hi

Result:
no goals