awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
rw : ∃ (k : ℕ), Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k) ⊥
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)

Tactic:
rw [isNilpotent_iff A]

Premises used: LieModule.isNilpotent_iff
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k) ⊥

Tactic:
simp [hk]
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : CommRing A
inst_8 : Algebra R A
inst_9 : IsNilpotent L M
k : ℕ
hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥
⊢ ∃ (k : ℕ), Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k) ⊥

Tactic:
exact ⟨k, by simp [hk]⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
⊢ LieModule.IsNilpotent L ↥(maxNilpotentIdeal R L)

Tactic:
instMaxNilpotentSubmoduleIsNilpotent R L L

Premises used: LieAlgebra.maxNilpotentIdeal, Set.Mem, LieModule.instMaxNilpotentSubmoduleIsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : IsNoetherian R L
I : LieIdeal R L
⊢ LieModule.IsNilpotent L ↥I ↔ I ≤ maxNilpotentIdeal R L

Tactic:
isNilpotent_iff_le_maxNilpotentSubmodule R L L I

Premises used: Set.Mem, LieModule.isNilpotent_iff_le_maxNilpotentSubmodule
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LE.le (α := LieIdeal R L) (center R L) (maxNilpotentIdeal R L)

Tactic:
le_sSup (trivialIsNilpotent L (center R L))

Premises used: Set.Mem, Membership.mem, Subtype, le_sSup, LieAlgebra.center, LieModule.trivialIsNilpotent
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ LE.le (α := LieSubmodule R L L) (maxNilpotentIdeal R L) (radical R L)

Tactic:
sSup_le_sSup fun I (_ : IsNilpotent L I) ↦ isSolvable_of_isNilpotent I

Premises used: Set.Mem, Membership.mem, Subtype, LieAlgebra.isSolvable_of_isNilpotent, sSup_le_sSup
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing.IsNilpotent L
⊢ Eq (α := LieSubmodule R L L) (maxNilpotentIdeal R L) ⊤

Tactic:
maxNilpotentSubmodule_eq_top_of_isNilpotent R L L

Premises used: LieAlgebra.maxNilpotentIdeal, LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent
-- Module: Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ IsScalarTower.{u, v, v} R (CommutatorRing L) (CommutatorRing L)

Tactic:
⟨smul_lie (L := L) (M := L)⟩

Premises used: smul_lie, IsScalarTower.mk
-- Module: Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ SMulCommClass.{u, v, v} R (CommutatorRing L) (CommutatorRing L)

Tactic:
⟨fun t x y => (lie_smul t x y).symm⟩

Premises used: lie_smul, SMulCommClass.mk, Eq.symm
-- Module: Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
L₂ : Type w
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
⊢ Function.Injective (α := L →ₗ⁅R⁆ L₂) toNonUnitalAlgHom

Tactic:
fun _ _ h => ext <| NonUnitalAlgHom.congr_fun h

Premises used: NonUnitalAlgHom.congr_fun, LieHom.ext, Function.Injective
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a b : M
hm₁ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} a
hm₂ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} b
x : L
rw : ⁅x, a⁆ + ⁅x, b⁆ ∈ N
⊢ ⁅x, a + b⁆ ∈ N

Tactic:
rw [lie_add]

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a b : M
hm₁ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} a
hm₂ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} b
x : L
⊢ ⁅x, a⁆ + ⁅x, b⁆ ∈ N

Tactic:
N.add_mem' (hm₁ x) (hm₂ x)

Premises used: Submodule.toAddSubmonoid, Set.Mem, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
a b : M
hm₁ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} a
hm₂ : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} b
x : L
⊢ ⁅x, a⁆ + ⁅x, b⁆ ∈ N

Tactic:
exact N.add_mem' (hm₁ x) (hm₂ x)

Premises used: Submodule.toAddSubmonoid, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
⊢ ⁅x, 0⁆ ∈ N

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
x : L
rw : t • ⁅x, m⁆ ∈ N
⊢ ⁅x, t • m⁆ ∈ N

Tactic:
rw [lie_smul]

Premises used: lie_smul
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
x : L
⊢ t • ⁅x, m⁆ ∈ N

Tactic:
N.smul_mem' t (hm x)

Premises used: Submodule.smul_mem', Set.Mem, LieSubmodule.toSubmodule
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
x : L
⊢ t • ⁅x, m⁆ ∈ N

Tactic:
exact N.smul_mem' t (hm x)

Premises used: Submodule.smul_mem', LieSubmodule.toSubmodule
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
y : L
rw : ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆ ∈ N
⊢ ⁅y, ⁅x, m⁆⁆ ∈ N

Tactic:
rw [leibniz_lie]

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
y : L
⊢ ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆ ∈ N

Tactic:
N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))

Premises used: Submodule.toAddSubmonoid, Set.Mem, Bracket.bracket, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, LieSubmodule.lie_mem, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x : L
m : M
hm : Membership.mem (γ := Set M) {m : M | ∀ (x : L), ⁅x, m⁆ ∈ N} m
y : L
⊢ ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆ ∈ N

Tactic:
exact N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))

Premises used: Submodule.toAddSubmonoid, Bracket.bracket, LieSubmodule.toSubmodule, AddSubmonoid.toAddSubsemigroup, LieSubmodule.lie_mem, AddSubsemigroup.add_mem'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N : LieSubmodule R L M
m : M
⊢ m ∈ N.normalizer ↔ ∀ (x : L), ⁅x, m⁆ ∈ N

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N

Tactic:
fun x => N.lie_mem hm

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N

