-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma totallyBounded_iff_finite_residueField [IsDiscreteValuationRing 𝒪[K]] :
    TotallyBounded (Set.univ (α := 𝒪[K])) ↔ Finite 𝓀[K]

Proof state:
case mpr.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : ‖p‖ < 1
n : ℕ
hn : ‖p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ Set.univ ⊆ ⋃ y ∈ Quotient.out '' Set.univ, Metric.ball y ε

Tactic:
simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n), hp.maximalIdeal_pow_eq_closedBall_pow,
  AddSubgroupClass.coe_norm, Set.image_add_left, preimage_add_closedBall, sub_neg_eq_add,
  zero_add, Set.image_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
  Set.iUnion_subset_iff, Metric.vadd_closedBall, vadd_eq_add, add_zero]

Result:
case mpr.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : ‖p‖ < 1
n : ℕ
hn : ‖p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ ∀ (i : ↥𝒪[K] ⧸ 𝓂[K] ^ n), Metric.closedBall (Quotient.out i) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Proof state:
case mp.intro.intro.intro.mk.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ 𝓂[K]

Tactic:
rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
  coe_span_singleton_eq_closedBall]

Result:
case mp.intro.intro.intro.mk.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ Metric.closedBall 0 ‖p‖

Proof state:
case mp
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ → Finite 𝓀[K]

Tactic:
intro H

Result:
case mp
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
⊢ Finite 𝓀[K]

Proof state:
case mpr.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : ‖p‖ < 1
n : ℕ
hn : ‖p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ ∀ (i : ↥𝒪[K] ⧸ 𝓂[K] ^ n), Metric.closedBall (Quotient.out i) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Tactic:
intro

Result:
case mpr.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : ‖p‖ < 1
n : ℕ
hn : ‖p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
i✝ : ↥𝒪[K] ⧸ 𝓂[K] ^ n
⊢ Metric.closedBall (Quotient.out i✝) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Proof state:
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ ↔ Finite 𝓀[K]

Tactic:
constructor

Result:
case mp
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ → Finite 𝓀[K]

case mpr
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ Finite 𝓀[K] → TotallyBounded Set.univ

Proof state:
case mp.intro.intro.intro.mk
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
ht' : x ∈ ⋃ y ∈ t, Metric.ball y ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Tactic:
simp only [Set.mem_iUnion, Metric.mem_ball, exists_prop] at ht'

Result:
case mp.intro.intro.intro.mk
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
ht' : ∃ i ∈ t, dist x i < ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Proof state:
case mp.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
this : ∃ t ⊆ Set.univ, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ‖p‖
⊢ Finite 𝓀[K]

Tactic:
simp only [Set.subset_univ, Set.univ_subset_iff, true_and] at this

Result:
case mp.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
this : ∃ t, t.Finite ∧ ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Proof state:
case mpr.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : ‖p‖ < 1
n : ℕ
hn : ‖p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
i✝ : ↥𝒪[K] ⧸ 𝓂[K] ^ n
⊢ Metric.closedBall (Quotient.out i✝) (‖↑p‖ ^ n) ⊆ ⋃ y, Metric.ball y.out ε

Tactic:
exact (Metric.closedBall_subset_ball hn).trans (Set.subset_iUnion_of_subset _ le_rfl)

Result:
no goals

Proof state:
case mp.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
this : ∃ t, t.Finite ∧ ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Tactic:
obtain ⟨t, ht, ht'⟩ := this

Result:
case mp.intro.intro.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : ⋃ y ∈ t, Metric.ball y ‖p‖ = Set.univ
⊢ Finite 𝓀[K]

Proof state:
case mp.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
⊢ Finite 𝓀[K]

Tactic:
have := Metric.finite_approx_of_totallyBounded H ‖p‖ (norm_pos_iff.mpr hp.ne_zero)

Result:
case mp.intro
K : Type u_2
inst✝² : NontriviallyNormedField K
inst✝¹ : IsUltrametricDist K
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
this : ∃ t ⊆ Set.univ, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ‖p‖
⊢ Finite 𝓀[K]