case zero
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
k : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ ucs Nat.zero N₁ ≤ ucs Nat.zero N₂

case succ
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
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (Nat.succ k) N₁ ≤ ucs (Nat.succ k) 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
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂
induction' k with k ih
case succ
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
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ normalizer (ucs k N₁) ≤ normalizer (ucs k N₂)
case succ
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
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (Nat.succ k) N₁ ≤ ucs (Nat.succ k) N₂
simp only [ucs_succ]
no goals
case succ
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
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ normalizer (ucs k N₁) ≤ normalizer (ucs k N₂)
apply monotone_normalizer ih
no goals
case zero
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
k : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ ucs Nat.zero N₁ ≤ ucs Nat.zero N₂
simpa