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
S : Set (LieSubmodule R L M)
⊢ (⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p) = ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
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
S : Set (LieSubmodule R L M)
⊢ ↑(sInf S) = ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
rw [← LieSubmodule.coe_toSubmodule, sInf_coe_toSubmodule, Submodule.sInf_coe]
case h
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
S : Set (LieSubmodule R L M)
m : M
⊢ (m ∈ ⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p) ↔ m ∈ ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
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
S : Set (LieSubmodule R L M)
⊢ (⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p) = ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
ext m
no goals
case h
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
S : Set (LieSubmodule R L M)
m : M
⊢ (m ∈ ⋂ (p : Submodule R M) (_ : p ∈ {x | ∃ s, s ∈ S ∧ ↑s = x}), ↑p) ↔ m ∈ ⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s
simp only [mem_iInter, mem_setOf_eq, forall_apply_eq_imp_iff₂, exists_imp,
  and_imp, SetLike.mem_coe, mem_coeSubmodule]