mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ { f := (CategoryTheory.shiftFunctor C n).map (𝟙 X).f, comm := ⋯ } =
    𝟙
      { obj := (CategoryTheory.shiftFunctor C n).obj X.obj,
        d := (CategoryTheory.shiftFunctor C n).map X.d ≫ (shiftComm X.obj 1 n).hom, d_squared := ⋯ }

Tactic:
by ext1; dsimp; rw [Functor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
⊢ (ObjectProperty.ofObj (separatingFamily c X)).IsSeparating

Tactic:
by
  intro K L f g h
  ext j
  apply hX
  rintro _ ⟨a⟩ p
  have H := evalCompCoyonedaCorepresentable c (X a) j
  apply H.homEquiv.symm.injective
  simpa only [H.homEquiv_symm_comp] using! h _
    (ObjectProperty.ofObj_apply _ ⟨a, j⟩) (H.homEquiv.symm p)

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

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

Tactic:
← hβ

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
β : (projectiveResolution X).complex ⟶ P.complex
hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) =
    (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
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
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.fromLeftDerivedZero.app X =
    (P.isoLeftDerivedObj F 0).hom ≫
      (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom ≫
        P.fromLeftDerivedZero' F

Tactic:
dsimp [Functor.fromLeftDerivedZero, isoLeftDerivedObj]
  have h₁ := ProjectiveResolution.fromLeftDerivedZero'_naturality
    (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F
  have h₂ : (P.isoLeftDerivedToHomotopyCategoryObj F).inv =
    (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (lift (𝟙 X) _ _) :=
      id_comp _
  simp only [Functor.map_id, comp_id] at h₁
  rw [assoc, ← cancel_epi ((HomotopyCategory.homologyFunctor _ _ 0).map
      (P.isoLeftDerivedToHomotopyCategoryObj F).inv), ← Functor.map_comp_assoc,
      Iso.inv_hom_id, Functor.map_id, id_comp, ← h₁, h₂,
      ← HomologicalComplex.homologyι_naturality_assoc]
  erw [← NatTrans.naturality_assoc]
  rfl

Goal state after:
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 j : I
⊢ K.rightUnitor'.inv i ≫ (K.tensorObj (tensorUnit C c)).d i j = K.d i j ≫ K.rightUnitor'.inv j

Tactic:
by_cases hij : c.Rel i j
  · simp only [rightUnitor'_inv, assoc, mapBifunctor.d_eq,
      Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
      tensor_unit_d₂, comp_zero, add_zero]
    rw [mapBifunctor.d₁_eq _ _ _ _ hij _ _ (by simp)]
    dsimp
    simp only [one_smul, whisker_exchange_assoc, whiskerRight_id, assoc, Iso.inv_hom_id_assoc]
  · simp only [shape _ _ _ hij, comp_zero, zero_comp]

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.toCycles f₃ f₄ f₃₄ h₃₄ n₁ ≫
      X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ ≫ 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:
X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,

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.π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.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.H n₁).map (twoδ₂Toδ₁ f₁ f₂ f₁₂ h₁₂) =
    (X.H n₀).map (twoδ₁Toδ₀ f₂ f₃ (f₂ ≫ f₃) ⋯) ≫ X.δ f₁₂ f₃ n₀ n₁ hn₁

Tactic:
exact (X.δ_naturality _ _ _ _ _ _ _ _ rfl).symm

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

Tactic:
X.toCycles_πE_d_assoc f₁ f₂ f₃ f₄ f₅ _ rfl _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,

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₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ 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₃ ≫ X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    X.δ f₂ (f₃ ≫ f₄) n₁ n₂ ⋯ ≫ X.pOpcycles f₂ f₃ n₂
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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43
⊢ WithBotTop.coe (hr.2 - r' + 2) = WithBotTop.coe (hr.2 + (1 - r))

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_41
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_43
⊢ WithBotTop.coe (hr.2 - r' + 2) = WithBotTop.coe (hr.2 + (1 - r))
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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_47
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ WithBotTop.coe (hr.2 + (1 - r) + r' - 1) = WithBotTop.coe (hr.2 + 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
hr : ℤ × ℤ
hrr'✝ : autoParam (r + 1 = r') SpectralSequenceDataCore._auto_47
hr✝ : autoParam (2 ≤ r) SpectralSequenceDataCore._auto_49
⊢ WithBotTop.coe (hr.2 + (1 - r) + r' - 1) = WithBotTop.coe (hr.2 + 1)
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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq.2 - r + 2) = WithBotTop.coe (↑pq'.2 + 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq.2 - r + 2) = WithBotTop.coe (↑pq'.2 + 1)
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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe ↑pq.2 = WithBotTop.coe (↑pq'.2 + r - 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe ↑pq.2 = WithBotTop.coe (↑pq'.2 + r - 1)
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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq.2 - r' + 2) = WithBotTop.coe ↑pq'.2

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq.2 - r' + 2) = WithBotTop.coe ↑pq'.2
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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq'.2 + r' - 1) = WithBotTop.coe (↑pq.2 + 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + r = ↑pq'.1 ∧ ↑pq.2 + (1 - r) = ↑pq'.2
⊢ WithBotTop.coe (↑pq'.2 + r' - 1) = WithBotTop.coe (↑pq.2 + 1)
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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2 - r + 2) = WithBotTop.coe (-↑pq'.2 + 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2 - r + 2) = WithBotTop.coe (-↑pq'.2 + 1)
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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2) = WithBotTop.coe (-↑pq'.2 + r - 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r : ℤ
pq pq' : ℕ × ℕ
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2) = WithBotTop.coe (-↑pq'.2 + r - 1)
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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2 - r' + 2) = WithBotTop.coe (-↑pq'.2)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq.2 - r' + 2) = WithBotTop.coe (-↑pq'.2)
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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq'.2 + r' - 1) = WithBotTop.coe (-↑pq.2 + 1)

Tactic:
#adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/

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₀ r r' : ℤ
pq pq' : ℕ × ℕ
hrr' : r + 1 = r'
hr : 2 ≤ r
hpq : ↑pq.1 + -r = ↑pq'.1 ∧ ↑pq.2 + (r - 1) = ↑pq'.2
⊢ WithBotTop.coe (-↑pq'.2 + r' - 1) = WithBotTop.coe (-↑pq.2 + 1)
Module: Mathlib.RingTheory.Jacobson.Semiprimary

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
r : R
hr : r ∈ Ring.jacobson R
m : M
this : r ∈ Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)
⊢ r • m = 0

