mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι' : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι'
X' : SpectralObject C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂

Tactic:
rw [← map_comp .., ← map_comp ..]

Goal state after:
C : Type u_1
ι' : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι'
X' : SpectralObject C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ ≫ fourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅) n₀ n₁ n₂ ⋯ ⋯ =
    X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ ≫ fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯) n₀ n₁ n₂ ⋯ ⋯
Module: Mathlib.Algebra.Homology.SpectralObject.Homology

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
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₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
⊢ x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0 →
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f

Tactic:
hx₂

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
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₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
A : C
x₂ : A ⟶ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).X₂
hx₂ : x₂ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ ⋯ ⋯ ⋯).f
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
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ IsLimit (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯)

Tactic:
refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2
        (kernelIsKernel (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂))
      · exact parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa) (by simp)
      · exact Fork.ext (Iso.refl _)

Goal state after:
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
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂
⊢ x₂ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
hx₂

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₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂
hx₂ : x₂ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
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
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂
⊢ x₂ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
hx₂

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₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
A : C
x₂ : A ⟶ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂
hx₂ : x₂ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
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.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂
⊢ x₂ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
hx₂

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.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂
hx₂ : x₂ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).f
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.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂
⊢ x₂ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = 0 →
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f

Tactic:
hx₂

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.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂
hx₂ : x₂ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
Module: Mathlib.Order.Filter.EventuallyConst

Goal state before:
pp: case refine_2
α : Type u_1
f : ℕ → α
n : ℕ
h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
m : ℕ
hm : n ≤ m
⊢ f m = f n

Tactic:
induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm

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₂
h : (c r).Rel pq' pq''
⊢ n₂ = data.deg pq''

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

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

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → OrderDual.toDual f (m + 1) = ⊤
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊤

Tactic:
apply w
      exact Nat.succ_le_succ_iff.mp p

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y z : L
m n : M
⊢ { toFun := fun m ↦ ⁅0, m⁆, map_zero' := ⋯, map_add' := ⋯ } = 0

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y z : L
m n✝ n : M
⊢ { toFun := fun m ↦ ⁅0, m⁆, map_zero' := ⋯, map_add' := ⋯ } n = 0 n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y✝ z✝ : L
m n : M
y z : L
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } =
    { toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
      { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x y✝ z✝ : L
m n✝ : M
y z : L
n : M
⊢ { toFun := fun m ↦ ⁅y + z, m⁆, map_zero' := ⋯, map_add' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅y, m⁆, map_zero' := ⋯, map_add' := ⋯ } +
        { toFun := fun m ↦ ⁅z, m⁆, map_zero' := ⋯, map_add' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n : M
x y : L
f : M →ₗ[R] N
⊢ { toFun := fun m ↦ ⁅x + y, f m⁆ - f ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n✝ : M
x y : L
f : M →ₗ[R] N
n : M
⊢ { toFun := fun m ↦ ⁅x + y, f m⁆ - f ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m n : M
x : L
f g : M →ₗ[R] N
⊢ { toFun := fun m ↦ ⁅x, (f + g) m⁆ - (f + g) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m ↦ ⁅x, g m⁆ - g ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y z : L
m n✝ : M
x : L
f g : M →ₗ[R] N
n : M
⊢ { toFun := fun m ↦ ⁅x, (f + g) m⁆ - (f + g) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m ↦ ⁅x, g m⁆ - g ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n : M
x y : L
f : M →ₗ[R] N
⊢ {
      toFun := fun m ↦
        ⁅x, { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
          { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m⁆,
      map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m ↦ ⁅⁅x, y⁆, f m⁆ - f ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
      {
        toFun := fun m ↦
          ⁅y, { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
            { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅y, m⁆,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m n✝ : M
x y : L
f : M →ₗ[R] N
n : M
⊢ {
        toFun := fun m ↦
          ⁅x, { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
            { toFun := fun m ↦ ⁅y, f m⁆ - f ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅x, m⁆,
        map_add' := ⋯, map_smul' := ⋯ }
      n =
    ({ toFun := fun m ↦ ⁅⁅x, y⁆, f m⁆ - f ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } +
        {
          toFun := fun m ↦
            ⁅y, { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } m⁆ -
              { toFun := fun m ↦ ⁅x, f m⁆ - f ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ } ⁅y, m⁆,
          map_add' := ⋯, map_smul' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
⊢ ⁅t • x, f⁆ = t • ⁅x, f⁆

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n✝ : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ ⁅t • x, f⁆ n = (t • ⁅x, f⁆) n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
⊢ ⁅x, t • f⁆ = t • ⁅x, f⁆

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m n✝ : M
t : R
x : L
f : M →ₗ[R] N
n : M
⊢ ⁅x, t • f⁆ n = (t • ⁅x, f⁆) n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m✝ n : M
x y : L
m : M →ₗ[R] R
⊢ { toFun := fun m_1 ↦ -m ⁅x + y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun m_1 ↦ -m ⁅y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t : R
x✝ y✝ z : L
m✝ n✝ : M
x y : L
m : M →ₗ[R] R
n : M
⊢ { toFun := fun m_1 ↦ -m ⁅x + y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } n =
    ({ toFun := fun m_1 ↦ -m ⁅x, m_1⁆, map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun m_1 ↦ -m ⁅y, m_1⁆, map_add' := ⋯, map_smul' := ⋯ })
      n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x : L
m : M →ₗ[R] R
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅t • x, m⁆ n = (t • ⁅x, m⁆) n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x : L
m : M →ₗ[R] R
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
ext n

Goal state after:
R : Type u
L : Type v
M : Type w
N : 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✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n✝ : M
t : R
x : L
m : M →ₗ[R] R
n : M
⊢ ⁅x, t • m⁆ n = (t • ⁅x, m⁆) n
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
M : Type w₁
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M
inst✝² : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst✝¹ : Module R M
inst✝ : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, smul_lie, map_smul]

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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ x✝ : L₁
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
rw [← coe_toLinearEquiv, map_add]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ x✝ : M
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
rw [← coe_toLinearEquiv, map_add]

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'
⊢ n₀ = data.deg pq

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

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
⊢ IsNilpotent (Ring.jacobson R)

Tactic:
have ⟨n, hn⟩ := IsArtinian.monotone_stabilizes ⟨(Jac ^ ·), @Ideal.pow_le_pow_right _ _ _⟩

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ IsNilpotent (Ring.jacobson R)
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
x y : L
z : M
n : ℕ
⊢ (φ x ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L) x ^ ij.1) y, (φ x ^ ij.2) z⁆

Tactic:
induction n with

Goal state after: