case intro
R : Type u
ι : Type ?u.292952
inst✝ : CommSemiring R
I J K L : Ideal R
m n : ℕ
h : m ≤ n
k : ℕ
hk : n = m + k
⊢ I ^ n ≤ I ^ m
R : Type u
ι : Type ?u.292952
inst✝ : CommSemiring R
I J K L : Ideal R
m n : ℕ
h : m ≤ n
⊢ I ^ n ≤ I ^ m
cases' Nat.exists_eq_add_of_le h with k hk
case intro
R : Type u
ι : Type ?u.292952
inst✝ : CommSemiring R
I J K L : Ideal R
m n : ℕ
h : m ≤ n
k : ℕ
hk : n = m + k
⊢ I ^ m * I ^ k ≤ I ^ m
case intro
R : Type u
ι : Type ?u.292952
inst✝ : CommSemiring R
I J K L : Ideal R
m n : ℕ
h : m ≤ n
k : ℕ
hk : n = m + k
⊢ I ^ n ≤ I ^ m
rw [hk, pow_add]
no goals
case intro
R : Type u
ι : Type ?u.292952
inst✝ : CommSemiring R
I J K L : Ideal R
m n : ℕ
h : m ≤ n
k : ℕ
hk : n = m + k
⊢ I ^ m * I ^ k ≤ I ^ m
exact le_trans mul_le_inf inf_le_left