mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove 0) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
φ : (stdSimplex.obj Δ).left _⦋n⦌
i✝ : Fin (unop (op ⦋n + 1 + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.predAbove i✝.succ) =
    shiftFun (fun x ↦ (SimplexCategory.Hom.toOrderHom φ.down) (i.predAbove x)) i✝.succ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) 0 ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ Fin.cases ((WidePullback.base fun x ↦ f.hom) ≫ S.section_) (WidePullback.π fun x ↦ f.hom) i✝.succ ≫ f.hom =
    WidePullback.base fun x ↦ f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ∀ (j : Fin ((unop (op ⦋0⦌)).len + 1)), 𝟙 f.left ≫ f.hom = f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.«_@»._internal._hyg.0.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
i₂ i₂' : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i : I₂
i✝ j✝ : I₁
a✝ : c₁.Rel i✝ j✝
⊢ (f.f i✝).f i ≫ (L.flip.X i).d i✝ j✝ = (K.flip.X i).d i✝ j✝ ≫ (f.f j✝).f i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
i✝ : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ((ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i✝¹ j✝ : I₂
a✝ : c₂.Rel i✝¹ j✝
i✝ : I₁
⊢ ({ f := fun j ↦ (f.f j).f i✝¹, comm' := ⋯ } ≫ L.flip.d i✝¹ j✝).f i✝ =
    (K.flip.d i✝¹ j✝ ≫ { f := fun j ↦ (f.f j).f j✝, comm' := ⋯ }).f i✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ : I₁
⊢ ∀ (i j : I₂),
    c₂.Rel i j →
      (Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).X i)).hom ≫
          (((flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁).obj K).X i₁).d i j =
        (((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).d i j ≫
          (Iso.refl ((((𝟭 (HomologicalComplex₂ C c₁ c₂)).obj K).X i₁).X j)).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₂ c₁
i₂ : I₂
⊢ ∀ (i j : I₁),
    c₁.Rel i j →
      (Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).X i)).hom ≫
          (((𝟭 (HomologicalComplex₂ C c₂ c₁)).obj K).X i₂).d i j =
        (((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).d i j ≫
          (Iso.refl ((((flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂).obj K).X i₂).X j)).hom

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) 0 =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
i✝ : Fin (n + 2)
⊢ (ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.π (fun x ↦ f.hom) i✝.succ

Tactic:
simp

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * c₂.ε₁ c₁ c₁₂ (i₂, i₁) = c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂'

Tactic:
by
    apply mul_right_cancel (b := ComplexShape.ε₂ c₁ c₂ c₁₂ (i₁, i₂))
    rw [mul_assoc]
    nth_rw 2 [mul_comm]
    rw [← mul_assoc, ComplexShape.σ_ε₂ c₁ c₁₂ i₁ h₂, mul_comm, ← mul_assoc,
      Int.units_mul_self, one_mul, mul_comm, ← mul_assoc, Int.units_mul_self, one_mul]

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ((ExtraDegeneracy.s f S n ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.predAbove i_1)) ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.predAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S (n + 1)) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ K₁' : HomologicalComplex C₁ c₁
f : K₁ ⟶ K₁'
K₂ : HomologicalComplex C₂ c₂
⊢ ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂) ≫
          (((F.mapBifunctorHomologicalComplexObj c₂ K₁').obj K₂).X i₁).d i₂ i₂' =
        (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' ≫
          ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂')

Tactic:
simp

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

Goal state before:
pp: 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
i₁✝ : I₂
i₂✝ : I₁
hi✝ : c₂.π c₁ c (i₁✝, i₂✝) = j
⊢ (K.flip.ιTotal c i₁✝ i₂✝ j hi✝ ≫
      (K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) ≫
        K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) =
    K.flip.ιTotal c i₁✝ i₂✝ j hi✝ ≫ 𝟙 ((K.flip.total c).X j)

Tactic:
simp

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

Goal state before:
pp: 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
i₁✝ : I₁
i₂✝ : I₂
hi✝ : c₁.π c₂ c (i₁✝, i₂✝) = j
⊢ (K.ιTotal c i₁✝ i₂✝ j hi✝ ≫
      (K.totalDesc fun i₁ i₂ h ↦ c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) ≫
        K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) =
    K.ιTotal c i₁✝ i₂✝ j hi✝ ≫ 𝟙 ((K.total c).X j)

Tactic:
simp

Goal state after:
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = -K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂''

Tactic:
simp

Goal state after:
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).hom ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
simp

Goal state after:
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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
x₁ : I₁
x₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (x₁, x₂) = i₁₂
⊢ (XXIsoOfEq C c₁ c₂ K ⋯ ⋯).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ ⋯

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₂
inst✝¹¹ : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ : I₁
i₂ : I₂
j : J
hj : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.π c₂ c (i₁, i₂) = j

Tactic:
by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, hj]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
X Y : t.Category
f : X ⟶ Y
m : A
⊢ (shiftFunctor t.Category m).map f = (t.shiftIso m).hom.app X ≫ (shiftFunctor C m).map f ≫ (t.shiftIso m).inv.app Y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X
⊢ (shiftFunctorAdd' C i j k h).hom.app X =
    𝟙 ((shiftFunctor C k).obj X) ≫
      (shiftFunctorAdd' C i j k h).hom.app X ≫
        (shiftFunctor C j).map (𝟙 ((shiftFunctor C i).obj X)) ≫ 𝟙 ((shiftFunctor C j).obj ((shiftFunctor C i).obj X))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X
⊢ (shiftFunctorAdd' C i j k h).inv.app X =
    𝟙 ((shiftFunctor C j).obj ((shiftFunctor C i).obj X)) ≫
      (shiftFunctor C j).map (𝟙 ((shiftFunctor C i).obj X)) ≫
        (shiftFunctorAdd' C i j k h).inv.app X ≫ 𝟙 ((shiftFunctor C k).obj X)

Tactic:
simp

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

Goal state before:
pp: case a
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)
⊢ (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.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_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
    · rw [HomologicalComplex₂.d₁_eq _ _ h₃ _ _ (by rw [← h, ComplexShape.next_π₁ c₂ c h₃]),
        Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, Linear.units_smul_comp, assoc,
        ιMapBifunctor_hom₁ _ _ _ _ i₁ _ _ _ _ _ (c₁.prev_eq' h₃),
        Linear.comp_units_smul, smul_smul, Int.units_mul_self, one_smul,
        ιMapBifunctorOrZero_eq]
    · rw [K₁.shape _ _ h₃, Functor.map_zero, zero_app, zero_comp,
        HomologicalComplex₂.d₁_eq_zero _ _ _ _ _ h₃, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n})
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => ⟨(a, b - y), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => ⟨(a, b + y), ⋯⟩)
        x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n : ℤ
x✝ : ↑((up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + y})
⊢ (fun x ↦
        match x with
        | ⟨(a, b), h⟩ => ⟨(a, b + y), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(a, b), h⟩ => ⟨(a, b - y), ⋯⟩)
        x✝) =
    x✝

Tactic:
simp

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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
⊢ mapBifunctorMap f₁ f₂ F c =
    (K₁.mapBifunctorFlipIso K₂ F c).inv ≫ mapBifunctorMap f₂ f₁ F.flip c ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom

Tactic:
simp

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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
⊢ (K₁.mapBifunctorFlipIso K₂ F c).inv ≫ mapBifunctorMap f₂' f₁ F.flip c ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom =
    mapBifunctorMap f₁ f₂' F c

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x✝¹ x✝ : ℤ
⊢ (fun n ↦ -n) x✝¹ = (fun n ↦ -n) x✝ → x✝¹ = x✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {i₁ i₂ : ℤ}, (up ℤ).Rel i₁ i₂ → (down ℤ).Rel (-i₁) (-i₂)

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℤ
n : ℤ
⊢ n = ComplexShape.embeddingUpIntDownInt.f (ComplexShape.embeddingDownIntUpInt.f n)

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ ComplexShape.embeddingDownIntUpInt.f (ComplexShape.embeddingUpIntDownInt.f n) = n

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (-(n + 1)) (-n)

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel n (n + 1)

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
simp

Goal state after: