mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
h :
  g₁ ≫
      (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.f +
          { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.g ≫ σ₂.s) ≫
        σ₁.s =
    g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.X₂ ≫ σ₁.s
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X

Tactic:
simp only [add_comp, assoc, comp_add, id_comp] at h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
h : g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0

Tactic:
refine ⟨fun _ Y f _ ↦ t.zero f n₀ n₁ (by lia), fun hX ↦ ?_⟩
  rw [t.isGE_iff_isZero_truncLT_obj n₁ X, IsZero.iff_id_eq_zero]
  exact t.to_truncLT_obj_ext (by simpa using hX _ _ (by rw [← h]; infer_instance))

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
⊢ IsIso (α.app X₂)

Tactic:
have := Φ.essSurj_of_hasLeftResolutions L₂
      rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]
      apply hα

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr.zero
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hk : q₁ + 0 = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
obtain rfl : q₁ = q₂ := by simpa using hk
      simp only [homOfLE_refl, op_id, CategoryTheory.Functor.map_id,
        ObjectProperty.FullSubcategory.id_hom, Factorisation.id_h, id_f]
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
⊢ IsConnected (CostructuredArrowDownwards e.hom g)

Tactic:
let Z (s : S) : CostructuredArrowDownwards e.hom g :=
    CostructuredArrowDownwards.mk _ _ X₀ e₀.inv s.val (by simp [s.property])

Goal state after:
C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H
B : C ⥤ H
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
⊢ IsConnected (CostructuredArrowDownwards e.hom g)
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_3
D : Type u_1
H : Type u_2
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : Category.{v_3, u_1} D
inst✝² : Category.{v_5, u_2} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
⊢ G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
rw [isRightDerivedFunctor_iff_isLeftKanExtension]
  have := IsRightDerivedFunctor.isLeftKanExtension _ α W
  exact isLeftKanExtension_iff_isIso _ α _ (by simp)

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this✝² : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
this✝¹ : L.IsGE n
this✝ : QuasiIso (L.πTruncGE n)
this : Injective (opcycles L n)
⊢ ∃ L i, ∃ (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n

Tactic:
refine ⟨L.truncGE n, i ≫ L.πTruncGE n, inferInstance, fun q ↦ ?_, inferInstance⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this✝² : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
this✝¹ : L.IsGE n
this✝ : QuasiIso (L.πTruncGE n)
this : Injective (opcycles L n)
q : ℤ
⊢ Injective ((L.truncGE n).X q)
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_1
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (CochainComplex.Plus.quasiIso C).IsInvertedBy (quotient C ⋙ L)

pp: case refine_2
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) ≤ CochainComplex.Plus.quasiIso C

pp: case refine_3
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ quasiIso C ≤ (CochainComplex.Plus.quasiIso C).map (quotient C)

Tactic:
· intro _ _ f hf
    refine Localization.inverts L (quasiIso C) _ ?_
    simpa [quasiIso, quotient_map_mem_quasiIso_iff]

Goal state after:
case refine_2
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) ≤ CochainComplex.Plus.quasiIso C

case refine_3
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
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ quasiIso C ≤ (CochainComplex.Plus.quasiIso C).map (quotient C)
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₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)

Tactic:
rw [if_neg h₀, if_neg h₁]

Goal state after:
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₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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

Tactic:
obtain rfl : m = .ofNat (n + 1) := by simp [← hnm]

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
p : ℤ
n : ℕ
hmp : Int.ofNat (n + 1) + 1 = p
hnm : Int.ofNat n + 1 = Int.ofNat (n + 1)
⊢ h.d (Int.ofNat n) (Int.ofNat (n + 1)) ≫ h.d (Int.ofNat (n + 1)) p = 0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (shiftFunctorAdd C n 0).hom.app X = eqToHom ⋯ ≫ (shiftZero C).inv.app ((shiftFunctor C n).obj X)

