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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : Cylinder X.obj
left✝ : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject C ⥤ (weakEquivalences (FibrantObject C)).Localization := (weakEquivalences (FibrantObject C)).Q
⊢ L.map (homMk P.i₀) = L.map (homMk P.i₁)

Tactic:
have := Localization.inverts L (weakEquivalences _) (homMk P.π) (by
    simp only [← weakEquivalence_iff, weakEquivalence_homMk_iff]
    infer_instance)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : Cylinder X.obj
left✝ : P.IsVeryGood
h : P.LeftHomotopy f.hom g.hom
L : FibrantObject C ⥤ (weakEquivalences (FibrantObject C)).Localization := (weakEquivalences (FibrantObject C)).Q
this : IsIso (L.map (homMk P.π))
⊢ L.map (homMk P.i₀) = L.map (homMk P.i₁)
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
F : C₁ ⥤ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) := (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
X : (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
⊢ ∀ (j₂ : (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g), Zigzag X j₂

Tactic:
Y

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
F : C₁ ⥤ C₂
X₂ : C₁
X₃ : C₂
g : F.obj X₂ ⟶ X₃
Z : Type (max (max u₁ v₂) v₁) := (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
X₀ : Z := StructuredArrow.mk (CostructuredArrow.homMk (𝟙 (CostructuredArrow.mk g).left) ⋯)
φ : (X : Z) → X₀ ⟶ X
this : Nonempty Z
X Y : (mk (𝟭 C₁) F F (𝟭 C₂) (𝟙 F)).StructuredArrowRightwards g
⊢ Zigzag X Y
Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
inst✝¹ : K.IsKProjective
inst✝ : L.IsKProjective
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
  rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
  obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
  refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
  · simp [hg]
  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j j' : ι
h : j = j'
⊢ ¬c.Rel j j'

Tactic:
subst h

Goal state after:
ι : Type u_1
c : ComplexShape ι
inst✝ : c.HasNoLoop
j : ι
⊢ ¬c.Rel j j
Module: Mathlib.Algebra.Homology.DifferentialObject

Goal state before:
pp: β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : i + b = j
⊢ (f.f i ≫ if h : i + b = j then Y.d i ≫ Y.objEqToHom ⋯ else 0) =
    (if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ f.f j

Tactic:
subst h

Goal state after:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
⊢ (f.f i ≫ if h : i + b = i + b then Y.d i ≫ Y.objEqToHom ⋯ else 0) =
    (if h : i + b = i + b then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ f.f (i + b)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X Y : DifferentialObject S C
h : X = Y
⊢ (eqToHom h).f = eqToHom ⋯

Tactic:
subst h

Goal state after:
S : Type u_1
inst✝³ : AddMonoidWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ (eqToHom ⋯).f = eqToHom ⋯
Module: Mathlib.Algebra.Homology.EulerCharacteristic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ ∑ᶠ (i : ι), ↑(c.χ i) * ↑(Module.finrank R ↑(X i)) = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))

Tactic:
finsum_eq_sum_of_support_subset

Goal state after:
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ ∑ i ∈ ?s, ↑(c.χ i) * ↑(Module.finrank R ↑(X i)) = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))

case s
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ Finset ι

case h
R : Type u_1
inst✝¹ : Ring R
ι : Type u_2
c : ComplexShape ι
inst✝ : c.EulerCharSigns
X : GradedObject ι (ModuleCat R)
indices : Finset ι
h_support : finrankSupport X ⊆ ↑indices
⊢ (Function.support fun i ↦ ↑(c.χ i) * ↑(Module.finrank R ↑(X i))) ⊆ ↑?s
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case zero.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m✝ : ℤ
m : ℕ
hnm : Int.negSucc 0 + 1 ≠ Int.ofNat (m + 1)
⊢ h.d (Int.negSucc 0) (Int.ofNat (m + 1)) = 0

Tactic:
· rfl

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (twoδ₂Toδ₁ f g fg h)

Tactic:
rw [isIso_iff₁]
  constructor <;> dsimp <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (twoδ₁Toδ₀ f g fg h)

Tactic:
rw [isIso_iff₁]
  constructor <;> dsimp <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X Y : Karoubi C
f : X ⟶ Y
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
dsimp at τ ⊢
        have h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f := by simp
        have h₂ := τ.naturality f.f
        have h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p := by simp
        dsimp at h₂
        rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ { X₁ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₁,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ C).obj Z)).X₂,
        f := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
              (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
          (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂

Tactic:
dsimp
        refine (ShortComplex.exact_and_epi_g_iff_of_iso ?_).2
          ⟨exact_d_f (Projective.π Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
          (by simp [ofComplex]) (by simp)

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
⊢ (singleObjApplyIsoOfEq j X i h).inv ≫ (single j).map f i = f ≫ (singleObjApplyIsoOfEq j Y i h).inv

Tactic:
subst h

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (singleObjApplyIsoOfEq i X i ⋯).inv ≫ (single i).map f i = f ≫ (singleObjApplyIsoOfEq i Y i ⋯).inv
Module: Mathlib.CategoryTheory.GradedObject.Single

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X Y : C
f : X ⟶ Y
i : J
h : i = j
⊢ (single j).map f i ≫ (singleObjApplyIsoOfEq j Y i h).hom = (singleObjApplyIsoOfEq j X i h).hom ≫ f

Tactic:
subst h

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
X Y : C
f : X ⟶ Y
i : J
⊢ (single i).map f i ≫ (singleObjApplyIsoOfEq i Y i ⋯).hom = (singleObjApplyIsoOfEq i X i ⋯).hom ≫ f
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case pos
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
j' : J
h✝ : (0, j') ∈ p ⁻¹' {j}
h : j' = j
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j'), h✝⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(0, j'), h✝⟩

Tactic:
subst h

Goal state after:
case pos
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j' : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j')
h : (0, j') ∈ p ⁻¹' {j'}
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j') ⟨(0, j'), h⟩ ≫
      e.inv.app (Y j') ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j') ≫ s.inj ⟨(0, j'), ⋯⟩ =
    s.inj ⟨(0, j'), h⟩
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom =
    (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ

Tactic:
rw [← cancel_mono (mapBifunctorLeftUnitor F X e p hp Y').inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, mapBifunctorLeftUnitor_inv_naturality, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: case pos
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
j' : J
h✝ : (j', 0) ∈ p ⁻¹' {j}
h : j' = j
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j', 0), h✝⟩ ≫
      e.inv.app (X j) ≫ (F.obj (X j)).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j, 0), ⋯⟩ =
    s.inj ⟨(j', 0), h✝⟩

Tactic:
subst h

Goal state after:
case pos
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j' : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j')
h : (j', 0) ∈ p ⁻¹' {j'}
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j') ⟨(j', 0), h⟩ ≫
      e.inv.app (X j') ≫ (F.obj (X j')).map (singleObjApplyIso 0 Y).inv ≫ s.inj ⟨(j', 0), ⋯⟩ =
    s.inj ⟨(j', 0), h⟩
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f g fg h) = 0

Tactic:
subst h

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

Goal state before:
pp: 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
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) = 0

Tactic:
subst h

Goal state after:
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
n₀ : ℤ
⊢ (X.H n₀).map (twoδ₂Toδ₁ f g (f ≫ g) ⋯) ≫ (X.H n₀).map (twoδ₁Toδ₀ f g (f ≫ g) ⋯) = 0
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.H n₀).map (twoδ₁Toδ₀ f g fg h) ≫ X.δ f g n₀ n₁ hn₁ = 0

Tactic:
subst h

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g fg h n₀ n₁ hn₁).Exact

Tactic:
subst h

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₁ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ : ℤ
⊢ (X.sc₂ f g fg h n₀).Exact

Tactic:
subst h

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
⊢ (X.sc₂ f g (f ≫ g) ⋯ n₀).Exact
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₃ f g fg h n₀ n₁ hn₁).Exact

Tactic:
subst h

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.sc₃ f g (f ≫ g) ⋯ n₀ n₁ hn₁).Exact
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''
α'' : mk₂ f g ⟶ mk₂ f'' g''
n : ℤ
h : α ≫ α' = α''
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' α'' n

Tactic:
subst h

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 : ι
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 : ℤ
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n = X.cyclesMap f g f'' g'' (α ≫ α') n
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''
α'' : mk₂ f g ⟶ mk₂ f'' g''
n : ℤ
h : α ≫ α' = α''
⊢ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' α'' n

Tactic:
subst h

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 : ι
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 : ℤ
⊢ X.opcyclesMap f g f' g' α n ≫ X.opcyclesMap f' g' f'' g'' α' n = X.opcyclesMap f g f'' g'' (α ≫ α') n
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₁
⊢ X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁ ≫
      X.opcyclesMap f₁ f₂ f₁ f₂₃ (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁ ≫ X.fromOpcycles f₁ f₂₃ (f₁ ≫ f₂ ≫ f₃) ⋯ n₁ =
    0

Tactic:
X.opcyclesMap_fromOpcycles f₁ f₂ f₁ f₂₃ f₁₂ h₁₂
    (f₁ ≫ f₂ ≫ f₃) (by rw [h₂₃]) (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃)
    (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) (by rw [reassoc_of% h₁₂])) n₁ rfl rfl,

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₁₂
f₂₃ : j ⟶ l
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.H n₁).map (twoδ₂Toδ₁ f₁₂ f₃ (f₁ ≫ f₂ ≫ f₃) ⋯) = 0
Module: Mathlib.Algebra.Homology.SpectralSequence.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence C c r₀
pq : κ
r r' : ℤ
h : r = r'
hr : r₀ ≤ r
⊢ (E.page r ⋯).X pq = (E.page r' ⋯).X pq

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence C c r₀
pq : κ
r : ℤ
hr : r₀ ≤ r
⊢ (E.page r ⋯).X pq = (E.page r ⋯).X pq
Module: Mathlib.Algebra.Homology.SpectralObject.Page

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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.EIsoH f (n₁ - 1) n₁ n₂ hn₁ hn₂).inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂

Tactic:
dsimp [EIsoH]

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 ι
n₁ n₂ : ℤ
hn₂ : n₁ + 1 = n₂
i j : ι
f : i ⟶ j
hn₁ : n₁ - 1 + 1 = n₁
h : (X.shortComplex (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).LeftHomologyData :=
  (X.homologyDataIdId f (n₁ - 1) n₁ n₂ hn₁ hn₂).left
this : h.cyclesIso.inv = X.toCycles (𝟙 i) f f ⋯ n₁ ≫ (X.cyclesIso (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂).inv
⊢ (X.homologyDataIdId f (n₁ - 1) n₁ n₂ ⋯ ⋯).left.homologyIso.inv =
    X.toCycles (𝟙 i) f f ⋯ n₁ ≫ X.πE (𝟙 i) f (𝟙 j) (n₁ - 1) n₁ n₂ hn₁ hn₂
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
⊢ n₂ = data.deg pq''

Tactic:
have := data.hc r _ _ h

Goal state after:
C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq' pq'' : κ
hpq' : (c r).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq' pq''
this : data.deg pq' + 1 = data.deg pq''
⊢ n₂ = data.deg pq''