awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
t : R
m'' : M
refine_4 :
  ∀ (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        m'' hx →
      (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        (t • m'') ⋯
⊢ ∀ (hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''),
    (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        m'' hx →
      (fun (m' : M) (x : Membership.mem (γ := Submodule R M) (Submodule.span R s) m') ↦
          Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m'⁆)
        (t • m'') ⋯

Tactic:
_
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
t : R
m'' : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''
hm'' : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆
refine_4 : Membership.mem (γ := Submodule R M) (Submodule.span R s) (t • ⁅y, m''⁆)
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, t • m''⁆

Tactic:
rw [lie_smul]

Premises used: lie_smul
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
t : R
m'' : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''
hm'' : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) (t • ⁅y, m''⁆)

Tactic:
Submodule.smul_mem _ t hm''

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
y : L
m' : M
hm' : Membership.mem (γ := Submodule R M) (Submodule.span R s) m'
t : R
m'' : M
hx : Membership.mem (γ := Submodule R M) (Submodule.span R s) m''
hm'' : Membership.mem (γ := Submodule R M) (Submodule.span R s) ⁅y, m''⁆
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R s) (t • ⁅y, m''⁆)

Tactic:
exact Submodule.smul_mem _ t hm''

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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}
⊢ ∀ (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''
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'⁆
a :
  ⁅I, N⁆ ≤
    let __src : Submodule R M := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }
⊢ (↑⁅I, N⁆ : Submodule R M) ≤ Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}

Tactic:
change _ ≤ ({ Submodule.span R s with lie_mem := fun hm' => aux _ _ hm' } : LieSubmodule R L M)

Premises used: Submodule.span, LieSubmodule.mk
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'⁆
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 := ⋯ : LieSubmodule R L M }) :
      Set M)
⊢ ⁅I, N⁆ ≤
    let __src : Submodule R M := Submodule.span R s;
    { toSubmodule := __src, lie_mem := ⋯ }

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'⁆
⊢ {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 := ⋯ : LieSubmodule R L M }) :
      Set M)

Tactic:
Submodule.subset_span

Premises used: Set.Mem, setOf, Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'⁆
⊢ {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 := ⋯ : LieSubmodule R L M }) :
      Set M)

Tactic:
exact Submodule.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ LE.le.{w} (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    (↑(lieSpan R L {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}) : Submodule R M)

Tactic:
apply submodule_span_le_lieSpan

Premises used: LieSubmodule.submodule_span_le_lieSpan
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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})
⊢ (↑⁅I, N⁆ : Submodule R M) = Submodule.span R {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}

Tactic:
rw [lieIdeal_oper_eq_linear_span]

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
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
⊢ 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:
congr
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
e_s : ∀ (m : M), (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔ ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = 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

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
e_s₁ : (∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m) → ∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m
⊢ (∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m) ↔ ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ x_1 ∈ I,
    ∃ n_1 ∈ N,
      ⁅x_1, n_1⁆ =
        ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆

Tactic:
⟨x, hx, n, hn, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ x_1 ∈ I,
    ∃ n_1 ∈ N,
      ⁅x_1, n_1⁆ =
        ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆

Tactic:
exact ⟨x, hx, n, hn, rfl⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ (x_1 : ↥I) (n_1 : ↥N), ⁅(↑x_1 : L), (↑n_1 : M)⁆ = ⁅x, n⁆

Tactic:
⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ∃ (x_1 : ↥I) (n_1 : ↥N), ⁅(↑x_1 : L), (↑n_1 : M)⁆ = ⁅x, n⁆

Tactic:
exact ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
⊢ ⁅I, N⁆ ≤ N' ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.IdealOperations
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'

Tactic:
⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩

Premises used: Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
refine : (∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N') → {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M)
⊢ {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N' : Set M) ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'

Tactic:
refine ⟨fun h x hx m hm => h ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M)⁆ ∈
    (↑N' : Set M)

Tactic:
h x hx m hm

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ ∈ N'
x : L
hx : x ∈ I
m : M
hm : m ∈ N
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm) : M)⁆ ∈
    (↑N' : Set M)

Tactic:
exact h x hx m hm
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
a : Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅(↑x : L), (↑m : M)⁆
⊢ 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)⁆

Tactic:
apply subset_lieSpan

Premises used: LieSubmodule.subset_lieSpan
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
h : ⁅(↑x : L), (↑m : M)⁆ = ⁅(↑x : L), (↑m : M)⁆
⊢ Membership.mem (γ := Set M) {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⁅(↑x : L), (↑m : M)⁆

Tactic:
use x, m
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 : L
m : M
hx : x ∈ I
hm : m ∈ N
⊢ ⁅x, m⁆ ∈ ⁅I, N⁆

Tactic:
lie_coe_mem_lie ⟨x, hx⟩ ⟨m, hm⟩

Premises used: Set.Mem, Subtype.mk, LieSubmodule.lie_coe_mem_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
this : ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
le_antisymm (this I J) (this J I)

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
this : ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
exact le_antisymm (this I J) (this J I)

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
suffices : ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
⊢ ⁅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)
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
rw : {x : L | ∃ (x_1 : ↥I) (n : ↥J), ⁅(↑x_1 : L), (↑n : L)⁆ = x} ⊆ (↑⁅J, I⁆ : Set L)
⊢ ⁅I, J⁆ ≤ ⁅J, I⁆

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : ⁅(↑y : L), (↑z : L)⁆ ∈ (↑⁅J, I⁆ : Set L)
⊢ x ∈ (↑⁅J, I⁆ : Set L)

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : ⁅(↑z : L), (↑(-y) : L)⁆ ∈ (↑⁅J, I⁆ : Set L)
⊢ ⁅(↑y : L), (↑z : L)⁆ ∈ (↑⁅J, I⁆ : Set L)

Tactic:
rw [← lie_skew, ← lie_neg, ← LieSubmodule.coe_neg]

Premises used: lie_neg, lie_skew, LieSubmodule.coe_neg
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅(↑z : L), (↑(-y) : L)⁆ ∈ (↑⁅J, I⁆ : Set L)

Tactic:
apply lie_coe_mem_lie

Premises used: LieSubmodule.lie_coe_mem_lie
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
⊢ ⁅I, N⁆ ≤ N

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : ⁅(↑x : L), (↑n : M)⁆ ∈ (↑N : Set M)
⊢ m ∈ (↑N : Set M)

Tactic:
rw [← hn]
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅(↑x : L), (↑n : M)⁆ ∈ (↑N : Set M)

Tactic:
N.lie_mem n.property

Premises used: Set.Mem, LieSubmodule.lie_mem, Subtype.property
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ⁅(↑x : L), (↑n : M)⁆ ∈ (↑N : Set M)

Tactic:
exact N.lie_mem n.property

Premises used: LieSubmodule.lie_mem, Subtype.property
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
rw : ⁅J, I⁆ ≤ I
⊢ ⁅I, J⁆ ≤ I

Tactic:
rw [lie_comm]

Premises used: LieSubmodule.lie_comm
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅J, I⁆ ≤ I

Tactic:
lie_le_right I J

Premises used: Set.Mem, LieSubmodule.lie_le_right
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅J, I⁆ ≤ I

Tactic:
exact lie_le_right I J

Premises used: LieSubmodule.lie_le_right
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I J : LieIdeal R L
rw : ⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J
⊢ ⁅I, J⁆ ≤ I ⊓ J

Tactic:
rw [le_inf_iff]

Premises used: le_inf_iff
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 ∧ ⁅I, J⁆ ≤ J

Tactic:
⟨lie_le_left I J, lie_le_right J I⟩

Premises used: LieSubmodule.lie_le_right, And.intro, LieSubmodule.lie_le_left
-- Module: Mathlib.Algebra.Lie.IdealOperations
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 ∧ ⁅I, J⁆ ≤ J

Tactic:
exact ⟨lie_le_left I J, lie_le_right J I⟩
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
rw : ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) ⁅I, ⊥⁆ m → m = 0
⊢ Eq.{w + 1} (α := LieSubmodule R L M) ⁅I, ⊥⁆ ⊥

Tactic:
rw [eq_bot_iff]

Premises used: LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
⊢ ∀ (m : M), Membership.mem (γ := LieSubmodule R L M) ⁅I, ⊥⁆ m → m = 0

Tactic:
apply lie_le_right

Premises used: LieSubmodule.lie_le_right
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
this : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N ≤ ⊥
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N = ⊥

Tactic:
le_bot_iff.mp this

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.IdealOperations
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
this : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N ≤ ⊥
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N = ⊥

Tactic:
exact le_bot_iff.mp this

Premises used: le_bot_iff, Iff.mp