Tactic:
jacobson_eq_bot

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
r : R
hr : r ∈ Ring.jacobson R
m : M
this : r ∈ Submodule.comap (LinearMap.toSpanSingleton R M m) ⊥
⊢ r • m = 0
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: case pos
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₂
h : (c r).Rel pq' pq''
⊢ (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

pp: case neg
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₂
h : ¬(c r).Rel pq' pq''
⊢ (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:
· 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]

Goal state after:
case neg
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₂
h : ¬(c r).Rel pq' pq''
⊢ (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
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' pq'' : κ
i₀' 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' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Fork.ι (kf X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯) ≫
      Cofork.π (cc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯) =
    X.mapFourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯ ≫ X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯

Tactic:
simp [← map_comp]
  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₀
Y : SpectralObject C EInt
inst✝ : Y.IsThirdQuadrant
r : ℤ
hr : 2 ≤ r
p q : ℤ
hq : 0 < q
⊢ IsZero ((Y.E₂SpectralSequence.page r ⋯).X (p, q))

Tactic:
by
  apply isZero_spectralSequence_page_X_of_isZero_H' _ _ _ hr
  apply Y.isZero₁_of_isThirdQuadrant
  simp
  lia

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

Goal state before:
pp: 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
inst✝ : IsFaithful R L M
L' : LieSubalgebra R L
⊢ IsFaithful R (↥L') M

Tactic:
by
  refine ⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩
  exact IsFaithful.injective_toEnd.comp Subtype.val_injective

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieRing L'
inst✝⁹ : LieAlgebra R L'
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : LieRingModule L M'
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M
inst✝ : LieModule R L M'
f : L →ₗ⁅R⁆ L'
I I₂ : LieIdeal R L
J : LieIdeal R L'
x y : L
h : y ∈ (Submodule.comap (↑f) (toLieSubalgebra R L' J).toSubmodule).carrier
⊢ ⁅f x, f y⁆ ∈ J

Tactic:
apply J.lie_mem h

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

Goal state before:
pp: case add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
⊢ ⟨u, hx✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
    ⟨v, hy✝⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) →
      ⟨u + v, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
exact add_mem

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

Goal state before:
pp: case a.add
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x u v : L
hx✝ : u ∈ lieSpan R L (range (Subtype.val ∘ f))
hy✝ : v ∈ lieSpan R L (range (Subtype.val ∘ f))
⊢ u ∈ map K.incl (lieSpan R (↥K) (range f)) →
    v ∈ map K.incl (lieSpan R (↥K) (range f)) → u + v ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact add_mem

Goal state after: