-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma finite_quotient_maximalIdeal_pow_of_finite_residueField [IsDiscreteValuationRing 𝒪[K]]
    (h : Finite 𝓀[K]) (n : ℕ) :
    Finite (𝒪[K] ⧸ 𝓂[K] ^ n)

Proof state:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
ih : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Tactic:
replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv

Result:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Proof state:
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)

Tactic:
induction n with
| zero =>
  simp only [pow_zero, Ideal.one_eq_top]
  exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)
| succ n ih =>
  have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
  replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
  suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
    Finite.of_finite_quot_finite_ideal
      (I := Ideal.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
  exact @Finite.of_equiv _ _ h
    ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
      (IsDiscreteValuationRing.not_a_field _) n).trans
      (Ideal.powQuotPowSuccEquivMapMkPowSuccPow _ n))

Result:
no goals

Proof state:
case zero
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]

Result:
case zero
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ ⊤)

Proof state:
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
ih : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ n ≤ n + 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite ↥(Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))

Tactic:
exact @Finite.of_equiv _ _ h
  ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
    (IsDiscreteValuationRing.not_a_field _) n).trans
    (Ideal.powQuotPowSuccEquivMapMkPowSuccPow _ n))

Result:
no goals

Proof state:
case zero
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ ⊤)

Tactic:
exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)

Result:
no goals

Proof state:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
ih : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Tactic:
have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)

Result:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
ih : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Proof state:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1))

Tactic:
suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
  Finite.of_finite_quot_finite_ideal
    (I := Ideal.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))

Result:
case succ
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
n : ℕ
this : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n
ih : Finite ((↥𝒪[K] ⧸ 𝓂[K] ^ (n + 1)) ⧸ Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))
⊢ Finite ↥(Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n))