case h
R : Type u_2
L : Type u_3
M : Type u_1
M' : Type ?u.11866
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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ normalizer (N₁ ⊓ N₂) ↔ m✝ ∈ normalizer N₁ ⊓ normalizer N₂
R : Type u_2
L : Type u_3
M : Type u_1
M' : Type ?u.11866
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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
⊢ normalizer (N₁ ⊓ N₂) = normalizer N₁ ⊓ normalizer N₂
ext
no goals
case h
R : Type u_2
L : Type u_3
M : Type u_1
M' : Type ?u.11866
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
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : LieRingModule L M'
inst✝ : LieModule R L M'
N N₁ N₂ : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ normalizer (N₁ ⊓ N₂) ↔ m✝ ∈ normalizer N₁ ⊓ normalizer N₂
simp [← forall_and]