mathlib-initiative/mathlib-tactics huggingface dataset:
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.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:
← Submodule.Quotient.mk_smul (R := R) (M := L)

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
I : LieIdeal R L
N : LieSubmodule R L M
s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}
x✝ : A ⊗[R] M
⊢ x✝ ∈ ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} ↔ x✝ ∈ s

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}
x✝ : A ⊗[R] M
⊢ x✝ ∈ ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} ↔ x✝ ∈ s
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:
← Submodule.Quotient.mk_smul (R := R) (M := L)

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.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:
← Submodule.Quotient.mk_smul (R := R) (M := L)

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.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
⊢ ⁅x, t • y⁆ = 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
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
m✝ : M
⊢ m✝ ∈ (mk' N).ker ↔ m✝ ∈ N

Tactic:
;

Goal state after:
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 : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
m✝ : M
⊢ m✝ ∈ (mk' N).ker ↔ m✝ ∈ N
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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 : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
inst✝² : LieModule R L M₂
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
⊢ lowerCentralSeries ℤ L M 1 = ⊥

Tactic:
;

Goal state after:
case h
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 : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
inst✝² : LieModule R L M₂
inst✝¹ : LieModule R L M
inst✝ : IsTrivial L M
⊢ lowerCentralSeries ℤ L M 1 = ⊥
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.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
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 : L
hx : x ∈ ↑↑I
y : M
hy : y ∈ ↑↑N
⊢ ⁅((TensorProduct.mk R A L) 1) x, ((TensorProduct.mk R A M) 1) y⁆ ∈ Submodule.span A s

Tactic:
;

Goal state after:
case refine_2.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
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 : L
hx : x ∈ ↑↑I
y : M
hy : y ∈ ↑↑N
⊢ ⁅((TensorProduct.mk R A L) 1) x, ((TensorProduct.mk R A M) 1) y⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
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 : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
⊢ (toEnd R L M) x ^ k = 0

Tactic:
;

Goal state after:
case h
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 : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
⊢ (toEnd R L M) x ^ k = 0
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
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * 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
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) ≤ lowerCentralSeries R L M k
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.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✝ y✝ : A ⊗[R] L
z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
a✝ : ⁅y✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝ + y✝, z✝⁆ ∈ Submodule.span A s

Tactic:
;

Goal state after:
case refine_2.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✝ y✝ : A ⊗[R] L
z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
a✝ : ⁅y✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝ + y✝, z✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_3
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✝ : A ⊗[R] L
y✝ z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
a✝ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, y✝ + z✝⁆ ∈ Submodule.span A s

Tactic:
;

Goal state after:
case refine_2.refine_3
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✝ : A ⊗[R] L
y✝ z✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
hz✝ : z✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝¹ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
a✝ : ⁅x✝, z✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, y✝ + z✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_4
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)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅r✝ • x✝, y✝⁆ ∈ Submodule.span A s

Tactic:
;

Goal state after:
case refine_2.refine_4
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)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅r✝ • x✝, y✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.BaseChange

Goal state before:
pp: case refine_2.refine_5
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)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, r✝ • y✝⁆ ∈ Submodule.span A s

Tactic:
;

Goal state after:
case refine_2.refine_5
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)
r✝ : A
x✝ : A ⊗[R] L
y✝ : A ⊗[R] M
hx✝ : x✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A L) 1) ↑I)
hy✝ : y✝ ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) ↑N)
a✝ : ⁅x✝, y✝⁆ ∈ Submodule.span A s
⊢ ⁅x✝, r✝ • y✝⁆ ∈ Submodule.span A s
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M

Tactic:
;

Goal state after:
case inl
L : Type v
M : Type w
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : LieRingModule L M
inst✝ : IsNilpotent L M
h✝ : nilpotencyLength L M ≤ 1
a✝ : Nontrivial M
h : Subsingleton M
⊢ IsTrivial L M
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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M 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
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
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
⊢ (∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs 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
⊢ (∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs k ⊥ = ⊤
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
inst✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

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
inst✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
L : Type v
inst✝ : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LieModule.lowerCentralSeries ℤ L L k = ⊥
⊢ derivedSeries ℤ L k = ⊥

Tactic:
;

Goal state after:
case h
L : Type v
inst✝ : LieRing L
hL : LieModule.IsNilpotent L L
k : ℕ
h : LieModule.lowerCentralSeries ℤ L L k = ⊥
⊢ derivedSeries ℤ L k = ⊥
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
h' : map f ⊤ = ⊤
⊢ map f ⊤ = ⊤

Tactic:
;

Goal state after:
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ⇑f
h' : map f ⊤ = ⊤
⊢ map f ⊤ = ⊤
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
x✝ : F
⊢ x✝ ∈ fixedPoints M F ↔ x✝ ∈ ↑(⨅ m, FixedBy.subfield F m)

Tactic:
;

Goal state after:
M : Type u
inst✝⁷ : Monoid M
G : Type u
inst✝⁶ : Group G
K : Type u_1
F : Type v
inst✝⁵ : Field F
inst✝⁴ : MulSemiringAction M F
inst✝³ : MulSemiringAction G F
m : M
inst✝² : Field K
inst✝¹ : Algebra K F
inst✝ : SMulCommClass M K F
x✝ : F
⊢ x✝ ∈ fixedPoints M F ↔ x✝ ∈ ↑(⨅ m, FixedBy.subfield F m)
Module: Mathlib.Algebra.Lie.Nilpotent

Goal state before:
pp: case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥

Tactic:
;

Goal state after:
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : ∃ k, lowerCentralSeries R L' L' k = ⊥
f : L →ₗ⁅R⁆ L'
h₂ : Injective ⇑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
Module: Mathlib.FieldTheory.Fixed

Goal state before:
pp: G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
⊢ LinearIndepOn F ⇑(toFun G F) ↑s ∧ (toFun G F) a ∉ Submodule.span F (⇑(toFun G F) '' ↑s)

Tactic:
;

Goal state after:
G : Type u
inst✝² : Group G
F : Type v
inst✝¹ : Field F
inst✝ : MulSemiringAction G F
s✝ : Finset F
this : IsEmpty ↑↑∅
a : F
s : Finset F
has : a ∉ s
ih : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(toFun G F) ↑s
hs : LinearIndepOn (↥(subfield G F)) id ↑s ∧ id a ∉ Submodule.span (↥(subfield G F)) (id '' ↑s)
⊢ LinearIndepOn F ⇑(toFun G F) ↑s ∧ (toFun G F) a ∉ Submodule.span F (⇑(toFun G F) '' ↑s)
Module: Mathlib.FieldTheory.Normal.Defs

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ (map (algebraMap F E') (minpoly F x)).Splits

Tactic:
;

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
inst✝³ : Field E
inst✝² : Algebra F E
E' : Type u_4
inst✝¹ : Field E'
inst✝ : Algebra F E'
h : ∀ (x : E), IsIntegral F x ∧ (map (algebraMap F E) (minpoly F x)).Splits
f : E ≃ₐ[F] E'
x : E'
⊢ IsIntegral F x ∧ (map (algebraMap F E') (minpoly F x)).Splits