-- Mathlib/Algebra/Homology/BifunctorHomotopy.lean
@[reassoc]
lemma ιMapBifunctor_hom₁ (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J)
    (h : ComplexShape.π c₁ c₂ c (i₁', i₂) = j) (h' : c₁.prev i₁' = i₁) :
    ιMapBifunctor K₁ K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' = ComplexShape.ε₁ c₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
        ιMapBifunctorOrZero L₁ L₂ F c _ _ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_9, u_1} C₁
inst✝¹⁰ : Category.{u_8, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
h' : c₁.prev i₁' = i₁
⊢ K₁.ιMapBifunctor K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' =
    c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'

Tactic:
subst h'

Result:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_9, u_1} C₁
inst✝¹⁰ : Category.{u_8, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' =
    c₁.ε₁ c₂ c (c₁.prev i₁', i₂) •
      (F.map (h₁.hom i₁' (c₁.prev i₁'))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁'))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁') i₂ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{u_9, u_1} C₁
inst✝¹⁰ : Category.{u_8, u_2} C₂
inst✝⁹ : Category.{u_7, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' =
    c₁.ε₁ c₂ c (c₁.prev i₁', i₂) •
      (F.map (h₁.hom i₁' (c₁.prev i₁'))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁'))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁') i₂ j'

Tactic:
simp [hom₁]

Result:
no goals