awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact sub_mem (N.lie_mem (hy m)) (hy ⁅x, m⁆)

Premises used: Bracket.bracket, sub_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
x : L
⊢ Membership.mem (γ := LieIdeal R L) N.idealizer x ↔ ∀ (m : M), ⁅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
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
h : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (idealizer I) x ↔ x ∈ normalizer I
⊢ idealizer I = normalizer I

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
⊢ ⁅x, y⁆ ∈ I ↔ ⁅y, x⁆ ∈ I

Tactic:
simp only [← lie_skew x y, neg_mem_iff]

Premises used: neg_mem_iff, lie_skew
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ Membership.mem (γ := LieSubmodule R L L) (idealizer I) x ↔ x ∈ normalizer I

Tactic:
exact forall_congr' fun y ↦ by simp only [← lie_skew x y, neg_mem_iff]

Premises used: forall_congr'
-- 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'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
x : ↥H
rw : ⁅⁅(↑x : L), y⁆, z⁆ - ⁅⁅(↑x : L), z⁆, y⁆ ∈ H
⊢ ⁅x, ⁅y, z⁆⁆ ∈ H.toLieSubmodule

Tactic:
rw [coe_bracket_of_module, mem_toLieSubmodule, leibniz_lie, ← lie_skew y, ← sub_eq_add_neg]

Premises used: leibniz_lie, sub_eq_add_neg, LieSubalgebra.coe_bracket_of_module, LieSubalgebra.mem_toLieSubmodule, lie_skew
-- 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'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
x : ↥H
⊢ ⁅⁅(↑x : L), y⁆, z⁆ - ⁅⁅(↑x : L), z⁆, y⁆ ∈ H

Tactic:
H.sub_mem (hz ⟨_, hy x⟩) (hy ⟨_, hz x⟩)

Premises used: Subtype.mk, LieSubalgebra.sub_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'
H : LieSubalgebra R L
y z : L
hy : y ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
hz : z ∈ (↑H.toLieSubmodule.normalizer : Submodule R L).carrier
x : ↥H
⊢ ⁅⁅(↑x : L), y⁆, z⁆ - ⁅⁅(↑x : L), z⁆, y⁆ ∈ H

Tactic:
exact H.sub_mem (hz ⟨_, hy x⟩) (hy ⟨_, hz x⟩)

Premises used: Subtype.mk, LieSubalgebra.sub_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
rw : x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅(↑x_1 : L), x⁆ ∈ H
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H

