awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
refine_1 : ∀ (h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))), LieRing.IsNilpotent L
⊢ LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L)) ↔ LieRing.IsNilpotent L
have refine_2 : LieRing.IsNilpotent L → LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : LieRing.IsNilpotent.{v} ↥(LieHom.range (ad R L))
⊢ LieRing.IsNilpotent L
have this : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (center R L)
Tactic: have : (ad R L).ker = center R L := by simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k_1 : ℕ
inst_6 : LieModule R L M
k : ℕ
ih : Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(I.lcs M (k + 1)) : Submodule R M) (↑(lowerCentralSeries R (↥I) M (k + 1)) : Submodule R M)
have succ : Eq.{u_3 + 1} (α := Submodule R M)
  (Submodule.span R
    {x : M |
      ∃ x_1 ∈ I,
        ∃ (n : M),
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧ ⁅x_1, n⁆ = x})
  (Submodule.span R
    {x : M |
      ∃ (x_1 : ↥I) (n : M),
        Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥I) M) (lowerCentralSeries R (↥I) M k) n ∧
          ⁅(↑x_1 : L), n⁆ = x})
Tactic: simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule R L M
⊢ Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)
have zero : Eq (α := Submodule R M) (↑(I.lcs M 0) : Submodule R M) (↑(lowerCentralSeries R (↥I) M 0) : Submodule R M)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
    simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule R L M
zero : Eq (α := Submodule R M) (↑(I.lcs M 0) : Submodule R M) (↑(lowerCentralSeries R (↥I) M 0) : Submodule R M)
⊢ Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)
have succ : ∀ (k : ℕ)
  (ih : Eq (α := Submodule R M) (↑(I.lcs M k) : Submodule R M) (↑(lowerCentralSeries R (↥I) M k) : Submodule R M)),
  Eq (α := Submodule R M) (↑(I.lcs M (k + 1)) : Submodule R M) (↑(lowerCentralSeries R (↥I) M (k + 1)) : Submodule R M)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
      (I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top,
      true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
    simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (hypothesis)
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
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
inst_6 : LieModule.IsNilpotent L ↥I
f : ↥I →ₗ⁅R⁆ L := I.incl
g : ↥I →ₗ⁅R⁆ ↥I := LieHom.id
⊢ LieRing.IsNilpotent.{u_2} ↥I
have hfg : ∀ (x m : ↥I),
  Eq (α := ↥I) (Bracket.bracket (L := L) ((f : (a : ↥I) → L) x : L) ((g : (a : ↥I) → ↥I) m) : ↥I)
    ((g : (a : ↥I) → ↥I) ⁅x, m⁆ : ↥I)
Tactic: have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
k : ℕ
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
    (baseChange A (lowerCentralSeries R L M k))
have zero : Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0)
  (baseChange A (lowerCentralSeries R L M 0))
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
k : ℕ
zero :
  Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) 0)
    (baseChange A (lowerCentralSeries R L M 0))
⊢ Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
    (baseChange A (lowerCentralSeries R L M k))
have succ : ∀ (k : ℕ)
  (ih :
    Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k)
      (baseChange A (lowerCentralSeries R L M k))),
  Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1))
    (baseChange A (lowerCentralSeries R L M (k + 1)))
Tactic: induction k with
  | zero => simp
  | succ k ih => simp only [lowerCentralSeries_succ, ih, ← baseChange_top, lie_baseChange]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)
have obtain : ∀ (k : ℕ) (hk : Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M k) ⊥), IsNilpotent (A ⊗[R] L) (A ⊗[R] M)
Tactic: obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Nilpotent (goal)
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) ⊥
⊢ IsNilpotent (A ⊗[R] L) (A ⊗[R] M)
have rw : ∃ (k : ℕ), Eq (α := LieSubmodule A (A ⊗[R] L) (A ⊗[R] M)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k) ⊥
Tactic: rw [isNilpotent_iff A]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 + b⁆ ∈ N
have rw : ⁅x, a⁆ + ⁅x, b⁆ ∈ N
Tactic: rw [lie_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅x, t • m⁆ ∈ N
have rw : t • ⁅x, m⁆ ∈ N
Tactic: rw [lie_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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⁆⁆ ∈ N
have rw : ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆ ∈ N
Tactic: rw [leibniz_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ (N₁ ⊓ N₂).normalizer = N₁.normalizer ⊓ N₂.normalizer
have h : ∀ (m : M), m ∈ (N₁ ⊓ N₂).normalizer ↔ m ∈ N₁.normalizer ⊓ N₂.normalizer
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (hypothesis)
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
⊢ m ∈ N₂.normalizer
have hm₁ : ∀ (x : L), ⁅x, m⁆ ∈ N₁
Tactic: rw [mem_normalizer] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ comap f N.normalizer = (comap f N).normalizer
have h : ∀ (m : M'), m ∈ comap f N.normalizer ↔ m ∈ (comap f N).normalizer
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ Bracket.bracket.{u_2, u_3} (L := LieIdeal R L) ⊤ N ≤ N' ↔ N ≤ N'.normalizer
have rw : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
Tactic: rw [lie_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
have mp : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → N ≤ N'.normalizer
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
have mpr : N ≤ N'.normalizer → ∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
have mp₃ : (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') → ∀ ⦃x : M⦄, x ∈ N → x ∈ N'.normalizer
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ (∀ (x : L), Membership.mem (γ := LieIdeal R L) ⊤ x → ∀ m ∈ N, ⁅x, m⁆ ∈ N') ↔ N ≤ N'.normalizer
have 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'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 + y, m⁆ ∈ N
have rw : ⁅x, m⁆ + ⁅y, m⁆ ∈ N
Tactic: rw [add_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
have rw : t • ⁅x, m⁆ ∈ N
Tactic: rw [smul_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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⁆ ∈ N
have rw : ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ ∈ N
Tactic: rw [lie_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ idealizer I = normalizer I
have h : ∀ (x : L), Membership.mem (γ := LieSubmodule R L L) (idealizer I) x ↔ x ∈ normalizer I
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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, ⁅y, z⁆⁆ ∈ H.toLieSubmodule
have rw : ⁅⁅(↑x : L), y⁆, z⁆ - ⁅⁅(↑x : L), z⁆, y⁆ ∈ H
Tactic: rw [coe_bracket_of_module, mem_toLieSubmodule, leibniz_lie, ← lie_skew y, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 ↔ ∀ y ∈ H, ⁅y, x⁆ ∈ H
have rw : x ∈ H.normalizer ↔ ∀ (x_1 : ↥H), ⁅(↑x_1 : L), x⁆ ∈ H
Tactic: rw [Subtype.forall']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
have rw : (∀ y ∈ H, ⁅y, x⁆ ∈ H) ↔ ∀ y ∈ H, ⁅x, y⁆ ∈ H
Tactic: rw [mem_normalizer_iff']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
have refine : ∀ (y : L) (hy : y ∈ H), ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
Tactic: refine forall₂_congr fun y hy => ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
have rw : -⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
Tactic: rw [← lie_skew, neg_mem_iff (G := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅y, x⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
have rw₁ : ⁅x, y⁆ ∈ H ↔ ⁅x, y⁆ ∈ H
Tactic: rw [← lie_skew, neg_mem_iff (G := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (hypothesis)
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, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
have hy₁ : ∃ (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
Cleared hypotheses: hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (hypothesis)
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, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
have hz₁ : ∃ (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
Cleared hypotheses: hy, hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅y, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
have obtain : ∀ (u₁ : L) (hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) u₁) (v : L) (hv : v ∈ H),
  ⁅u₁ + v, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
Tactic: obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅u₁ + v, z⁆ ∈ R ∙ x ⊔ H.toSubmodule
have 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
Tactic: obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
⊢ ⁅u₁ + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
have obtain : ∀ (t : R) (hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)), ⁅t • x + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
Tactic: obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁
Cleared hypotheses: u₁, hu₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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)
⊢ ⁅t • x + v, u₂ + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
have obtain : ∀ (s : R) (hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)), ⁅t • x + v, s • x + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
Tactic: obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂
Cleared hypotheses: u₂, hu₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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)
⊢ ⁅t • x + v, s • x + w⁆ ∈ R ∙ x ⊔ H.toSubmodule
have a : ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
Tactic: apply Submodule.mem_sup_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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)
⊢ ⁅t • x + v, s • x + w⁆ ∈ H.toSubmodule
have a : s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H
Tactic: simp only [LieSubalgebra.mem_toSubmodule, smul_lie, add_lie, zero_add, lie_add, smul_zero,
    lie_smul, lie_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
have a : ⁅v, x⁆ ∈ H
Tactic: refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))