awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_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
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 <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_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
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'⁆
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have left₄ : N ≤ N ⊔ N'
Tactic: constructor <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_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
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'
⊢ ⁅I, N⁆ ≤ ⁅I, N ⊔ N'⁆ ∧ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
have right₄ : N' ≤ N ⊔ N'
Tactic: constructor <;>
    apply mono_lie_right <;> [exact le_sup_left; exact le_sup_right]
-- 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 : LieIdeal R L
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
have h : ⁅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]
-- 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
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N ⊔ N'⁆ = ⁅I, N⁆ ⊔ ⁅I, N'⁆
have suffices : ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
Tactic: suffices ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆ by exact le_antisymm this 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 : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅I, N'⁆ ≤ ⁅I, N ⊔ N'⁆
⊢ ⁅I, N ⊔ N'⁆ ≤ ⁅I, N⁆ ⊔ ⁅I, N'⁆
have rw : {x : M | ∃ (x_1 : ↥I) (n : ↥(N ⊔ N')), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑(⁅I, N⁆ ⊔ ⁅I, 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 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
⊢ m ∈ ⁅I, N⁆ ⊔ ⁅I, N'⁆
have 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
Tactic: rw [LieSubmodule.mem_sup] at hn ⊢
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 : 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
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
have rcases : ∀ (n₁ : M) (hn₁ : n₁ ∈ N) (n₂ : M) (hn₂ : n₂ ∈ N') (hn' : n₁ + n₂ = n), ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
Tactic: rcases hn with ⟨n₁, hn₁, n₂, hn₂, hn'⟩
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 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
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅I, N'⁆, y + z = m
have 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
Tactic: use ⁅(x : L), (⟨n₁, hn₁⟩ : N)⁆
-- 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
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⁆ ∧
    ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m
have h₁ : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ ∈ ⁅I, 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
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)⁆ ∈ ⁅I, N⁆ ∧
    ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m
have h₂ : ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = 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
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
⊢ ∃ z ∈ ⁅I, N'⁆, ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n₁ hn₁) : M)⁆ + z = m
have 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
Tactic: use ⁅(x : L), (⟨n₂, hn₂⟩ : N')⁆
-- 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
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'⁆ ∧
    ⁅(↑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
have h₁ : ⁅(↑x : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N') n₂ hn₂) : M)⁆ ∈ ⁅I, 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
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)⁆ ∈ ⁅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
have 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
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 J : LieIdeal R L
⊢ ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have rw : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have left : ⁅I, N⁆ ≤ ⁅I ⊔ J, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have right : ⁅J, N⁆ ≤ ⁅I ⊔ J, 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆
have left : I ≤ I ⊔ J
Tactic: apply mono_lie_left
-- 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 J : LieIdeal R L
⊢ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have right : J ≤ I ⊔ J
Tactic: apply mono_lie_left
-- 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 J : LieIdeal R L
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have left : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆
Tactic: constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
left : ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have right : ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
Tactic: constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_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 : 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⁆
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have left₄ : I ≤ I ⊔ J
Tactic: constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_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 : 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
⊢ ⁅I, N⁆ ≤ ⁅I ⊔ J, N⁆ ∧ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
have right₄ : J ≤ I ⊔ J
Tactic: constructor <;>
    apply mono_lie_left <;> [exact le_sup_left; exact le_sup_right]
-- 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 J : LieIdeal R L
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
have h : ⁅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]
-- 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 J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I ⊔ J, N⁆ = ⁅I, N⁆ ⊔ ⁅J, N⁆
have suffices : ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆
Tactic: suffices ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆ by exact le_antisymm this 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 : LieSubmodule R L M
inst_5 : LieAlgebra R L
I J : LieIdeal R L
h : ⁅I, N⁆ ⊔ ⁅J, N⁆ ≤ ⁅I ⊔ J, N⁆
⊢ ⁅I ⊔ J, N⁆ ≤ ⁅I, N⁆ ⊔ ⁅J, N⁆
have rw : {x : M | ∃ (x_1 : ↥(I ⊔ J)) (n : ↥N), ⁅(↑x_1 : L), (↑n : M)⁆ = x} ⊆ (↑(⁅I, N⁆ ⊔ ⁅J, 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 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
⊢ m ∈ ⁅I, N⁆ ⊔ ⁅J, N⁆
have 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
Tactic: rw [LieSubmodule.mem_sup] at hx ⊢
Cleared hypotheses: n, 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 : 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
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
have rcases : ∀ (x₁ : L) (hx₁ : x₁ ∈ I) (x₂ : L) (hx₂ : x₂ ∈ J) (hx' : x₁ + x₂ = x), ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
Tactic: rcases hx with ⟨x₁, hx₁, x₂, hx₂, hx'⟩
Cleared hypotheses: hx
-- 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 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
⊢ ∃ y ∈ ⁅I, N⁆, ∃ z ∈ ⁅J, N⁆, y + z = m
have 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
Tactic: use ⁅((⟨x₁, hx₁⟩ : I) : L), (n : N)⁆
-- 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 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⁆ ∧
    ∃ z ∈ ⁅J, N⁆, ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x₁ hx₁) : L), (↑n : M)⁆ + z = m
have h₁ : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x₁ hx₁) : L), (↑n : M)⁆ ∈ ⁅I, 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 : 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⁆
⊢ ⁅(↑(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
have h₂ : ∃ z ∈ ⁅J, N⁆, ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x₁ hx₁) : L), (↑n : M)⁆ + z = 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 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
⊢ ∃ z ∈ ⁅J, N⁆, ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x₁ hx₁) : L), (↑n : M)⁆ + z = m
have 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
Tactic: use ⁅((⟨x₂, hx₂⟩ : J) : L), (n : N)⁆
-- 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 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⁆ ∧
    ⁅(↑(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
have h₁ : ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ J) x₂ hx₂) : L), (↑n : M)⁆ ∈ ⁅J, 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 : 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 ∈ 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
have 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
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'⁆ ≤ ⁅I, N⁆ ⊓ ⁅I, N'⁆
have rw : ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
I : LieIdeal R L
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have left : ⁅I, N ⊓ N'⁆ ≤ ⁅I, 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 ⊓ N'⁆ ≤ ⁅I, N⁆
⊢ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N⁆ ∧ ⁅I, N ⊓ N'⁆ ≤ ⁅I, N'⁆
have right : ⁅I, N ⊓ N'⁆ ≤ ⁅I, 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 ⊓ N'⁆ ≤ ⁅I, 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 ⊓ N'⁆ ≤ ⁅I, N'⁆
have right : N ⊓ N' ≤ N'
Tactic: apply mono_lie_right