-- Mathlib/Algebra/Homology/TotalComplex.lean
@[ext]
lemma hom_ext {A : C} {i₁₂ : I₁₂} {f g : (K.total c₁₂).X i₁₂ ⟶ A}
    (h : ∀ (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂),
      K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g) : f = g

Proof state:
case hfg
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ ∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂),
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g

Tactic:
rintro ⟨i₁, i₂⟩ hi

Result:
case hfg.mk
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ f = g

Tactic:
apply GradedObject.mapObj_ext

Result:
case hfg
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ ∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂),
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g

Proof state:
case hfg.mk
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g

Tactic:
exact h i₁ i₂ hi

Result:
no goals