Tactic:
exact fun x => N.lie_mem hm

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : ∀ (m : M), m ∈ (N₁ ⊓ N₂).normalizer ↔ m ∈ N₁.normalizer ⊓ N₂.normalizer
⊢ (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N₁ N₂ : LieSubmodule R L M
m : M
⊢ m ∈ (N₁ ⊓ N₂).normalizer ↔ m ∈ N₁.normalizer ⊓ N₂.normalizer

Tactic:
simp [← forall_and]

Premises used: forall_and
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : m ∈ N₁.normalizer
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₁

Tactic:
rw [mem_normalizer] at hm ⊢

Premises used: LieSubmodule.mem_normalizer
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂

Tactic:
fun x ↦ h (hm x)
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
m : M
hm : ∀ (x : L), ⁅x, m⁆ ∈ N₁
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N₂

Tactic:
exact fun x ↦ h (hm x)
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ Monotone.{u_3, u_3} (α := LieSubmodule R L M) normalizer

Tactic:
fun _ _ ↦ normalizer_mono

Premises used: Monotone, LieSubmodule.normalizer_mono
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
h : ∀ (m : M'), m ∈ comap f N.normalizer ↔ m ∈ (comap f N).normalizer
⊢ comap f N.normalizer = (comap f N).normalizer

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N : LieSubmodule R L M
f : M' →ₗ⁅R,L⁆ M
m : M'
⊢ m ∈ comap f N.normalizer ↔ m ∈ (comap f N).normalizer

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N N' : LieSubmodule R L M
rw : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
⊢ Bracket.bracket.{u_2, u_3} (L := LieIdeal R L) ⊤ N ≤ N' ↔ N ≤ N'.normalizer

Tactic:
rw [lie_le_iff]

Premises used: LieSubmodule.lie_le_iff
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N N' : LieSubmodule R L M
mp : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → N ≤ N'.normalizer
mpr : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
mp₁ mp₂ : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → N ≤ N'.normalizer
mp₃ : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → ∀ ⦃x : M⦄, x ∈ N → x ∈ N'.normalizer
mpr₁ mpr₂ mpr₃ : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
mp₄ mp₅ :
  (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → ∀ ⦃x : M⦄, x ∈ N → x ∈ N'.normalizer
mp₆ :
  (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') →
    ∀ ⦃x : M⦄, x ∈ N → ∀ (x_1 : L), ⁅x_1, x⁆ ∈ N'
mpr₄ mpr₅ mpr₆ : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
mp₇ mp₈ mp₉ :
  (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') →
    ∀ ⦃x : M⦄, x ∈ N → ∀ (x_1 : L), ⁅x_1, x⁆ ∈ N'
mpr₇ mpr₈ mpr₉ : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
mp₁₀ mp₁₁ mp₁₂ :
  (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') →
    ∀ ⦃x : M⦄, x ∈ N → ∀ (x_1 : L), ⁅x_1, x⁆ ∈ N'
mpr₁₀ mpr₁₁ mpr₁₂ : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
mp₁₃ mp₁₄ :
  (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') →
    ∀ ⦃x : M⦄, x ∈ N → ∀ (x_1 : L), ⁅x_1, x⁆ ∈ N'
mpr₁₃ mpr₁₄ : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
⊢ (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ GaloisConnection (fun (N : LieSubmodule R L M) ↦ Bracket.bracket.{u_2, u_3} (L := LieIdeal R L) ⊤ N) normalizer

Tactic:
top_lie_le_iff_le_normalizer

Premises used: Set.Mem, LieSubmodule.top_lie_le_iff_le_normalizer, GaloisConnection
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ Eq (α := LieSubmodule R L M) (normalizer ⊥) (LieModule.maxTrivSubmodule R L M)

Tactic:
rfl

Premises used: Set.Mem, setOf, LieModule.maxTrivSubmodule, Set.singleton, LieSubmodule.normalizer, rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
hy : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} y
m : M
rw : ⁅x, m⁆ + ⁅y, m⁆ ∈ N
⊢ ⁅x + y, m⁆ ∈ N

Tactic:
rw [add_lie]

Premises used: add_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
hy : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} y
m : M
⊢ ⁅x, m⁆ + ⁅y, m⁆ ∈ N

Tactic:
N.add_mem (hx m) (hy m)

Premises used: Set.Mem, LieSubmodule.toSubmodule, Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
hy : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} y
m : M
⊢ ⁅x, m⁆ + ⁅y, m⁆ ∈ N

Tactic:
exact N.add_mem (hx m) (hy m)

Premises used: LieSubmodule.toSubmodule, Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
⊢ Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} 0

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
x : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
m : M
rw : t • ⁅x, m⁆ ∈ N
⊢ ⁅t • x, m⁆ ∈ N

Tactic:
rw [smul_lie]

Premises used: smul_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
x : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
m : M
⊢ t • ⁅x, m⁆ ∈ N

Tactic:
N.smul_mem t (hx m)

Premises used: Set.Mem, LieSubmodule.toSubmodule, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
t : R
x : L
hx : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} x
m : M
⊢ t • ⁅x, m⁆ ∈ N

Tactic:
exact N.smul_mem t (hx m)

Premises used: LieSubmodule.toSubmodule, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hy : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} y
m : M
rw : ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ ∈ N
⊢ ⁅⁅x, y⁆, m⁆ ∈ N

Tactic:
rw [lie_lie]

Premises used: lie_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
M' : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
inst_10 : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
x y : L
hy : Membership.mem (γ := Set L) {x : L | ∀ (m : M), ⁅x, m⁆ ∈ N} y
m : M
⊢ ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ ∈ N

Tactic:
sub_mem (N.lie_mem (hy m)) (hy ⁅x, m⁆)

Premises used: Bracket.bracket, sub_mem, LieSubmodule.lie_mem