awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
⊢ (↑⁅I, N⁆ : Submodule R M) ≤ Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
have aux : ∀ (y : L) (m' : M),
  Membership.mem (γ := Submodule R M) (Submodule.span R s) m' →
    Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
Tactic: have aux : ∀ (y : L), ∀ m' ∈ Submodule.span R s, ⁅y, m'⁆ ∈ Submodule.span R s := by
      intro y m' hm'
      refine Submodule.span_induction (R := R) (M := M) (s := s)
        (p := fun m' _ ↦ ⁅y, m'⁆ ∈ Submodule.span R s) ?_ ?_ ?_ ?_ hm'
      · rintro m'' ⟨x, n, hm''⟩; rw [← hm'', leibniz_lie]
        refine Submodule.add_mem _ ?_ ?_ <;> apply Submodule.subset_span
        · use ⟨⁅y, ↑x⁆, I.lie_mem x.property⟩, n
        · use x, ⟨⁅y, ↑n⁆, N.lie_mem n.property⟩
      · simp
      · intro m₁ m₂ _ _ hm₁ hm₂; rw [lie_add]; exact Submodule.add_mem _ hm₁ hm₂
      · intro t m'' _ hm''; rw [lie_smul]; exact Submodule.smul_mem _ t hm''
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
aux :
  ∀ (y : L) (m' : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R s) m' →
      Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
⊢ (↑⁅I, N⁆ : Submodule R M) ≤ Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
have a : ⁅I, N⁆ ≤
  let __src : Submodule R M := Submodule.span R s;
  { toSubmodule := __src, lie_mem := sorry }
Tactic: change _ ≤ ({ Submodule.span R s with lie_mem := fun hm' => aux _ _ hm' } : LieSubmodule R L M)
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
s : Set M := {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
aux :
  ∀ (y : L) (m' : M),
    Membership.mem (γ := Submodule R M) (Submodule.span R s) m' →
      Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆
⊢ ⁅I, N⁆ ≤
    let __src : Submodule R M := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }
have a : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆
  (↑(let __src : Submodule R M := Submodule.span R s;
      { toSubmodule := __src, lie_mem := sorry : LieSubmodule R L M }) :
    Set M)
Tactic: rw [lieIdeal_oper_eq_span, lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
⊢ (↑⁅I, N⁆ : Submodule R M) = Submodule.span R {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
have rw : Eq.{w + 1} (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
  (Submodule.span R {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})
Tactic: rw [lieIdeal_oper_eq_linear_span]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
⊢ Eq.{w + 1} (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    (Submodule.span R {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})
have e_s : Eq.{w + 1} (α := M → Prop) (fun (x : M) ↦ ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x) fun (x : M) ↦
  ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
⊢ Eq.{w + 1} (α := M → Prop) (fun (x : M) ↦ ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x) fun (x : M) ↦
    ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x
have e_s : ∀ (m : M), (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔ ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
m : M
⊢ (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔ ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m
have e_s : (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) → ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
inst_6 : LieModule R L M
m : M
e_s : (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) → ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m
⊢ (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔ ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m
have e_s₁ : (∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m) → ∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
have rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
Tactic: rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
have refine : (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N') → {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M)
Tactic: refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
⊢ Membership.mem (γ := LieSubmodule R L M) (lieSpan R L {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    ⁅(↑x : L), (↑m : M)⁆
have a : Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅(↑x : L), (↑m : M)⁆
Tactic: apply subset_lieSpan
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
x : ↥I
m : ↥N
w : ↥I
w₁ : ↥N
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅(↑x : L), (↑m : M)⁆
have h : ⁅(↑x : L), (↑m : M)⁆ = ⁅(↑x : L), (↑m : M)⁆
Tactic: use x, m
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ = ⁅J, I⁆
have suffices : ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
Tactic: suffices ∀ I J : LieIdeal R L, ⁅I, J⁆ ≤ ⁅J, I⁆ by exact le_antisymm (this I J) (this J I)
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ ⁅J, I⁆
have rw : {x : L | ∃ (x_1 : ↥I) (n : ↥J), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑⁅J, I⁆ : Set L)
Tactic: rw [lieIdeal_oper_eq_span, lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅(↑y : L), (↑z : L)⁆ = x
⊢ x ∈ (↑⁅J, I⁆ : Set L)
have rw : ⁅(↑y : L), (↑z : L)⁆ ∈ (↑⁅J, I⁆ : Set L)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅(↑y : L), (↑z : L)⁆ = x
⊢ ⁅(↑y : L), (↑z : L)⁆ ∈ (↑⁅J, I⁆ : Set L)
have rw : ⁅(↑z : L), (↑(-y) : L)⁆ ∈ (↑⁅J, I⁆ : Set L)
Tactic: rw [← lie_skew, ← lie_neg, ← LieSubmodule.coe_neg]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ N
have rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
Tactic: rw [lieIdeal_oper_eq_span, lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
m : M
x : ↥I
n : ↥N
hn : ⁅(↑x : L), (↑n : M)⁆ = m
⊢ m ∈ (↑N : Set M)
have rw : ⁅(↑x : L), (↑n : M)⁆ ∈ (↑N : Set M)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I
have rw : ⁅J, I⁆ ≤ I
Tactic: rw [lie_comm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I ⊓ J
have rw : ⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J
Tactic: rw [le_inf_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ Eq.{w + 1} (α := LieSubmodule R L M) ⁅I, ⊥⁆ ⊥
have rw : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) ⁅I, ⊥⁆ m → m = 0
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N = ⊥
have suffices : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N ≤ ⊥
Tactic: suffices ⁅(⊥ : LieIdeal R L), N⁆ ≤ ⊥ by exact le_bot_iff.mp this
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N ≤ ⊥
have rw : {x : M | ∃ (x_1 : ↥⊥) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑⊥ : Set M)
Tactic: rw [lieIdeal_oper_eq_span, lieSpan_le]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
m : M
x : L
hx : Membership.mem (γ := LieIdeal R L) ⊥ x
n : ↥N
hn : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ = m
⊢ m ∈ (↑⊥ : Set M)
have rw : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
m : M
x : L
hx : Membership.mem (γ := LieIdeal R L) ⊥ x
n : ↥N
hn : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ = m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)
have change : ∀ (hx : Membership.mem (γ := LieIdeal R L) ⊥ x)
  (hn : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ = m),
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)
Tactic: change x ∈ (⊥ : LieIdeal R L) at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
m : M
x : L
n : ↥N
hx : Membership.mem (γ := LieIdeal R L) ⊥ x
hn : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ = m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)
have hx₁ : x = 0
Tactic: rw [mem_bot] at hx
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
have rw : (∀ (m : M), Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} m → m = 0) ↔
  ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
Tactic: rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ (∀ (m : M), Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} m → m = 0) ↔
    ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
have refine : (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0) →
  ∀ (m : M), Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} m → m = 0
Tactic: refine ⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : m ∈ ⁅I, N⁆
⊢ m ∈ ⁅J, N'⁆
have h₃ : ∀ (N_1 : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N_1 : Set M) → m ∈ N_1
Tactic: rw [lieIdeal_oper_eq_span, mem_lieSpan] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N ≤ N'
m : M
h : ∀ (N_1 : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N_1 : Set M) → m ∈ N_1
⊢ m ∈ ⁅J, N'⁆
have rw : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
Tactic: rw [lieIdeal_oper_eq_span, mem_lieSpan]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
⊢ m ∈ N
have a : {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N_1
hm : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ = m'
⊢ m' ∈ (↑N : Set M)
have a : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ ∈
  (↑N : Set M)
Tactic: rw [← hm]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N_1
hm : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ = m'
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ ∈
    (↑N : Set M)
have a : Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆
Tactic: apply hN
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N_1
hm : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ = m'
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆
have w : ↥J
Tactic: use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N_1
hm : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ = m'
w : ↥J
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆
have w₁ : ↥N'
Tactic: use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N_1 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h₁ : I ≤ J
h₂ : N_1 ≤ N'
m : M
h : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
N : LieSubmodule R L M
hN : {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
m' : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N_1
hm : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆ = m'
w : ↥J
w₁ : ↥N'
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x}
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆
have h₃ : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ J) x sorry) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n sorry) : M)⁆ =
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : M)⁆
Tactic: use ⟨x, h₁ hx⟩, ⟨n, h₂ hn⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have rw : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
Tactic: rw [sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have left : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have right : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
have left : N ≤ N ⊔ N'
Tactic: apply mono_lie_right
-- Lean 4 proof step from Mathlib.Algebra.Lie.IdealOperations (goal)
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have right : N' ≤ N ⊔ N'
Tactic: apply mono_lie_right