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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅↑x_1, x⁆ ∈ H
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, z⁆ + ⁅y, 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, z⁆ + ⁅y, z⁆)
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H

Tactic:
]

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

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : ∃ y_1 ∈ R ∙ x, ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ y ∈ R ∙ x, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : ∃ y_1 ∈ R ∙ x, ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ y ∈ R ∙ x, ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ ⁅c • a, b⁆ ∈ Submodule.span R₂ S

Tactic:
]

Goal state after:
case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ I
b : L
hb : b ∈ I
⊢ ⁅c • a, b⁆ ∈ Submodule.span R₂ S
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ derivedSeriesOfIdeal R₁ L k ⊤
b : L
hb : b ∈ I
⊢ c • a ∈ derivedSeriesOfIdeal R₁ L k ⊤

Tactic:
]

Goal state after:
case smul_mem
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
inst✝⁴ : CommRing R₁
inst✝³ : CommRing R₂
inst✝² : LieRing L
inst✝¹ : LieAlgebra R₁ L
inst✝ : LieAlgebra R₂ L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R₁ L k ⊤ ↔ x ∈ derivedSeriesOfIdeal R₂ L k ⊤
I : LieIdeal R₂ L := derivedSeriesOfIdeal R₂ L k ⊤
S : Set L := {x | ∃ a ∈ I, ∃ b ∈ I, ⁅a, b⁆ = x}
x : L
c : R₁
a : L
ha : a ∈ derivedSeriesOfIdeal R₁ L k ⊤
b : L
hb : b ∈ I
⊢ c • a ∈ derivedSeriesOfIdeal R₁ L k ⊤
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
⊢ ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑↑⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ =
    ↑↑⁅derivedSeriesOfIdeal ℤ L k ⊤, derivedSeriesOfIdeal ℤ 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 : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑↑⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ =
    ↑↑⁅derivedSeriesOfIdeal ℤ L k ⊤, derivedSeriesOfIdeal ℤ L k ⊤⁆
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, Quotient.mk'' y + Quotient.mk'' z⁆ = ⁅mk x, Quotient.mk'' y⁆ + ⁅mk x, Quotient.mk'' 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, Quotient.mk'' y + Quotient.mk'' z⁆ = ⁅mk x, Quotient.mk'' y⁆ + ⁅mk x, Quotient.mk'' z⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑↑⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ =
    ↑↑⁅derivedSeriesOfIdeal ℤ L k ⊤, derivedSeriesOfIdeal ℤ L k ⊤⁆

Tactic:
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ↑↑(derivedSeriesOfIdeal R L k ⊤) = ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ ↑↑(derivedSeriesOfIdeal R L k ⊤) ↔ x ∈ ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
]

Goal state after:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ ↑↑(derivedSeriesOfIdeal R L k ⊤) ↔ x ∈ ↑↑(derivedSeriesOfIdeal ℤ L k ⊤)
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔ ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
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, mk y + Quotient.mk'' z⁆ = ⁅mk x, mk y⁆ + ⁅mk x, Quotient.mk'' 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, mk y + Quotient.mk'' z⁆ = ⁅mk x, mk y⁆ + ⁅mk x, Quotient.mk'' z⁆
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ x ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
this : x ∈ H
⊢ x ∈ H
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, mk y + mk z⁆ = ⁅mk x, mk y⁆ + ⁅mk x, mk 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, mk y + mk z⁆ = ⁅mk x, mk y⁆ + ⁅mk x, mk z⁆
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
]

Goal state after:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x : L
hx : Quot.mk (⇑(↑H.toLieSubmodule).quotientRel) x ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)
⊢ ∀ y ∈ H, ⁅y, x⁆ ∈ H
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, x⁆ ∈ H.toLieSubmodule
⊢ ⁅y, x⁆ ∈ H

Tactic:
]

Goal state after:
case refine_1.mk
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m✝ : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx : ⁅⟨y, hy⟩, x⁆ ∈ H.toLieSubmodule
⊢ ⁅y, x⁆ ∈ H
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, mk y + mk z⁆ = mk ⁅x, y⁆ + ⁅mk x, mk 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, mk y + mk z⁆ = mk ⁅x, y⁆ + ⁅mk x, mk z⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 ≠ ⊤

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : derivedSeries R L n = ⊥
⊢ derivedSeries R L 1 ≠ ⊤
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : ⊤ = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : IsSolvable L
inst✝ : Nontrivial L
n : ℕ
hn : ⊤ = ⊥
contra : derivedSeries R L 1 = ⊤
⊢ False
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, mk y + mk z⁆ = mk ⁅x, y⁆ + mk ⁅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, mk y + mk z⁆ = mk ⁅x, y⁆ + mk ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ ∃ k, derivedSeries A (A ⊗[R] L) k = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ ∃ k, derivedSeries A (A ⊗[R] L) k = ⊥
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : LieRing L'
inst✝³ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsSolvable L
k : ℕ
hk : derivedSeries R L k = ⊥
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → ∃ k, derivedSeries R L k = ⊥

Tactic:
]

Goal state after:
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
⊢ (∃ k, derivedSeries A (A ⊗[R] L) k = ⊥) → ∃ k, derivedSeries R L k = ⊥
Module: Mathlib.Algebra.Lie.Normalizer

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Tactic:
]

Goal state after:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
h : ∀ m ∈ LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule), m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : derivedSeries A (A ⊗[R] L) k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥
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, Submodule.Quotient.mk (y + z)⁆ = mk ⁅x, y⁆ + mk ⁅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, Submodule.Quotient.mk (y + z)⁆ = mk ⁅x, y⁆ + mk ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : LieSubmodule.baseChange A (derivedSeries R L k) ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
h : LieSubmodule.baseChange A (derivedSeries R L k) ≤ ⊥
x : L
hx : x ∈ derivedSeries R L k
⊢ x ∈ ⊥
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⁆ + mk ⁅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⁆ + mk ⁅x, z⁆
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : 1 ⊗ₜ[R] x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : 1 ⊗ₜ[R] x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0

Tactic:
]

Goal state after:
case h
R : Type u
L : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Module.FaithfullyFlat R A
k : ℕ
x : L
h : x = 0
hx : x ∈ derivedSeries R L k
⊢ x = 0
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⁆ + ⁅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⁆ + ⁅x, z⁆)
Module: Mathlib.Algebra.Lie.Solvable

Goal state before:
pp: 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
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∃ k, derivedSeries R L' k = ⊥

Tactic:
]

Goal state after:
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
hL : ∃ k, derivedSeries R L k = ⊥
h : Injective ⇑f
⊢ ∃ k, derivedSeries R L' k = ⊥