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 : M
⊢ (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = x) ↔ ∃ y, y ∈ N ∧ ∃ z, z ∈ N' ∧ y + z = x
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 : M
⊢ x ∈ N ⊔ N' ↔ ∃ y, y ∈ N ∧ ∃ z, z ∈ N' ∧ y + z = x
rw [← mem_coeSubmodule, sup_coe_toSubmodule, Submodule.mem_sup]
no goals
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 : M
⊢ (∃ y, y ∈ ↑N ∧ ∃ z, z ∈ ↑N' ∧ y + z = x) ↔ ∃ y, y ∈ N ∧ ∃ z, z ∈ N' ∧ y + z = x
exact Iff.rfl