Tactic:
by
        ext1
        convert! shiftFunctorAdd_add_zero_hom_app n X.obj
        simp

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₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
        g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.Exact ∧
    Epi ((((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0)

Tactic:
refine (ShortComplex.exact_and_epi_g_iff_of_iso ?_).2
          ⟨exact_d_f (Projective.π Z), by dsimp; infer_instance⟩

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
      g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ } ≅
    { X₁ := syzygies (Projective.π Z), X₂ := over Z, X₃ := Z, f := d (Projective.π Z), g := Projective.π Z, zero := ⋯ }
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ (GradedObject.Monoidal.rightUnitor K.X).inv i ≫ GradedObject.Monoidal.tensorHom (𝟙 K.X) (tensorUnitIso C c).hom i =
    (ρ_ (K.X i)).inv ≫ K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯

Tactic:
rw [GradedObject.Monoidal.rightUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
    GradedObject.Monoidal.ι_tensorHom]

Goal state after:
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i : I
⊢ K.X i ◁ GradedObject.Monoidal.tensorUnit₀.inv ≫
      (𝟙 K.X i ⊗ₘ (tensorUnitIso C c).hom 0) ≫ GradedObject.Monoidal.ιTensorObj K.X (tensorUnit C c).X i 0 i ⋯ =
    K.X i ◁ (singleObjXSelf c 0 (𝟙_ C)).inv ≫ K.ιTensorObj (tensorUnit C c) i 0 i ⋯
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ leftHomologyMap' (a • φ) h₁ h₂ = a • leftHomologyMap' φ h₁ h₂

Tactic:
by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [(γ.smul a).leftHomologyMap'_eq, LeftHomologyMapData.smul_φH, γ.leftHomologyMap'_eq]

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₀ : ℤ
l : ℕ
⊢ ∀ (r r' : ℤ) (pq pq' : ℤ × Fin l),
    (ComplexShape.spectralSequenceFin l (r, 1 - r)).Rel pq pq' →
      ∀ (hrr' : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41)
        (hr : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43), ⟨(↑↑pq.2 - (r' - 2)).toNat, ⋯⟩ = pq'.2.castSucc

Tactic:
rintro r r' ⟨a, ⟨a', _⟩⟩ ⟨b, ⟨b', _⟩⟩ ⟨h₁, h₂⟩ hrr' hr
    ext
    dsimp
    lia

Goal state after:
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: α : Type u_1
f : ℕ → α
⊢ EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m

Tactic:
eventuallyConst_atTop

Goal state after:
α : Type u_1
f : ℕ → α
⊢ (∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
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'' : κ
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'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃ ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ hn₁ hn₂ ≫
        (pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).inv) ≫
      (page X data r hr).d pq' pq'' =
    0

Tactic:
by_cases h : (c r).Rel pq' pq''
  · dsimp
    rw [pageD_eq X data r hr pq' pq'' h
      (homOfLE (by simpa only [hi₀', data.i₀_prev r r' _ _ h] using data.le₀₁ r pq''))
      (homOfLE (data.i₀_le' hrr' hr pq' hi₀' hi₀)) (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
      (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃)) rfl
      (by rw [hi₀', data.i₀_prev r r' pq' pq'' h]) hi₀ hi₁ hi₂ hi₃ _ _ _ _ hn₁' hn₁ hn₂ rfl,
      Category.assoc, Iso.inv_hom_id_assoc, map_fourδ₁Toδ₀_d_assoc .., zero_comp]
  · rw [HomologicalComplex.shape _ _ _ h, comp_zero]

Goal state after:
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₂
⊢ (kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).Exact

Tactic:
by
  by_cases h : (c r).Rel pq' pq''
  · refine ShortComplex.exact_of_iso (Iso.symm ?_)
      (X.dKernelSequence_exact
        (homOfLE (show data.i₀ r pq'' ≤ i₀' by
          simpa only [hi₀', data.i₀_prev r r' _ _ h] using data.le₀₁ r pq''))
        (homOfLE (data.i₀_le' hrr' hr pq' hi₀' hi₀)) (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
        (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃)) _ rfl
        n₀ n₁ n₂ (n₂ + 1) hn₁ hn₂ rfl)
    refine ShortComplex.isoMk (Iso.refl _)
      (pageXIso X data _ hr _ _ _ _ _ hi₀ hi₁ hi₂ hi₃ _ _ _ hn₁')
      (pageXIso X data _ hr _ _ _ _ _ rfl (by rw [hi₀', data.i₀_prev r r' _ _ h])
      (by rw [hi₀, data.hc₀₂ r _ _ h]) (by rw [hi₁, data.hc₁₃ r _ _ h]) _ _ _
      (by have := data.hc r _ _ h; lia)) ?_ ?_
    · simp
    · dsimp
      rw [pageD_eq X data r hr pq' pq'' h
        (homOfLE (data.le₀₁' r hr pq'' rfl (by simpa [← data.i₀_prev r r' _ _ h])))
        (homOfLE (data.i₀_le' hrr' hr pq' hi₀' hi₀)) (homOfLE (data.le₀₁' r hr pq' hi₀ hi₁))
        (homOfLE (data.le₁₂' pq' hi₁ hi₂)) (homOfLE (data.le₂₃' r hr pq' hi₂ hi₃))
        rfl (by rw [hi₀', data.i₀_prev r r' _ _ h]) hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ (n₂ + 1) hn₁',
        Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
  · rw [ShortComplex.exact_iff_epi _ ((page X data r hr).shape _ _ h)]
    have := isIso_mapFourδ₁Toδ₀' X data r r' hrr' hr pq' pq'' hpq'
      i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' h
    dsimp
    infer_instance

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
⊢ r • x ∈ N

Tactic:
apply N.smul_mem _ hx

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
S : Type u_5
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsArtinian R M
inst✝ : IsScalarTower S R M
H : Function.Surjective ⇑(algebraMap S R)
⊢ IsArtinian S M

Tactic:
by
  apply (OrderEmbedding.wellFoundedLT (β := Submodule R M))
  refine ⟨⟨?_, ?_⟩, ?_⟩
  · intro N
    refine { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ?_ }
    intro c x hx
    obtain ⟨r, rfl⟩ := H c
    suffices r • x ∈ N by simpa [Algebra.algebraMap_eq_smul_one, smul_assoc]
    apply N.smul_mem _ hx
  · intro N1 N2 h
    rwa [Submodule.ext_iff] at h ⊢
  · intro N1 N2
    rfl

Goal state after:
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' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ data.i₃ r' pq' ⋯ = data.i₂ pq

Tactic:
data.i₃_next r 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' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ data.i₂ pq = data.i₂ pq
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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r 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'
⊢ i₃' ≤ data.i₃ r pq ⋯

Tactic:
by
        simpa only [hi₃', data.i₃_next r r' _ _ h] using data.le₂₃ r pq

Goal state after:
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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r 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'
⊢ data.i₃ r' pq' ⋯ = data.i₂ pq

Tactic:
data.i₃_next r 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).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r 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'
⊢ data.i₂ pq = data.i₂ pq
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsRightRegular x

Tactic:
IsRightRegular,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : IsArtinianRing R
x : R
⊢ IsUnit x ↔ Injective fun x_1 ↦ x_1 * x
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h : IsFaithful R L M
x : L
hx : (toEnd R L M) x = 0
⊢ x = 0

Tactic:
simpa using hx

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

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ (Submodule.toAddSubmonoid 0).carrier
_hy : y ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅x, y⁆ ∈ (Submodule.toAddSubmonoid 0).carrier

Tactic:
(Submodule.mem_bot R).1 hx,

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
hx : x ∈ (Submodule.toAddSubmonoid 0).carrier
_hy : y ∈ (Submodule.toAddSubmonoid 0).carrier
⊢ ⁅0, y⁆ ∈ (Submodule.toAddSubmonoid 0).carrier
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Semigroup A
a b : A
⊢ a * a * (a * b) = a * (a * a * b)

Tactic:
rw [mul_assoc, mul_assoc]

Goal state after: