case zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j : ℕ
⊢ I ^ Nat.zero • N F j ≤ N F (Nat.zero + j)

case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j n✝ : ℕ
ih : I ^ n✝ • N F j ≤ N F (n✝ + j)
⊢ I ^ Nat.succ n✝ • N F j ≤ N F (Nat.succ n✝ + j)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
i j : ℕ
⊢ I ^ i • N F j ≤ N F (i + j)
induction' i with _ ih
no goals
case zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j : ℕ
⊢ I ^ Nat.zero • N F j ≤ N F (Nat.zero + j)
simp
case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j n✝ : ℕ
ih : I ^ n✝ • N F j ≤ N F (n✝ + j)
⊢ I • I ^ n✝ • N F j ≤ N F (n✝ + j + 1)
case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j n✝ : ℕ
ih : I ^ n✝ • N F j ≤ N F (n✝ + j)
⊢ I ^ Nat.succ n✝ • N F j ≤ N F (Nat.succ n✝ + j)
rw [pow_succ, mul_smul, Nat.succ_eq_add_one, add_assoc, add_comm 1, ← add_assoc]
no goals
case succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
j n✝ : ℕ
ih : I ^ n✝ • N F j ≤ N F (n✝ + j)
⊢ I • I ^ n✝ • N F j ≤ N F (n✝ + j + 1)
exact (Submodule.smul_mono_right ih).trans (F.smul_le _)