-- Mathlib/RingTheory/Ideal/Quotient/Index.lean
lemma Ideal.index_pow_le
    (s : Finset R) (hs : Ideal.span s = I) [Finite (R ⧸ I)] (n) :
    (I ^ n).toAddSubgroup.index ≤ I.toAddSubgroup.index ^ ∑ i ∈ Finset.range n, s.card ^ i

Proof state:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ (Submodule.toAddSubgroup (I ^ (n + 1))).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Tactic:
refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_

Result:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ (Submodule.toAddSubgroup (I ^ n)).index ^ s.card * (Submodule.toAddSubgroup I).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Proof state:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ (Submodule.toAddSubgroup (I ^ n)).index ^ s.card * (Submodule.toAddSubgroup I).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Tactic:
refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_

Result:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ ((Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i) ^ s.card * (Submodule.toAddSubgroup I).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
n : ℕ
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
⊢ (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i

Tactic:
induction n with
| zero =>
  simp
| succ n IH =>
  refine (Submodule.index_smul_le (I ^ n) s hs).trans ?_
  refine (Nat.mul_le_mul (Nat.pow_le_pow_left IH _) le_rfl).trans ?_
  rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
n : ℕ
IH : (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i
⊢ ((Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i) ^ s.card * (Submodule.toAddSubgroup I).index ≤
    (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range (n + 1), s.card ^ i

Tactic:
rw [← pow_mul, ← pow_succ, geom_sum_succ, mul_comm]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
⊢ (Submodule.toAddSubgroup (I ^ 0)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range 0, s.card ^ i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
n : ℕ
⊢ (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i

Tactic:
have := Ideal.finite_quotient_pow ⟨s, hs⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
s : Finset R
hs : span ↑s = I
inst✝ : Finite (R ⧸ I)
n : ℕ
this : ∀ (n : ℕ), Finite (R ⧸ I ^ n)
⊢ (Submodule.toAddSubgroup (I ^ n)).index ≤ (Submodule.toAddSubgroup I).index ^ ∑ i ∈ Finset.range n, s.card ^ i