mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D₁
inst✝⁵ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
X₁ : C₁
e : L.functor.obj X₁ ≅ ρ.X₁
⊢ W₂ (R.functor.preimage (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w))

Tactic:
simp only [← R.inverseImage_eq, MorphismProperty.inverseImage_iff, Functor.map_preimage]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D₁
inst✝⁵ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁴ : L.functor.EssSurj
inst✝³ : R.functor.Full
inst✝² : R.IsInduced
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : B.HasLeftResolutions
X₂ : C₂
ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary (B.LeftResolution (R.functor.obj X₂))
X₁ : C₁
e : L.functor.obj X₁ ≅ ρ.X₁
⊢ W₂' (iso.hom.app X₁ ≫ B.functor.map e.hom ≫ ρ.w)
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := { obj := X }
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g : (Paths.of (LocQuiver W)).obj { obj := X } ⟶ (Paths.of (LocQuiver W)).obj { obj := Y }
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))

Tactic:
exact this g

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K : Plus C
n : ℤ
inst✝ : K.obj.IsStrictlyGE n
⊢ ∃ L, ∃ (_ : L.obj.IsStrictlyGE n), ∃ i, quasiIso C i

Tactic:
by
  obtain ⟨L, i, _, _, _⟩ := modelCategoryQuillen.exists_quasiIso_injective K.obj n
  let L' : CochainComplex (InjectiveObject C) ℤ :=
    HomologicalComplex.liftObjectProperty _ L inferInstance
  have hL' : L'.IsStrictlyGE n := by
    rwa [← isStrictlyGE_mapHomologicalComplex_obj_iff _ (InjectiveObject.ι _)]
  exact ⟨⟨L', n, hL'⟩, hL', ObjectProperty.homMk i, by assumption⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
        Q.map ((Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
← F.mapDerivedCategoryFactors_hom_naturality_assoc,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃) ≫
      F.mapDerivedCategoryFactors.hom.app
          ((shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle S.f).obj₁) ≫
        Q.map ((Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
          (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
            (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
              (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
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
f : X ≅ Y
⊢ f.hom.f ≫ f.inv.f = 𝟙 X.obj

Tactic:
rw [← comp_f, Iso.hom_inv_id, id_f]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
⊢ ∀ (i j k : ι),
    c.Rel i j →
      c.Rel j k →
        ((if hk : i = i₀ ∧ j = i₁ ∧ i₀ ≠ i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) ≫
            if hk : j = i₀ ∧ k = i₁ ∧ i₀ ≠ i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) =
          0

Tactic:
rintro i j k hij hjk
    dsimp
    by_cases hi : i = i₀
    · subst hi
      by_cases hj : j = i₁
      · subst hj
        nth_rw 2 [dif_neg (by tauto)]
        rw [comp_zero]
      · rw [dif_neg (by tauto), zero_comp]
    · rw [dif_neg (by tauto), zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : m + 1 = p
⊢ h.d n m ≫ h.d m p = 0

Tactic:
obtain n | (_ | _ | n) := n

Goal state after:
case pos.ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.ofNat n + 1 = m
⊢ h.d (Int.ofNat n) m ≫ h.d m p = 0

case pos.negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc 0 + 1 = m
⊢ h.d (Int.negSucc 0) m ≫ h.d m p = 0

case pos.negSucc.succ.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
hnm : Int.negSucc (0 + 1) + 1 = m
⊢ h.d (Int.negSucc (0 + 1)) m ≫ h.d m p = 0

case pos.negSucc.succ.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m p : ℤ
hmp : m + 1 = p
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = m
⊢ h.d (Int.negSucc (n + 1 + 1)) m ≫ h.d m p = 0
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : Abelian V
S₁ S₂ : ShortComplex (T ⥤ V)
f : S₁ ⟶ S₂
hf : ∀ (j : T), QuasiIso (((evaluation T V).obj j).mapShortComplex.map f)
⊢ QuasiIso f

Tactic:
by
    rw [quasiIso_iff, NatTrans.isIso_iff_isIso_app]
    exact fun j ↦ ((MorphismProperty.isomorphisms V).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
      ((homologyFunctorIso ((evaluation T V).obj j)))).app (Arrow.mk f))).1
        ((quasiIso_iff _).1 (hf j))

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:
isIso_iff₁

Goal state after:
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).app 0) ∧ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)
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:
isIso_iff₁

Goal state after:
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).app 0) ∧ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt (ofComplex Z) (n✝ + 1)

pp: case succ.hL
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj Z) (n✝ + 1)

Tactic:
· apply ofComplex_exactAt_succ

Goal state after:
case succ.hL
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n✝ : ℕ
⊢ HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj Z) (n✝ + 1)
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ IsConnected (CostructuredArrow (idealPowersToSelfLERadical J) J')

Tactic:
apply +allowSynthFailures zigzag_isConnected

Goal state after:
case inst
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ Nonempty (CostructuredArrow (idealPowersToSelfLERadical J) J')

case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
⊢ ∀ (j₁ j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j₁ j₂

Tactic:
intro j1

Goal state after:
case h
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 : CostructuredArrow (idealPowersToSelfLERadical J) J'
⊢ ∀ (j₂ : CostructuredArrow (idealPowersToSelfLERadical J) J'), Zigzag j1 j₂
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 : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (F.leftDerived n).map f =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          g ≫
        (Q.isoLeftDerivedObj F n).inv

Tactic:
by
  rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q g _ F n,
    assoc, assoc, Iso.inv_hom_id, comp_id]
  rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    ChainComplex.single₀_map_f_zero]

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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).opcyclesMap'_eq, RightHomologyMapData.smul_φQ, γ.opcyclesMap'_eq]

Goal state after:
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 ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso φ

Tactic:
isIso_iff₁

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 ι
n : ℤ
i₀ i₁ : ι
f : i₀ ⟶ i₁
inst✝ : IsIso f
φ : mk₁ f ⟶ mk₁ (inv f) := twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯
⊢ IsIso (φ.app 0) ∧ IsIso (φ.app 1)
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
n : ℤ
⊢ Mono (X.iCycles f g n)

Tactic:
dsimp [iCycles]

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
n : ℤ
⊢ Mono (kernel.ι (X.δ f g n (n + 1) ⋯))
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
n : ℤ
h : IsZero ((X.H n).obj (mk₁ g))
⊢ IsZero (X.cycles f g n)

Tactic:
by
  rw [IsZero.iff_id_eq_zero, ← cancel_mono (X.iCycles ..)]
  apply h.eq_of_tgt

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₀ 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₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ X.pOpcycles f₂ f₃ n₂ ≫ X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂ =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂

Tactic:
p_fromOpcycles,

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₀ 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₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.δ (f₁ ≫ f₂) f₃₄ n₁ n₂ hn₂ ≫
      X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.iCycles f₁ f₂ n₂ ≫ (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) =
    X.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.ιE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫ X.fromOpcycles f₄ f₅ f₄₅ h₄₅ n₁ ≫ X.δ f₂₃ f₄₅ n₁ n₂ hn₂
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₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    X.toCycles f₂ f₃ (f₂ ≫ f₃) ⋯ n₀ ≫ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
p_fromOpcycles,

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.toCycles f₂ f₃ (f₂ ≫ f₃) ⋯ n₀ ≫ X.iCycles f₂ f₃ n₀ ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁
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'
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
⊢ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ X.pOpcycles f' g' n ≫ X.fromOpcycles f' g' fg' h' n =
    (X.H n).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n).map β

Tactic:
p_fromOpcycles,

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'
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
⊢ (X.H n).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ (X.H n).map (twoδ₂Toδ₁ f' g' fg' h') =
    (X.H n).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n).map β
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₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
⊢ π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ =
    z₂ ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ X.pOpcycles f₁ f₂ n₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁

Tactic:
p_fromOpcycles,

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₁
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₁
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
z₂ : A₂ ⟶ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).X₁
hz₂ : π₂ ≫ z₁ = z₂ ≫ (X.cokernelSequenceOpcycles f₁ f₂₃ n₀ n₁ hn₁).f
⊢ π₂ ≫ π₁ ≫ z₀ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = z₂ ≫ X.δ f₁ f₂₃ n₀ n₁ ⋯ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
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 ι
i j k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)

Tactic:
have : IsIso (shortComplexMap X f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂) := by
    apply +allowSynthFailures ShortComplex.isIso_of_isIso <;> assumption

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
i' j' k' l' : ι
f₁' : i' ⟶ j'
f₂' : j' ⟶ k'
f₃' : k' ⟶ l'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂' f₃'
n₀ n₁ n₂ : ℤ
h₀ : IsIso ((X.H n₀).map ((functorArrows ι 2 3 3 isIso_map._proof_6 shortComplexMap._proof_3).map α))
h₁ : IsIso ((X.H n₁).map ((functorArrows ι 1 2 3 isIso_map._proof_8 isIso_map._proof_6).map α))
h₂ : IsIso ((X.H n₂).map ((functorArrows ι 0 1 3 isIso_map._proof_10 isIso_map._proof_12).map α))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
this : IsIso (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ ⋯ ⋯)
⊢ IsIso (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
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 ι
i₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
obtain ⟨A₁, π₁, _, y₂, hy₂⟩ :=
    surjective_up_to_refinements_of_epi (X.pOpcycles f₁₂ f₃ n₁) x₂

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₀ i₁ i₂ i₃ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ X.opcycles f₁₂ f₃ n₁
hx₂ : x₂ ≫ X.opcyclesToE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
y₂ : A₁ ⟶ (X.H n₁).obj (mk₁ f₁₂)
hy₂ : π₁ ≫ x₂ = y₂ ≫ X.pOpcycles f₁₂ f₃ n₁
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
f g : α → β
h : f =ᶠ[l] g
⊢ EventuallyConst f l ↔ EventuallyConst g l

Tactic:
by
  simp only [EventuallyConst, map_congr h]

Goal state after: