-- Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
@[ext]
lemma mapBifunctorMapObj_ext {X : GradedObject I C₁} {Y : GradedObject J C₂} {A : C₃} {k : K}
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p]
    {f g : mapBifunctorMapObj F p X Y k ⟶ A}
    (h : ∀ (i : I) (j : J) (hij : p ⟨i, j⟩ = k),
      ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g) :
    f = g

Proof state:
case hfg
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ ∀ (i : I × J) (hij : p i = k),
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ f =
      (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ g

Tactic:
rintro ⟨i, j⟩ hij

Result:
case hfg.mk
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
i : I
j : J
hij : p (i, j) = k
⊢ (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ f =
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ g

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ f = g

Tactic:
apply mapObj_ext

Result:
case hfg
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ ∀ (i : I × J) (hij : p i = k),
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ f =
      (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ g

Proof state:
case hfg.mk
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{u_9, u_1} C₁
inst✝² : Category.{u_8, u_2} C₂
inst✝¹ : Category.{u_7, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
i : I
j : J
hij : p (i, j) = k
⊢ (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ f =
    (((mapBifunctor F I J).obj X).obj Y).ιMapObj p (i, j) k hij ≫ g

Tactic:
exact h i j hij

Result:
no goals