mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso f).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝²)) (Iso.refl (F.obj w✝¹)) ⋯).hom =
    homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.SpectralObject

Goal state before:
pp: case e'_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
w✝² w✝¹ w✝ : ι'
f : w✝² ⟶ w✝¹
g : w✝¹ ⟶ w✝
this :
  X.ω₁.map (homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯) ≫ X.δ'.app (mk₂ (F.map f) (F.map g)) =
    X.δ'.app ((F.mapComposableArrows 2).obj (mk₂ f g)) ≫
      (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (𝟙 (F.obj w✝²)) (𝟙 (F.obj w✝¹)) ⋯))
⊢ (F.mapComposableArrowsObjMk₁Iso g).inv ≫ (isoMk₁ (Iso.refl (F.obj w✝¹)) (Iso.refl (F.obj w✝)) ⋯).hom =
    homMk₁ (𝟙 (F.obj w✝¹)) (𝟙 (F.obj w✝)) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙
              HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
              (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
simp only [Functor.comp_map, Iso.hom_inv_id_app_assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
⊢ F.whiskerLeft π₁Toπ₂ ≫ F.whiskerLeft π₂Toπ₃ = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₁ ≫
      { X₁ := Y✝ ⋙ π₁, X₂ := Y✝ ⋙ π₂, X₃ := Y✝ ⋙ π₃, f := Y✝.whiskerLeft π₁Toπ₂, g := Y✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.f =
    { X₁ := X✝ ⋙ π₁, X₂ := X✝ ⋙ π₂, X₃ := X✝ ⋙ π₃, f := X✝.whiskerLeft π₁Toπ₂, g := X✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.f ≫
      whiskerRight φ π₂

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : J ⥤ ShortComplex C
φ : X✝ ⟶ Y✝
⊢ whiskerRight φ π₂ ≫
      { X₁ := Y✝ ⋙ π₁, X₂ := Y✝ ⋙ π₂, X₃ := Y✝ ⋙ π₃, f := Y✝.whiskerLeft π₁Toπ₂, g := Y✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.g =
    { X₁ := X✝ ⋙ π₁, X₂ := X✝ ⋙ π₂, X₃ := X✝ ⋙ π₃, f := X✝.whiskerLeft π₁Toπ₂, g := X✝.whiskerLeft π₂Toπ₃,
          zero := ⋯ }.g ≫
      whiskerRight φ π₃

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₁.obj x)) ⋯).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).f =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).f ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) ⋯).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : ShortComplex (J ⥤ C)
⊢ (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₂.obj x)) ⋯).hom ≫
      ((functor J C ⋙ inverse J C).obj x✝).g =
    ((𝟭 (ShortComplex (J ⥤ C))).obj x✝).g ≫
      (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj x✝).X₃.obj x)) ⋯).hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : ShortComplex (J ⥤ C)} (f : X ⟶ Y),
    (𝟭 (ShortComplex (J ⥤ C))).map f ≫
        (isoMk (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₁.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₂.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj Y).X₃.obj x)) ⋯) ⋯ ⋯).hom =
      (isoMk (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₁.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₂.obj x)) ⋯)
            (NatIso.ofComponents (fun x ↦ Iso.refl (((𝟭 (ShortComplex (J ⥤ C))).obj X).X₃.obj x)) ⋯) ⋯ ⋯).hom ≫
        (functor J C ⋙ inverse J C).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
x✝ : J ⥤ ShortComplex C
⊢ ∀ {X Y : J} (f : X ⟶ Y),
    ((inverse J C ⋙ functor J C).obj x✝).map f ≫
        (isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₁)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₂)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj Y).X₃) ⋯ ⋯).hom =
      (isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₁)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₂)
            (Iso.refl (((inverse J C ⋙ functor J C).obj x✝).obj X).X₃) ⋯ ⋯).hom ≫
        ((𝟭 (J ⥤ ShortComplex C)).obj x✝).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
