mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) • c₁.σ c₂ c (c₁.next i₁) i₂ • (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) i₂ j' ⋯

Tactic:
smul_smul,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₁ c₂ c (i₁, i₂)) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) • c₁.σ c₂ c (c₁.next i₁) i₂ • (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) i₂ j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₁ c₂ c (i₁, i₂)) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) • c₁.σ c₂ c (c₁.next i₁) i₂ • (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) i₂ j' ⋯

Tactic:
smul_smul,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₁ c₂ c (i₁, i₂)) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    (c₂.ε₂ c₁ c (i₂, i₁) * c₁.σ c₂ c (c₁.next i₁) i₂) •
      (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ K.ιTotal c (c₁.next i₁) i₂ j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.σ c₂ c i₁ i₂ • K.d₁ c i₁ i₂ j' =
    K.flip.d₂ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
· rw [K.d₁_eq_zero _ _ _ _ h₂, K.flip.d₂_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) • c₁.σ c₂ c i₁ (c₂.next i₂) • (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯

Tactic:
smul_smul,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₂ c₂ c (i₁, i₂)) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) • c₁.σ c₂ c i₁ (c₂.next i₂) • (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₂ c₂ c (i₁, i₂)) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) • c₁.σ c₂ c i₁ (c₂.next i₂) • (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯

Tactic:
smul_smul,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ (c₁.σ c₂ c i₁ i₂ * c₁.ε₂ c₂ c (i₁, i₂)) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    (c₂.ε₁ c₁ c (i₂, i₁) * c₁.σ c₂ c i₁ (c₂.next i₂)) •
      (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.ιTotal c i₁ (c₂.next i₂) j' ⋯
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, 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 L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
x✝ : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ (L.total c₁₂).d i₁₂ i₁₂' =
    (K.total c₁₂).d i₁₂ i₁₂' ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
by
    dsimp [total]
    rw [comp_add, add_comp, mapAux.mapMap_D₁, mapAux.mapMap_D₂]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: 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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      c₁.ε₂ c₂ c (i₁, i₂) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
        c₁.ε₁ c₂ c (i₁, i₂') •
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
            (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
              (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')

Tactic:
smul_smul,

Goal state after:
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₂ c₂ c (i₁, i₂)) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
        c₁.ε₁ c₂ c (i₁, i₂') •
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
            (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
              (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: 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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₂ c₂ c (i₁, i₂)) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
        c₁.ε₁ c₂ c (i₁, i₂') •
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
            (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
              (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')

Tactic:
smul_smul,

Goal state after:
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₂ c₂ c (i₁, i₂)) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -((c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
        ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
          (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
            (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: 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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = 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₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
by
  have hj' : ComplexShape.π c₁ c₂ c ⟨i₁, i₂'⟩ = j := by
    rw [← hj, ← ComplexShape.next_π₂ c₁ c i₁ hi₂, ComplexShape.next_π₁ c₂ c hi₁ i₂]
  rw [HomologicalComplex₂.d₂_eq _ _ _ hi₂ _ hj', HomologicalComplex₂.d₂_eq _ _ _ hi₂ _
        (by rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]),
    Linear.comp_units_smul, Linear.comp_units_smul, Linear.units_smul_comp, assoc,
    ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ (c₁.prev_eq' hi₁),
    ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ hj',
    Linear.comp_units_smul, smul_smul, smul_smul,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    Functor.mapBifunctorHomologicalComplex_obj_obj_X_d,
    NatTrans.naturality_assoc, ComplexShape.ε₁_ε₂ c hi₁ hi₂, neg_mul, Units.neg_smul, neg_inj,
    smul_left_cancel_iff, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, f₂.comm]

Goal state after:
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (i₁, i₂) •
      c₁.ε₁ c₂ c (i₁, i₂) •
        (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
          (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
            (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j

Tactic:
smul_smul,

Goal state after:
case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (i₁, i₂) * c₁.ε₁ c₂ c (i₁, i₂)) •
      (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
        (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    1 •
      (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
        (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j

Tactic:
one_smul,

Goal state after:
case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      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₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h

Tactic:
smul_smul,

Goal state after:
case pos
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.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, 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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) * 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₂) ≫
          ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h