Tactic:
rw [Subtype.forall']

Premises used: Subtype.forall'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅(↑x_1 : L), x⁆ ∈ H

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
rw : (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
⊢ x ∈ H.normalizer ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
rw [mem_normalizer_iff']

Premises used: LieSubalgebra.mem_normalizer_iff'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
forall₂_congr fun y hy => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
refine : ∀ (y : L) (hy : y ∈ H), ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
⊢ (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H

Tactic:
refine forall₂_congr fun y hy => ?_

Premises used: forall₂_congr
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hy : y ∈ H
rw : -⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
rw₁ rw₂ : ⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H

Tactic:
rw [← lie_skew, neg_mem_iff (G := L)]

Premises used: neg_mem_iff, lie_skew
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
⊢ H ≤ H.normalizer

Tactic:
H.toLieSubmodule.le_normalizer

Premises used: Set.Mem, LieSubalgebra.toLieSubmodule, LieSubmodule.le_normalizer
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
⊢ (↑H.toLieSubmodule.normalizer : Submodule R L) = H.normalizer.toSubmodule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : y ∈ R ∙ x ⊔ H.toSubmodule
hz : z ∈ R ∙ x ⊔ H.toSubmodule
⊢ ∃ (y_1 : L), Membership.mem (γ := Submodule R L) (R ∙ x) y_1 ∧ ∃ z ∈ H.toSubmodule, y_1 + z = y

Tactic:
rw [Submodule.mem_sup] at hy hz

Premises used: Submodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : y ∈ R ∙ x ⊔ H.toSubmodule
hz : z ∈ R ∙ x ⊔ H.toSubmodule
hy₁ : ∃ (y_1 : L), Membership.mem (γ := Submodule R L) (R ∙ x) y_1 ∧ ∃ z ∈ H.toSubmodule, y_1 + z = y
⊢ ∃ (y : L), Membership.mem (γ := Submodule R L) (R ∙ x) y ∧ ∃ z_1 ∈ H.toSubmodule, y + z_1 = z

Tactic:
rw [Submodule.mem_sup] at hy hz

Premises used: Submodule.mem_sup
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y z : L
hx : x ∈ H.normalizer
hy : ∃ (y_1 : L), Membership.mem (γ := Submodule R L) (R ∙ x) y_1 ∧ ∃ z ∈ H.toSubmodule, y_1 + z = y
hz : ∃ (y : L), Membership.mem (γ := Submodule R L) (R ∙ x) y ∧ ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
obtain :
  ∀ (u₁ : L) (hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) u₁) (v : L) (hv : v ∈ H),
    ⁅u₁ + v, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x z : L
hx : x ∈ H.normalizer
hz : ∃ (y : L), Membership.mem (γ := Submodule R L) (R ∙ x) y ∧ ∃ z_1 ∈ H.toSubmodule, y + z_1 = z
u₁ : L
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) u₁
v : L
hv : v ∈ H
obtain :
  ∀ (u₂ : L) (hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) u₂) (w : L) (hw : w ∈ H),
    ⁅u₁ + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
⊢ ⁅u₁ + v, z⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
u₁ : L
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) u₁
v : L
hv : v ∈ H
u₂ : L
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) u₂
w : L
hw : w ∈ H
obtain :
  ∀ (t : R) (hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)), ⁅t • x + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
⊢ ⁅u₁ + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
u₂ : L
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) u₂
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
obtain :
  ∀ (s : R) (hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)), ⁅t • x + v, s • x + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
⊢ ⁅t • x + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
a : ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
⊢ ⁅t • x + v, s • x + w⁆ ∈ R ∙ x ⊔ H.toSubmodule

Tactic:
apply Submodule.mem_sup_right

Premises used: Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
a : s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule

Tactic:
simp only [LieSubalgebra.mem_toSubmodule, smul_lie, add_lie, zero_add, lie_add, smul_zero,
    lie_smul, lie_self]

Premises used: lie_smul, LieSubalgebra.mem_toSubmodule, smul_zero, lie_self, zero_add, smul_lie, lie_add, add_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H

Tactic:
H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))

Premises used: LieSubalgebra.add_mem, LieSubalgebra.smul_mem, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
a : ⁅v, x⁆ ∈ H
a₁ : ⁅x, w⁆ ∈ H
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H

Tactic:
refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))

Premises used: LieSubalgebra.add_mem, LieSubalgebra.smul_mem, LieSubalgebra.lie_mem
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
⊢ ⁅v, x⁆ ∈ H

Tactic:
(H.mem_normalizer_iff' x).mp hx v hv

Premises used: LieSubalgebra.mem_normalizer_iff', Iff.mp
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
⊢ ⁅x, w⁆ ∈ H

Tactic:
(H.mem_normalizer_iff x).mp hx w hw

Premises used: Iff.mp, LieSubalgebra.mem_normalizer_iff
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
⊢ ⁅v, x⁆ ∈ H

Tactic:
exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]

Premises used: LieSubalgebra.mem_normalizer_iff', Iff.mp, LieSubalgebra.mem_normalizer_iff
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
rw : ⁅y, x⁆ ∈ H
⊢ ⁅x, y⁆ ∈ H

Tactic:
rw [← lie_skew, neg_mem_iff (G := L)]

Premises used: neg_mem_iff, lie_skew
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
hx ⟨y, hy⟩

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
exact hx ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
rw : ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
⊢ ∃ (I : LieIdeal R ↥K), LieIdeal.toLieSubalgebra R (↥K) I = ofLe h₁