⊢ ∀ {X Y : J ⥤ ShortComplex C} (f : X ⟶ Y),
    (inverse J C ⋙ functor J C).map f ≫
        (NatIso.ofComponents
            (fun x ↦
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj Y).obj x).X₃) ⋯ ⋯)
            ⋯).hom =
      (NatIso.ofComponents
            (fun x ↦
              isoMk (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₁)
                (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₂)
                (Iso.refl (((inverse J C ⋙ functor J C).obj X).obj x).X₃) ⋯ ⋯)
            ⋯).hom ≫
        (𝟭 (J ⥤ ShortComplex C)).map f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (x y : R) (b : S₁ ⟶ S₂), (x * y) • b = x • y • b

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (b : S₁ ⟶ S₂), 1 • b = b

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (a : R), a • 0 = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (a : R) (x y : S₁ ⟶ S₂), a • (x + y) = a • x + a • y

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (r s : R) (x : S₁ ⟶ S₂), (r + s) • x = r • x + s • x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
⊢ ∀ (x : S₁ ⟶ S₂), 0 • x = 0

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst✝ : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ π ((i₁, 0, i₃).1, τ.p₂₃ (i₁, 0, i₃).2) = π (i₁, i₃)

Tactic:
τ.h₃ i₃

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst✝ : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
⊢ π ((i₁, 0, i₃).1, i₃) = π (i₁, i₃)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: case e'_2.e'_6.e'_8
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
e_3✝ : (X.H n₀).obj (mk₁ g) = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯))
e_4✝ : (X.H n₀).obj (mk₁ g') = (X.H n₀).obj (mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯))
e_6✝ : mk₁ g = mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)
e_7✝ : mk₁ g' = mk₁ (Precomp.map (mk₁ g') f' 1 2 ⋯)
⊢ β = homMk₁ (α.app 1) (β.app 1) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: case e'_3.e'_7
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
e_1✝ :
  ((X.H n₀).obj (mk₁ g) ⟶ (X.H n₁).obj (mk₁ f')) =
    ((X.H n₀).obj (mk₁ (Precomp.map (mk₁ g) f 1 2 ⋯)) ⟶ (X.H n₁).obj (mk₁ f'))
⊢ α = homMk₁ (α.app 0) (α.app 1) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
Z : C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
i₁₂ : I
h' : i₁ + i₂ = i₁₂
⊢ i₁₂ + i₃ = j

Tactic:
rw [← h', h]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝¹⁴ : AddMonoid I
C : Type u_1
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝¹¹ : X₁.HasTensor X₂
inst✝¹⁰ : (tensorObj X₁ X₂).HasTensor X₃
inst✝⁹ : X₂.HasTensor X₃
inst✝⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝⁷ : Y₁.HasTensor Y₂
inst✝⁶ : (tensorObj Y₁ Y₂).HasTensor Y₃
inst✝⁵ : Y₂.HasTensor Y₃
inst✝⁴ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
inst✝³ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝² : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝¹ : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃
inst✝ : Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ f ⟶ mk₁ f'
n : ℤ
hβ : β = homMk₁ (α.app 0) (α.app 1) ⋯
⊢ X.pOpcycles f g n ≫ X.opcyclesMap f g f' g' α n = (X.H n).map β ≫ X.pOpcycles f' g' n

Tactic:
by
  subst hβ
  simp [opcyclesMap]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
α' : mk₂ f' g' ⟶ mk₂ f'' g''
n : ℤ
⊢ homMk₁ (α.app 0) (α.app 1) ⋯ ≫ homMk₁ (α'.app 0) (α'.app 1) ⋯ = homMk₁ ((α ≫ α').app 0) ((α ≫ α').app 1) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
rw [← cancel_epi (X.toCycles f₂ f₃ _ rfl n₀),
    toCycles_Ψ_assoc .., p_fromOpcycles, toCycles_i_assoc]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f₁ (f₂ ≫ f₃) n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: case h₀
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
fg : i ⟶ k
h : f ≫ g = fg
fg' : i' ⟶ k'
h' : f' ≫ g' = fg'
α : mk₂ f g ⟶ mk₂ f' g'
β : mk₁ fg ⟶ mk₁ fg'
n : ℤ
hβ₀ : β.app 0 = α.app 0
hβ₁ : β.app 1 = α.app 2
⊢ app' (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') 0 homMk₁._proof_4 =
    app' (twoδ₂Toδ₁ f g fg h ≫ β) 0 homMk₁._proof_4

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₃' : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₃' : i₂ ⟶ i₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this : Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)
⊢ 𝟙 (mk₂ f₁ f₂) = homMk₂ (α.app 0) (α.app 1) (α.app 2) ⋯ ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: case e'_5
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ homMk₁ (𝟙 ((mk₃ f₁ f₂ f₃).obj 1)) (𝟙 ((mk₃ f₁ f₂ f₃).obj 2)) ⋯ = 𝟙 (mk₁ f₂)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ homMk₁ (𝟙 ((mk₃ f₁ f₂ f₃).obj 0)) (𝟙 ((mk₃ f₁ f₂ f₃).obj 1)) ⋯ = 𝟙 (mk₁ f₁)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 𝟙 (mk₂ f₄ f₅) =
    homMk₂ ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 1) ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 2)
      ((fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃).app 3) ⋯ ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: case e'_5
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ homMk₁ (𝟙 ((mk₃ f₂₃ f₄ f₅).obj 2)) (𝟙 ((mk₃ f₂₃ f₄ f₅).obj 3)) ⋯ = 𝟙 (mk₁ f₅)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: case e'_5
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ homMk₁ (𝟙 ((mk₃ f₂₃ f₄ f₅).obj 1)) (𝟙 ((mk₃ f₂₃ f₄ f₅).obj 2)) ⋯ = 𝟙 (mk₁ f₄)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A : C
z :
  A ⟶
    { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
        f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.X₂
hz :
  z ≫
      { X₁ := X.cycles f₁₂ f₃ n₀, X₂ := X.cycles f₂ f₃ n₀, X₃ := X.opcycles f₁ f₂ n₁,
          f := X.cyclesMap f₁₂ f₃ f₂ f₃ (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂) n₀, g := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁, zero := ⋯ }.g =
    0
⊢ 𝟙 (mk₁ f₃) = homMk₁ ((threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1) ((threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Differentials

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
A✝ : C
z₀ :
  A✝ ⟶
    { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
        g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.X₂
hz₀ :
  z₀ ≫
      { X₁ := X.cycles f₂ f₃ n₀, X₂ := X.opcycles f₁ f₂ n₁, X₃ := X.opcycles f₁ f₂₃ n₁, f := X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁,
          g := X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁, zero := ⋯ }.g =
    0
A₁ : C
π₁ : A₁ ⟶ A✝
w✝ : Epi π₁
z₁ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁)
hz₁ : π₁ ≫ z₀ = z₁ ≫ X.pOpcycles f₁ f₂ n₁
⊢ 𝟙 (mk₁ f₁) = homMk₁ ((threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0) ((threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1) ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ homMk₁ (𝟙 ((mk₃ f₁ f₂ f₃).obj 2)) (𝟙 ((mk₃ f₁ f₂ f₃).obj 3)) ⋯ = 𝟙 (mk₁ f₃)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ homMk₁ (𝟙 ((mk₃ f₁ f₂ f₃).obj 1)) (𝟙 ((mk₃ f₁ f₂ f₃).obj 2)) ⋯ = 𝟙 (mk₁ f₂)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: case e'_2
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ homMk₁ (𝟙 ((mk₃ f₁ f₂ f₃).obj 0)) (𝟙 ((mk₃ f₁ f₂ f₃).obj 1)) ⋯ = 𝟙 (mk₁ f₁)

Tactic:
cat_disch

Goal state after: