case zero
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
⊢ I ^ Nat.zero ≤ J ^ Nat.zero

case succ
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ Nat.succ n✝ ≤ J ^ Nat.succ n✝
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n
induction' n with _ hn
no goals
case zero
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
⊢ I ^ Nat.zero ≤ J ^ Nat.zero
rw [pow_zero, pow_zero]
case succ
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I * I ^ n✝ ≤ J * J ^ n✝
case succ
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ Nat.succ n✝ ≤ J ^ Nat.succ n✝
rw [pow_succ, pow_succ]
no goals
case succ
R : Type u
ι : Type ?u.295460
inst✝ : CommSemiring R
I✝ J✝ K L I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I * I ^ n✝ ≤ J * J ^ n✝
exact Ideal.mul_mono e hn