Tactic:
rw [exists_nested_lieIdeal_coe_eq_iff]

Premises used: LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : 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:
fun x y hx hy => ideal_in_normalizer (h₂ hx) hy

Premises used: LieSubalgebra.ideal_in_normalizer
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : 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:
exact fun x y hx hy => ideal_in_normalizer (h₂ hx) hy

Premises used: LieSubalgebra.ideal_in_normalizer
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
rw :
  H.normalizer = H ↔
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0
⊢ H.normalizer = H ↔
    Eq.{u_2 + 1} (α := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
      (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) ⊥

Tactic:
rw [LieSubmodule.eq_bot_iff]

Premises used: LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
⊢ H.normalizer = H ↔
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0

Tactic:
⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩

Premises used: LieSubalgebra.le_normalizer, le_antisymm, Iff.intro
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
refine_1 :
  ∀ (h : H.normalizer = H) (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
refine_2 :
  ∀
    (h :
      ∀ (m : L ⧸ H.toLieSubmodule),
        Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
            (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
          m = 0),
    H.normalizer ≤ H
⊢ H.normalizer = H ↔
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0

Tactic:
refine ⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
this : x ∈ H
rwa : Eq (α := L ⧸ H.toLieSubmodule) (Submodule.Quotient.mk x) 0
rwa₁ : x ∈ (↑H.toLieSubmodule : Submodule R L)
rwa₂ : x ∈ H.toSubmodule
rwa₃ rwa₄ rwa₅ rwa₆ : x ∈ H
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0

Tactic:
rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]

Premises used: LieSubalgebra.mem_toSubmodule, LieSubalgebra.coe_toLieSubmodule, Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
refine_1 : x ∈ H
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0

Tactic:
suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
refine_1 : ∀ y ∈ H, ⁅y, x⁆ ∈ H
⊢ x ∈ H

Tactic:
rw [← h, H.mem_normalizer_iff']

Premises used: LieSubalgebra.mem_normalizer_iff'
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
y : L
hy : y ∈ H
⊢ Eq (α := L ⧸ H.toLieSubmodule)
    (⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy,
        (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x⁆ :
      L ⧸ H.toLieSubmodule)
    (0 : L ⧸ H.toLieSubmodule)

Tactic:
replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx :
  Eq (α := L ⧸ H.toLieSubmodule)
    (⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy,
        (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x⁆ :
      L ⧸ H.toLieSubmodule)
    (0 : L ⧸ H.toLieSubmodule)
refine_1 :
  ∀
    (hx :
      Eq (α := L ⧸ H.toLieSubmodule)
        ((LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule)
            ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ :
          L ⧸ H.toLieSubmodule)
        (0 : L ⧸ H.toLieSubmodule)),
    ⁅y, x⁆ ∈ H
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀ (hx : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ ∈ H.toLieSubmodule), ⁅y, x⁆ ∈ H
⊢ ⁅y, x⁆ ∈ H

Tactic:
rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx

Premises used: LieSubmodule.Quotient.mk_eq_zero, LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h :
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x
z : L
hz : z ∈ H
rw : ⁅z, x⁆ ∈ H
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz, y⁆ = 0

Tactic:
rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
        Submodule.coe_mk, mem_toLieSubmodule]

Premises used: LieSubmodule.Quotient.mk_eq_zero, LieSubalgebra.coe_bracket_of_module, Submodule.coe_mk, LieSubalgebra.mem_toLieSubmodule, LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h :
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Tactic:
(H.mem_normalizer_iff' x).mp hx z hz

Premises used: LieSubalgebra.mem_normalizer_iff', Iff.mp
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h :
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x
z : L
hz : z ∈ H
⊢ ⁅z, x⁆ ∈ H

Tactic:
exact (H.mem_normalizer_iff' x).mp hx z hz

Premises used: LieSubalgebra.mem_normalizer_iff', Iff.mp