R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'
have aux : ∀ {x : L} {m}, m ∈ (N ⊔ N' : Submodule R M) → ⁅x, m⁆ ∈ (N ⊔ N' : Submodule R M) := by
  simp only [Submodule.mem_sup]
  rintro x m ⟨y, hy, z, hz, rfl⟩
  refine' ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩
case refine'_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ (let src := ↑N ⊔ ↑N';
      {
        toSubmodule :=
          { toAddSubmonoid := src.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
        lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) ∈
      {x | N ≤ x ∧ N' ≤ x} ∧
    ↑(let src := ↑N ⊔ ↑N';
        {
          toSubmodule :=
            { toAddSubmonoid := src.toAddSubmonoid,
              smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
          lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) =
      ↑N ⊔ ↑N'

case refine'_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ⊔ ↑N' ≤ ↑(N ⊔ N')
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'
refine' le_antisymm (sInf_le ⟨{ (N ⊔ N' : Submodule R M) with lie_mem := aux }, _⟩) _
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ∀ {x : L} {m : M}, (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = m) → ∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = ⁅x, m⁆
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
simp only [Submodule.mem_sup]
case intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : L
y : M
hy : y ∈ ↑N
z : M
hz : z ∈ ↑N'
⊢ ∃ y_1, y_1 ∈ ↑N ∧ ∃ z_1, z_1 ∈ ↑N' ∧ y_1 + z_1 = ⁅x, y + z⁆
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
⊢ ∀ {x : L} {m : M}, (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = m) → ∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = ⁅x, m⁆
rintro x m ⟨y, hy, z, hz, rfl⟩
no goals
case intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
x : L
y : M
hy : y ∈ ↑N
z : M
hz : z ∈ ↑N'
⊢ ∃ y_1, y_1 ∈ ↑N ∧ ∃ z_1, z_1 ∈ ↑N' ∧ y_1 + z_1 = ⁅x, y + z⁆
refine' ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩
case refine'_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) } ∧
    ↑N' ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
case refine'_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ (let src := ↑N ⊔ ↑N';
      {
        toSubmodule :=
          { toAddSubmonoid := src.toAddSubmonoid,
            smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
        lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) ∈
      {x | N ≤ x ∧ N' ≤ x} ∧
    ↑(let src := ↑N ⊔ ↑N';
        {
          toSubmodule :=
            { toAddSubmonoid := src.toAddSubmonoid,
              smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ src.carrier → c • x ∈ src.carrier) },
          lie_mem := (_ : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N') }) =
      ↑N ⊔ ↑N'
simp only [← coeSubmodule_le_coeSubmodule, mem_setOf_eq, and_true_iff]
no goals
case refine'_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) } ∧
    ↑N' ≤
      { toAddSubmonoid := (↑N ⊔ ↑N').toAddSubmonoid,
        smul_mem' := (_ : ∀ (c : R) {x : M}, x ∈ (↑N ⊔ ↑N').carrier → c • x ∈ (↑N ⊔ ↑N').carrier) }
constructor <;> intro x hx <;> simp [Submodule.mem_sup_left hx, hx, Submodule.mem_sup_right hx]
no goals
case refine'_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
aux : ∀ {x : L} {m : M}, m ∈ ↑N ⊔ ↑N' → ⁅x, m⁆ ∈ ↑N ⊔ ↑N'
⊢ ↑N ⊔ ↑N' ≤ ↑(N ⊔ N')
simp