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 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)⁆ +
      ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ =
    m

Tactic:
simp [← 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
rw : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆
right : ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : I ≤ I ⊔ J
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆

Tactic:
apply mono_lie_left

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

Tactic:
apply mono_lie_left

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

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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ I ≤ I ⊔ J

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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ J ≤ I ⊔ J

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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ J ≤ I ⊔ J

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

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

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

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

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

Tactic:
rw [LieSubmodule.mem_sup] at hx ⊢

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

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

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

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

Tactic:
simp [← h, ← 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 N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
rw : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆

Tactic:
rw [le_inf_iff]

Premises used: le_inf_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 ⊓ N'⁆ ≤ ⁅I, N⁆
right : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, 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 ⊓ N'⁆ ≤ ⁅I, 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 ⊓ N'⁆ ≤ ⁅I, 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:
inf_le_left

Premises used: Set.Mem, inf_le_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:
exact inf_le_left

Premises used: inf_le_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:
inf_le_right

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

Tactic:
exact inf_le_right

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

Tactic:
constructor <;>
  apply mono_lie_right <;> [exact inf_le_left; exact inf_le_right]

Premises used: inf_le_right, LieSubmodule.mono_lie_right, inf_le_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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
rw : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ⊓ ⁅J, N⁆

Tactic:
rw [le_inf_iff]

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

Tactic:
apply mono_lie_left

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

Tactic:
apply mono_lie_left

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

Tactic:
inf_le_left

Premises used: Set.Mem, inf_le_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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ I ⊓ J ≤ I

Tactic:
exact inf_le_left

Premises used: inf_le_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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ I ⊓ J ≤ J

Tactic:
inf_le_right

Premises used: Set.Mem, inf_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
I J : LieIdeal R L
⊢ I ⊓ J ≤ J

Tactic:
exact inf_le_right

Premises used: inf_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
I J : LieIdeal R L
left : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₁ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₁ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₂ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₂ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₃ : ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆
right₃ : ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆
left₄ : I ⊓ J ≤ I
right₄ : I ⊓ J ≤ J
left₅ : I ⊓ J ≤ I
right₅ : I ⊓ J ≤ J
⊢ ⁅I ⊓ J, N⁆ ≤ ⁅I, N⁆ ∧ ⁅I ⊓ J, N⁆ ≤ ⁅J, N⁆

Tactic:
constructor <;>
  apply mono_lie_left <;> [exact inf_le_left; exact inf_le_right]

Premises used: inf_le_right, LieSubmodule.mono_lie_left, inf_le_left
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
M : Type w
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 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
rw :
  Eq.{w₁ + 1} (α := Submodule R M₂)
    (Submodule.span R
      (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
        {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}))
    (Submodule.span R {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x})
⊢ map f ⁅I, N⁆ = ⁅I, map f N⁆

Tactic:
rw [← toSubmodule_inj, toSubmodule_map, lieIdeal_oper_eq_linear_span,
    lieIdeal_oper_eq_linear_span, Submodule.map_span]

Premises used: LieSubmodule.toSubmodule_map, LieSubmodule.toSubmodule_inj, LieSubmodule.lieIdeal_oper_eq_linear_span, Submodule.map_span
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
M : Type w
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 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
e_s :
  Eq.{w₁ + 1} (α := Set M₂)
    (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
      {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x}
⊢ Eq.{w₁ + 1} (α := Submodule R M₂)
    (Submodule.span R
      (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
        {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x}))
    (Submodule.span R {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x})

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
M : Type w
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 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
e_s :
  ∀ (m : M₂),
    Membership.mem (γ := Set M₂)
        (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
          {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
        m ↔
      Membership.mem (γ := Set M₂) {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x} m
⊢ Eq.{w₁ + 1} (α := Set M₂)
    (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
      {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
    {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x}

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.IdealOperations
Goal:
R : Type u
L : Type v
M : Type w
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 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst_8 : LieAlgebra R L
inst_9 : LieModule R L M₂
I : LieIdeal R L
inst_10 : LieModule R L M
m : M₂
⊢ Membership.mem (γ := Set M₂)
      (Set.image.{w, w₁} (α := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂)
        {x : M | ∃ (x_1 : ↥I) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x})
      m ↔
    Membership.mem (γ := Set M₂) {x : M₂ | ∃ (x_1 : ↥I) (n : ↥(map f N)), ⁅(↑x_1 : L), (↑n : M₂)⁆ = x} m

Tactic:
simp