mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = mk ⁅⁅x, y⁆, z⁆ + mk ⁅y, ⁅x, z⁆⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = mk ⁅⁅x, y⁆, z⁆ + mk ⁅y, ⁅x, z⁆⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case refine_2
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
z : M
hz : z ∈ (fun a ↦ ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
⊢ z ∈ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
rcases hz with (⟨m, hm, rfl⟩ | ⟨y, -, m, hm, rfl⟩)
    exacts [⟨x, m, hm, rfl⟩, ⟨y, m, hm, rfl⟩]

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

Goal state before:
pp: case inl
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✝ : IsArtinian R M
h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m
l : ℕ
hl : n ≤ l
m : ℕ
h : l ≤ m
⊢ lowerCentralSeries R L M n ≤ lowerCentralSeries R L M n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.baseChange A ↑N
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.baseChange A ↑N
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case mpr
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
h : ∀ m ∈ lowerCentralSeries R L M 1, m = 0
⊢ IsTrivial L M

Tactic:
]

Goal state after:
case mpr
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
h : ∀ m ∈ lowerCentralSeries R L M 1, m = 0
⊢ IsTrivial L M
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • Quotient.mk'' y⁆ = t • ⁅mk x, Quotient.mk'' y⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • Quotient.mk'' y⁆ = t • ⁅mk x, Quotient.mk'' y⁆
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • ⁅mk x, mk y⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • ⁅mk x, mk y⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
x✝¹ : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
val✝ : A ⊗[R] M
n : M
hn : n ∈ ↑↑N
h : ((TensorProduct.mk R A M) 1) n = val✝
x✝ : ⟨val✝, ⋯⟩ ∈ c.support
⊢ ⁅a ⊗ₜ[R] y, ((TensorProduct.mk R A M) 1) n⁆ ∈ Submodule.baseChange A ↑N

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a : A
y : L
x✝¹ : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
val✝ : A ⊗[R] M
n : M
hn : n ∈ ↑↑N
h : ((TensorProduct.mk R A M) 1) n = val✝
x✝ : ⟨val✝, ⋯⟩ ∈ c.support
⊢ ⁅a ⊗ₜ[R] y, ((TensorProduct.mk R A M) 1) n⁆ ∈ Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • mk ⁅x, y⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, t • mk y⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
y z : A ⊗[R] L
hy : ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
hz : ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
⊢ ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ + ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈
    Submodule.baseChange A ↑N

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
x : A ⊗[R] L
c : ↑↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N) →₀ A
hm : (Finsupp.linearCombination A Subtype.val) c ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
y z : A ⊗[R] L
hy : ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
hz : ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈ Submodule.baseChange A ↑N
⊢ ⁅y, (Finsupp.linearCombination A Subtype.val) c⁆ + ⁅z, (Finsupp.linearCombination A Subtype.val) c⁆ ∈
    Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
m : A ⊗[R] M
⊢ m ∈ baseChange A N ↔ m ∈ Submodule.baseChange A ↑N

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
N : LieSubmodule R L M
m : A ⊗[R] M
⊢ m ∈ baseChange A N ↔ m ∈ Submodule.baseChange A ↑N
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: case succ.refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ Submodule.map ((toEnd R L M) x) ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
]

Goal state after:
case succ.refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ Submodule.map ((toEnd R L M) x) ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, Submodule.Quotient.mk (t • y)⁆ = t • mk ⁅x, y⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ ⁅mk x, Submodule.Quotient.mk (t • y)⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
⊢ baseChange A ⊥ = ⊥

Tactic:
by
  simp only [baseChange, bot_toSubmodule, Submodule.baseChange_bot]
  rfl

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

Goal state before:
pp: case succ.refine_1
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
n i j : ℕ
hxn : (toEnd R L M) x ^ n = 0
hIM : lowerCentralSeries R L M i ≤ I.lcs M j
l : ℕ
ih : ↑(⊤.lcs M (i + l)) ≤ Submodule.map ((toEnd R L M) x ^ l) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))
⊢ Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1)) ≤
    Submodule.map ((toEnd R L M) x ^ (l + 1)) ↑(I.lcs M j) ⊔ ↑(I.lcs M (j + 1))

Tactic:
]

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

Goal state before:
pp: case zero
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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f

Tactic:
]

Goal state after:
case zero
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
k : ℕ
M₂ : Type w₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L M₂
inst✝¹ : LieModule R L M₂
inst✝ : LieModule R L M
f : M →ₗ⁅R,L⁆ M₂
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑f
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = t • mk ⁅x, y⁆

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = t • mk ⁅x, y⁆
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
⊢ Submodule.span A s = Submodule.span A {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}

Tactic:
]

Goal state after:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
⊢ Submodule.span A s = Submodule.span A {x | ∃ x_1 ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x_1, n⁆ = x}
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ⊤ ≤ ⊤

Tactic:
]

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

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = Submodule.Quotient.mk (t • ⁅x, y⁆)

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ mk ⁅x, t • y⁆ = Submodule.Quotient.mk (t • ⁅x, y⁆)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆
Module: Mathlib.Algebra.Lie.Nilpotent

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✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k ≤ lowerCentralSeries R L M k

Tactic:
]

Goal state after:
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✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k ≤ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.Nilpotent

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
N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L (↥N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥

Tactic:
]

Goal state after:
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
N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L (↥N) k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N N' : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ N' ≤ N ↔ N' ≤ N

Tactic:
]

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

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
N : LieSubmodule R L M
k : ℕ
⊢ LieSubmodule.lcs k N = ⊥ ↔ LieSubmodule.lcs k N = ⊥

Tactic:
]

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

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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✝¹ : CommRing A
inst✝ : Algebra R A
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s
x : A ⊗[R] L
hx : x ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
m : A ⊗[R] M
hm : m ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
⊢ ⁅x, m⁆ ∈ ↑(Submodule.span A s)
Module: Mathlib.Algebra.Lie.Engel

Goal state before:
pp: R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
]

Goal state after:
R : Type u₁
L : Type u₂
M : Type u₄
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
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
hIM : LieModule.IsNilpotent (↥I) M
n : ℕ
hn : (toEnd R L M) x ^ n = 0
k : ℕ
hk : lowerCentralSeries R (↥I) M k = ⊥
hk' : I.lcs M k = ⊥
this : ∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
⊢ ∃ k, lowerCentralSeries R L M k = ⊥
Module: Mathlib.Algebra.Lie.Quotient

Goal state before:
pp: case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ⁅↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹)), ↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝))⁆

Tactic:
]

Goal state after:
case H.H
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z✝¹ z✝ : L
⊢ ↑((↑f).quotKerEquivRange ⁅Submodule.Quotient.mk z✝¹, Submodule.Quotient.mk z✝⁆) =
    ⁅↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝¹)), ↑((↑f).quotKerEquivRange (Submodule.Quotient.mk z✝))⁆
Module: Mathlib.Algebra.Polynomial.GroupRingAction

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
S : Type u_3
inst✝¹ : CommSemiring S
inst✝ : MulSemiringAction M S
m : M
f : S[X]
x r : S
⊢ m • r = m • r

Tactic:
]

Goal state after: