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

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₁ : { obj := K₁, property := ⋯ } ⟶ (CochainComplex.Plus.localizerMorphism C).functor.obj { obj := K₂, property := ⋯ }
f₀ :
  { obj := K₁, property := ⋯ }.obj ⟶
    ((CochainComplex.Plus.localizerMorphism C).functor.obj { obj := K₂, property := ⋯ }).obj
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map f₁
⊢ ∃ P,
    (L C).functor.map P.p₀ = (L C).functor.map P.p₁ ∧
      Nonempty ((P.map (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy (ObjectProperty.homMk f₀) f₁)

Tactic:
obtain ⟨f₁, rfl⟩ := ObjectProperty.homMk_surjective f₁

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ :
  { obj := K₁, property := ⋯ }.obj ⟶
    ((CochainComplex.Plus.localizerMorphism C).functor.obj { obj := K₂, property := ⋯ }).obj
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ∃ P,
    (L C).functor.map P.p₀ = (L C).functor.map P.p₁ ∧
      Nonempty
        ((P.map (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy (ObjectProperty.homMk f₀)
          (ObjectProperty.homMk f₁))
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
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ ShiftedHom.map hS.singleδ F.mapDerivedCategory =
    (F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃ ≫
      ⋯.singleδ ≫ (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)

Tactic:
by
  simp [← hS.mapShiftedHom_singleδ'_assoc, ← Functor.map_comp]

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₁
h : i₀ ≠ i₁
⊢ (double f hi₀₁).X i₁ = X₁

Tactic:
dsimp [double]
    rw [if_neg h.symm, if_pos rfl]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
⊢ Small.{w, max t v} (K ⟶ L)

Tactic:
let emb (f : K ⟶ L) (i : Shrink.{w} ι) := (equivShrink.{w} _) (f.f ((equivShrink _).symm i))

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, t} ι
K L : HomologicalComplex C c
emb : (K ⟶ L) → (i : Shrink.{w, t} ι) → Shrink.{w, v} (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i)) :=
  fun f i ↦ (equivShrink (K.X ((equivShrink ι).symm i) ⟶ L.X ((equivShrink ι).symm i))) (f.f ((equivShrink ι).symm i))
⊢ Small.{w, max t v} (K ⟶ L)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
⊢ δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (K.d p' p ≫ f) h'

Tactic:
by_cases hp : p' + 1 = p
  · dsimp only [toSingleMk]
    rw [δ_single _ n n' (by lia) p' (q + 1) (by lia) rfl]
    simp
  · simp [δ_shape n n' (by lia), HomologicalComplex.shape K p' p (by simp; lia)]

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₃
⊢ r (i₁, 0, i₃) = π (i₁, i₃)

Tactic:
← τ.hp₂₃,

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, τ.p₂₃ (i₁, 0, i₃).2) = π (i₁, i₃)
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₀) ⋯
this : IsIso φ
⊢ (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯)

Tactic:
← Functor.map_comp

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₀) ⋯
this : IsIso φ
⊢ (X.H n).map φ = (X.H n).map (twoδ₂Toδ₁ f (inv f) (𝟙 i₀) ⋯ ≫ twoδ₁Toδ₀ f (inv f) (𝟙 i₀) ⋯)
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 : ℤ
⊢ X.cyclesMap f g f' g' α n ≫ X.cyclesMap f' g' f'' g'' α' n ≫ X.iCycles f'' g'' n =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n

Tactic:
X.cyclesMap_i f' g' f'' g'' α' _ n 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 : ι
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.iCycles f' g' n ≫ (X.H n).map (homMk₁ (α'.app 1) (α'.app 2) ⋯) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles 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''
n : ℤ
⊢ X.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ (X.H n).map (homMk₁ (α'.app 1) (α'.app 2) ⋯) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles f'' g'' n

Tactic:
← Functor.map_comp

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.iCycles f g n ≫ (X.H n).map (homMk₁ (α.app 1) (α.app 2) ⋯ ≫ homMk₁ (α'.app 1) (α'.app 2) ⋯) =
    X.cyclesMap f g f'' g'' (α ≫ α') n ≫ X.iCycles 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₀ 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₃₄
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.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
by rw [δ_δ_assoc .., zero_comp]

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'
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 (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) = (X.H n).map β ≫ (X.H n).map (twoδ₁Toδ₀ f' g' fg' h')

Tactic:
← Functor.map_comp

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 (twoδ₁Toδ₀ f g fg h ≫ homMk₁ (α.app 1) (α.app 2) ⋯) = (X.H n).map (β ≫ twoδ₁Toδ₀ f' g' fg' h')
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) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') = (X.H n).map (twoδ₂Toδ₁ f g fg h) ≫ (X.H n).map β

Tactic:
← Functor.map_comp

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) ⋯ ≫ twoδ₂Toδ₁ f' g' fg' h') = (X.H n).map (twoδ₂Toδ₁ f g fg h ≫ β)
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
fg : i ⟶ k
h : f ≫ g = fg
n : ℤ
⊢ (X.opcyclesIsoKernel f g fg h n).hom ≫ (Fork.ofι (kernel.ι (X.kernelSequenceOpcycles f g fg h n).g) ⋯).ι =
    Fork.ι (KernelFork.ofι (X.kernelSequenceOpcycles f g fg h n).f ⋯)

Tactic:
by
      simp [← cancel_epi (X.pOpcycles f g n)]

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

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₀).map (homMk₁ (α.app 2 ≫ β.app 2) (α.app 3 ≫ β.app 3) ⋯) =
    (X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯) ≫ (X.H n₀).map (homMk₁ (β.app 2) (β.app 3) ⋯)

Tactic:
← Functor.map_comp

Goal state after:
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₀).map (homMk₁ (α.app 2 ≫ β.app 2) (α.app 3 ≫ β.app 3) ⋯) =
    (X.H n₀).map (homMk₁ (α.app 2) (α.app 3) ⋯ ≫ homMk₁ (β.app 2) (β.app 3) ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (homMk₁ (α.app 1 ≫ β.app 1) (α.app 2 ≫ β.app 2) ⋯) =
    (X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯) ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)

Tactic:
← Functor.map_comp

Goal state after:
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₁).map (homMk₁ (α.app 1 ≫ β.app 1) (α.app 2 ≫ β.app 2) ⋯) =
    (X.H n₁).map (homMk₁ (α.app 1) (α.app 2) ⋯ ≫ homMk₁ (β.app 1) (β.app 2) ⋯)
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.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)

Tactic:
reassoc_of% hz₁,

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.pOpcycles f₁ f₂ n₁ ≫ X.fromOpcycles f₁ f₂ f₁₂ h₁₂ n₁ = π₂ ≫ z₁ ≫ (X.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₂).map (homMk₁ (α.app 0 ≫ β.app 0) (α.app 1 ≫ β.app 1) ⋯) =
    (X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯) ≫ (X.H n₂).map (homMk₁ (β.app 0) (β.app 1) ⋯)

Tactic:
← Functor.map_comp

Goal state after:
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
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₃'
β : mk₃ f₁' f₂' f₃' ⟶ mk₃ f₁'' f₂'' f₃''
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.H n₂).map (homMk₁ (α.app 0 ≫ β.app 0) (α.app 1 ≫ β.app 1) ⋯) =
    (X.H n₂).map (homMk₁ (α.app 0) (α.app 1) ⋯ ≫ homMk₁ (β.app 0) (β.app 1) ⋯)
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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
h : (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) ≫ (X.H n).map (twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) = 0
⊢ IsZero ((X.H n).obj (mk₁ (𝟙 i)))

Tactic:
← Functor.map_comp

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 : ι
f : i ⟶ j
hf : IsIso f
n : ℤ
e : mk₁ (𝟙 i) ≅ mk₁ f := isoMk₁ (Iso.refl ((mk₁ (𝟙 i)).obj' 0 homMk₁._proof_4)) (asIso f) ⋯
h : (X.H n).map (twoδ₂Toδ₁ (𝟙 i) (𝟙 i) (𝟙 i) ⋯ ≫ twoδ₁Toδ₀ (𝟙 i) (𝟙 i) (𝟙 i) ⋯) = 0
⊢ IsZero ((X.H n).obj (mk₁ (𝟙 i)))
Module: Mathlib.Algebra.Homology.Square

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
sq : Square C
inst✝ : HasBinaryBiproduct sq.X₂ sq.X₃
⊢ biprod.lift sq.f₁₂ (-sq.f₁₃) ≫ biprod.desc sq.f₂₄ sq.f₃₄ = 0

Tactic:
by simp [sq.fac]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
sq : Square C
inst✝ : HasBinaryBiproduct sq.X₂ sq.X₃
⊢ biprod.lift sq.f₁₂ sq.f₁₃ ≫ biprod.desc sq.f₂₄ (-sq.f₃₄) = 0

Tactic:
by simp [sq.fac]

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

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
pq : ℤ × Fin l
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq + 1
k : ℕ
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (2 + ↑k, 1 - (2 + ↑k))).Rel pq pq'
hr : 2 ≤ 2 + ↑k
⊢ (coreE₂CohomologicalFin l).i₀ (2 + ↑k + 1) pq ⋯ = (coreE₂CohomologicalFin l).i₀ (2 + ↑k) pq ⋯

Tactic:
obtain ⟨p, q, hq⟩ := pq

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
n : ℤ
k : ℕ
hr : 2 ≤ 2 + ↑k
p : ℤ
q : ℕ
hq : q < l
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) + 1
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (2 + ↑k, 1 - (2 + ↑k))).Rel (p, ⟨q, hq⟩) pq'
⊢ (coreE₂CohomologicalFin l).i₀ (2 + ↑k + 1) (p, ⟨q, hq⟩) ⋯ = (coreE₂CohomologicalFin l).i₀ (2 + ↑k) (p, ⟨q, hq⟩) ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r : ℤ
pq : ℤ × Fin l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' pq
n : ℤ
hn : n = (coreE₂CohomologicalFin l).deg pq - 1
hr : 2 ≤ r
⊢ (coreE₂CohomologicalFin l).i₃ r pq ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) pq ⋯

Tactic:
obtain ⟨p, q, hq⟩ := pq

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 ι
c : ℤ → ComplexShape κ
r₀ : ℤ
X : SpectralObject C ι
data : SpectralSequenceDataCore ι c r₀
inst✝ : X.HasSpectralSequence data
l : ℕ
E : SpectralObject C (Fin (l + 1))
r n : ℤ
hr : 2 ≤ r
p : ℤ
q : ℕ
hq : q < l
hpq : ∀ (pq' : ℤ × Fin l), ¬(ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq' (p, ⟨q, hq⟩)
hn : n = (coreE₂CohomologicalFin l).deg (p, ⟨q, hq⟩) - 1
⊢ (coreE₂CohomologicalFin l).i₃ r (p, ⟨q, hq⟩) ⋯ = (coreE₂CohomologicalFin l).i₃ (r + 1) (p, ⟨q, hq⟩) ⋯
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₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.cyclesIsoH f n₀ n₁ hn₁).inv = X.toCycles (𝟙 i₀) f f ⋯ n₀

Tactic:
rw [← cancel_mono (X.iCycles (𝟙 _) f n₀), toCycles_i]
  dsimp [cyclesIsoH]
  simp only [Category.assoc, cyclesIso_hom_i, homologyDataIdId_left_i,
    ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles, ← Functor.map_id]
  congr 1
  cat_disch

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ EventuallyConst (⇑f) atTop

Tactic:
eventuallyConst_atTop,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ i, ∀ (j : ℕ), i ≤ j → f j = f i
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
n : ℕ
⊢ ((f ^ n) ∘ₗ f).range < (f ^ n).range

Tactic:
LinearMap.range_comp,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : M →ₗ[R] M
s : Injective ⇑f
h : ¬Surjective ⇑f
n : ℕ
⊢ Submodule.map (f ^ n) f.range < (f ^ n).range
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ (b : ℕ),
    k ≤ b → IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ m, (f ^ m).range = (f ^ b).range ∧ ⨆ m, (f ^ m).ker = (f ^ b).ker
h₁ : IsCompl (f ^ k).ker (f ^ k).range
h₂ : ⨅ m, (f ^ m).range = (f ^ k).range
h₃ : ⨆ m, (f ^ m).ker = (f ^ k).ker
⊢ IsCompl (⨆ n, (f ^ n).ker) (⨅ n, (f ^ n).range)

Tactic:
rwa [h₂, h₃]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing Rᵐᵒᵖ
x✝ : R
⊢ x✝ ∈ IsUnit.submonoid R ↔ IsLeftRegular x✝

Tactic:
exact isUnit_iff_isLeftRegular

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (∃ K, K.toSubmodule = p) → ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
rintro ⟨K, rfl⟩ _ _
    exact K.lie_mem'

Goal state after: