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
suffices : Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N ≤ ⊥
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ N = ⊥

Tactic:
suffices ⁅(⊥ : LieIdeal R L), N⁆ ≤ ⊥ by exact le_bot_iff.mp this
-- 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
rw : {x : M | ∃ (x_1 : ↥⊥) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑⊥ : Set M)
⊢ Bracket.bracket.{v, w} (L := LieIdeal R L) ⊥ 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
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
rw : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)
⊢ m ∈ (↑⊥ : 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
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
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)
⊢ ⁅(↑(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

Premises used: Bot.bot
-- 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
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
⊢ x = 0

Tactic:
rw [mem_bot] at hx

Premises used: LieSubmodule.mem_bot
-- 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
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
hx₁ : x = 0
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx) : L), (↑n : M)⁆ = m

Tactic:
rw [mem_bot] at hx

Premises used: LieSubmodule.mem_bot
-- 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
m : M
x : L
n : ↥N
hx_1 : Membership.mem (γ := LieIdeal R L) ⊥ x
hx : x = 0
hn : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx_1) : L), (↑n : M)⁆ = m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) ⊥ x) x hx_1) : L), (↑n : M)⁆ ∈ (↑⊥ : Set M)

Tactic:
simp [hx]
-- 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 :
  (∀ (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
⊢ ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0

Tactic:
rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_iff]

Premises used: LieSubmodule.lieSpan_eq_bot_iff, LieSubmodule.lieIdeal_oper_eq_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
⊢ (∀ (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:
⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩

Premises used: Bracket.bracket, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
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
⊢ (∀ (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:
refine ⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆ = 0

Tactic:
h x hx n 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
h : ∀ x ∈ I, ∀ m ∈ N, ⁅x, m⁆ = 0
x : L
hx : x ∈ I
n : M
hn : n ∈ N
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆ = 0

Tactic:
exact h x hx n 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 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⁆
⊢ ∀ (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

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.mem_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 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
rw : ∀ (N : LieSubmodule R L M), {x : M | ∃ (x_1 : ↥J) (n : ↥N'), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M) → m ∈ N
⊢ m ∈ ⁅J, N'⁆

Tactic:
rw [lieIdeal_oper_eq_span, mem_lieSpan]

Premises used: LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.mem_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_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)
a : {x : M | ∃ (x_1 : ↥I) (n : ↥N_1), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑N : Set M)
⊢ m ∈ N

Tactic:
apply h
-- 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_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'
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)
⊢ m' ∈ (↑N : Set M)

Tactic:
rw [← 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_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'
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)⁆
⊢ ⁅(↑(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:
apply 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_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'
h₃ :
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ J) x ⋯) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n ⋯) : M)⁆ =
    ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N_1) n hn) : 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)⁆

Tactic:
use ⟨x, h₁ hx⟩, ⟨n, h₂ 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 J : LieIdeal R L
h : I ≤ J
⊢ ⁅I, N⁆ ≤ ⁅J, N⁆

Tactic:
mono_lie h (le_refl N)

Premises used: le_refl, LieSubmodule.mono_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h : N ≤ N'
⊢ ⁅I, N⁆ ≤ ⁅I, N'⁆

Tactic:
mono_lie (le_refl I) h

Premises used: le_refl, LieSubmodule.mono_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
rw : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
rw [sup_le_iff]

Premises used: sup_le_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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
right : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : N ≤ N ⊔ N'
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
apply mono_lie_right

Premises used: LieSubmodule.mono_lie_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
right : N' ≤ N ⊔ N'
⊢ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
apply mono_lie_right

Premises used: LieSubmodule.mono_lie_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ N ≤ N ⊔ N'

Tactic:
le_sup_left

Premises used: le_sup_left, 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
⊢ N ≤ N ⊔ N'

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- 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
⊢ N' ≤ N ⊔ N'

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ N' ≤ N ⊔ N'

Tactic:
exact le_sup_right

Premises used: le_sup_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
right : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
left₁ : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
right₁ : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
left₂ : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
right₂ : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
left₃ : ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆
right₃ : ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
left₄ : N ≤ N ⊔ N'
right₄ : N' ≤ N ⊔ N'
left₅ : N ≤ N ⊔ N'
right₅ : N' ≤ N ⊔ N'
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
constructor <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_right]

Premises used: le_sup_left, le_sup_right, LieSubmodule.mono_lie_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆

Tactic:
have h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆ := by
    rw [sup_le_iff]; constructor <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
this : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
le_antisymm this h

Premises used: le_antisymm
-- 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 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
this : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
exact le_antisymm this h

Premises used: le_antisymm
-- 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 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
suffices : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
suffices ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆ by exact le_antisymm this h
-- 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 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
rw : {x : M | ∃ (x_1 : ↥I) (n : ↥(N ⊔ N')), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑(⁅I, N⁆ ⊔ ⁅I, N'⁆) : Set M)
⊢ ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, 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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
rw :
  ∀ (hn_1 : ∃ y ∈ N, ∃ z ∈ N', y + z = n)
    (h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m),
    ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
⊢ m ∈ ⁅I, N⁆ ⊔ ⁅I, N'⁆

Tactic:
rw [LieSubmodule.mem_sup] at hn ⊢

Premises used: LieSubmodule.mem_sup
-- 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_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn_1 : n ∈ N ⊔ N'
hn : ∃ y ∈ N, ∃ z ∈ N', y + z = n
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn_1) : M)⁆ = m
rcases : ∀ (n₁ : M) (hn₁ : n₁ ∈ N) (n₂ : M) (hn₂ : n₂ ∈ N') (hn' : n₁ + n₂ = n), ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m

Tactic:
rcases hn with ⟨n₁, hn₁, n₂, hn₂, 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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
h₁ :
  ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ ∈ ⁅I, N⁆ ∧
    ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m

Tactic:
use ⁅(x : L), (⟨n₁, hn₁⟩ : N)⁆

Premises used: Subtype.mk, Subtype.val
-- 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_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
h₁ : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ ∈ ⁅I, N⁆
h₂ : ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m
⊢ ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ ∈ ⁅I, N⁆ ∧
    ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = 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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ ∈ ⁅I, N⁆

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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
h₁ :
  ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ ∈ ⁅I, N'⁆ ∧
    ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ +
        ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ =
      m
⊢ ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m

Tactic:
use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆

Premises used: Subtype.mk, Subtype.val
-- 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_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
h₁ : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ ∈ ⁅I, N'⁆
h₂ :
  ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ +
      ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ =
    m
⊢ ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ ∈ ⁅I, N'⁆ ∧
    ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ +
        ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ =
      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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
h_1 : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
m : M
x : ↥I
n : M
hn : n ∈ N ⊔ N'
h : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N ⊔ N') n hn) : M)⁆ = m
n₁ : M
hn₁ : n₁ ∈ N
n₂ : M
hn₂ : n₂ ∈ N'
hn' : n₁ + n₂ = n
⊢ ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ ∈ ⁅I, N'⁆

Tactic:
apply lie_coe_mem_lie

Premises used: LieSubmodule.lie_coe_mem_lie