awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
mp :
  ∀ (y : ↥𝒪[K]) (hy : y ∈ t) (hy' : dist x y < ‖p‖),
    Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K])) Set.univ
        (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x) →
      Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K]))
        ((⇑(IsLocalRing.residue ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) '' t)
        (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x)
⊢ Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K])) Set.univ
      (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x) →
    Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K]))
      ((⇑(IsLocalRing.residue ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) '' t)
      (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x)

Tactic:
obtain ⟨y, hy, hy'⟩ := ht'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
mp :
  ∃ x_1 ∈ t,
    Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) x_1 :
        IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
        HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))
⊢ Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K])) Set.univ
      (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x) →
    Membership.mem (γ := Set (IsLocalRing.ResidueField ↥𝒪[K]))
      ((⇑(IsLocalRing.residue ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) '' t)
      (Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K])) : ↥𝒪[K] → ↥𝒪[K] → Prop) x)

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Set.mem_univ,
      IsLocalRing.residue, Set.mem_image, true_implies]

Premises used: IsLocalRing.residue, Set.mem_image, true_implies, Set.mem_univ, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.quot_mk_eq_mk
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
⊢ ∃ x_1 ∈ t,
    Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) x_1 :
        IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
        HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))

Tactic:
⟨y, hy, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
mp :
  Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) y :
      IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
      HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))
⊢ ∃ x_1 ∈ t,
    Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) x_1 :
        IsLocalRing.ResidueField ↥𝒪[K])
      ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
        HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))

Tactic:
refine ⟨y, hy, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
⊢ Eq (α := HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) 𝓂[K])
    ((Ideal.Quotient.mk 𝓂[K] : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ 𝓂[K]) y : HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) 𝓂[K])
    ((Ideal.Quotient.mk 𝓂[K] : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ 𝓂[K]) x : HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) 𝓂[K])

Tactic:
(Ideal.Quotient.mk_eq_mk_iff_sub_mem (I := 𝓂[K]) y x).mpr
        _

Premises used: Iff.mpr, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
mp : Membership.mem (γ := Ideal ↥𝒪[K]) 𝓂[K] (y - x)
⊢ Eq (α := IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) y :
      IsLocalRing.ResidueField ↥𝒪[K])
    ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K]) : (a : ↥𝒪[K]) → ↥𝒪[K] ⧸ IsLocalRing.maximalIdeal ↥𝒪[K]) x :
      HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) (IsLocalRing.maximalIdeal ↥𝒪[K]))

Tactic:
convert!
      (Ideal.Quotient.mk_eq_mk_iff_sub_mem (I := 𝓂[K]) y x).mpr
        _

Premises used: Iff.mpr, Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
mp :
  Membership.mem (γ := Set ↥𝒪[K])
    {y : ↥(Valuation.integer v) |
      LE.le.{u_2} (α := Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) y : K) : Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) p : K) : Γ₀)}
    (y - x)
⊢ Membership.mem (γ := Ideal ↥𝒪[K]) 𝓂[K] (y - x)

Tactic:
rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
      (Valuation.integer.integers _).coe_span_singleton_eq_setOf_le_v_algebraMap]

Premises used: Valuation.integer.integers, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, SetLike.mem_coe, Irreducible.maximalIdeal_eq, Valued.maximalIdeal
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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‖
⊢ dist y x < ‖p‖

Tactic:
rw [dist_comm] at hy'

Premises used: dist_comm
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) 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 y x < ‖p‖
⊢ Membership.mem (γ := Set ↥𝒪[K])
    {y : ↥(Valuation.integer v) |
      LE.le.{u_2} (α := Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) y : K) : Γ₀)
        ((v : (a : K) → Γ₀) ((algebraMap (↥(Valuation.integer v)) K : (a : ↥v.integer) → K) p : K) : Γ₀)}
    (y - x)

Tactic:
simpa [dist_eq_norm] using hy'.le

Premises used: dist_eq_norm, LT.lt.le
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
mpr : ∀ ε > 0, ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ

Tactic:
rw [Metric.totallyBounded_iff]

Premises used: Metric.totallyBounded_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
mpr :
  ∀ (p : ↥𝒪[K]) (hp : Irreducible p),
    ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)

Tactic:
obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]

Premises used: Valued.integer, Membership.mem, IsDiscreteValuationRing.exists_irreducible, Subtype
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
⊢ LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)

Tactic:
have hp' := Valuation.integer.v_irreducible_lt_one hp
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
⊢ ∃ (n : ℕ), ‖(↑p : K)‖ ^ n < ε

Tactic:
exists_pow_lt_of_lt_one εpos
      (toNormedField.norm_lt_one_iff.mpr hp')

Premises used: Iff.mpr, exists_pow_lt_of_lt_one, Valued.toNormedField.norm_lt_one_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
mpr :
  ∀ (n : ℕ) (hn : ‖(↑p : K)‖ ^ n < ε),
    ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖(p : K)‖ ^ n < ε := exists_pow_lt_of_lt_one εpos
      (toNormedField.norm_lt_one_iff.mpr hp')

Premises used: Iff.mpr, exists_pow_lt_of_lt_one, Subtype.val, Valued.toNormedField.norm_lt_one_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)

Tactic:
have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)

Tactic:
⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩

Premises used: Set.univ, Quotient.out, Set.toFinite, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
mpr :
  Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ
    (⋃ (y : ↥𝒪[K]),
      ⋃ (_ :
        Membership.mem (γ := Set ↥𝒪[K])
          (Set.image (α := Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))) Quotient.out
            Set.univ)
          y),
        Metric.ball y ε)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ε)

Tactic:
refine ⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
h :
  ∀ (x : ↥𝒪[K]),
    Membership.mem (γ := Set ↥𝒪[K])
        {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n} x ↔
      Membership.mem (γ := Set ↥𝒪[K]) (Metric.closedBall 0 (‖p‖ ^ n)) x
⊢ Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
x : ↥𝒪[K]
⊢ Membership.mem (γ := Set ↥𝒪[K])
      {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n} x ↔
    Membership.mem (γ := Set ↥𝒪[K]) (Metric.closedBall 0 (‖p‖ ^ n)) x

Tactic:
simp [← norm_pow]

Premises used: norm_pow
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))

Tactic:
have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) := by
      ext
      simp [← norm_pow]
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
this :
  Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))
mpr :
  ∀ (i : ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n),
    Metric.closedBall (Quotient.out i) (‖(↑p : K)‖ ^ n) ⊆
      ⋃ (y : Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))), Metric.ball y.out ε
⊢ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ
    (⋃ (y : ↥𝒪[K]),
      ⋃ (_ :
        Membership.mem (γ := Set ↥𝒪[K])
          (Set.image (α := Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))) Quotient.out
            Set.univ)
          y),
        Metric.ball y ε)

Tactic:
simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n), hp.maximalIdeal_pow_eq_setOf_le_v_coe_pow,
      this, AddSubgroupClass.coe_norm, 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]

Premises used: Metric.vadd_closedBall, Set.image_univ, Set.mem_range, Set.iUnion_subset_iff, HPow.hPow, vadd_eq_add, Set.iUnion_exists, AddSubgroupClass.coe_norm, Ideal.univ_eq_iUnion_image_add, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, Valued.maximalIdeal, add_zero, Set.iUnion_iUnion_eq'
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
this :
  Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))
i : ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
⊢ Metric.closedBall (Quotient.out i) (‖(↑p : K)‖ ^ n) ⊆
    ⋃ (y : Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))), Metric.ball y.out ε

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

Premises used: le_rfl, Set.subset_iUnion_of_subset, Metric.closedBall_subset_ball, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : Finite.{u_1 + 1} 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : LT.lt.{u_2} (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) (1 : Γ₀)
n : ℕ
hn : ‖(↑p : K)‖ ^ n < ε
hF : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
this :
  Eq.{u_1 + 1} (α := Set ↥𝒪[K])
    {y : ↥𝒪[K] | (v : (a : K) → Γ₀) (↑y : K) ≤ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (↑p : K) : Γ₀) n}
    (Metric.closedBall 0 (‖p‖ ^ n))
i : ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
⊢ Metric.closedBall (Quotient.out i) (‖(↑p : K)‖ ^ n) ⊆
    ⋃ (y : Quotient (Submodule.quotientRel (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))), Metric.ball y.out ε

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

Premises used: le_rfl, Set.subset_iUnion_of_subset, Metric.closedBall_subset_ball, HasSubset.Subset.trans
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
val : LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
⊢ Nonempty.{u_2 + 1} (LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
val : ∀ (a b : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc a b).Finite
⊢ LocallyFiniteOrder (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ

Tactic:
refine LocallyFiniteOrder.ofFiniteIcc ?_

Premises used: LocallyFiniteOrder.ofFiniteIcc
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
inl : ∀ (hxy : y < x), (Set.Icc x y).Finite
inr : (Set.Icc y y).Finite
inr₁ : ∀ (hxy : x < y), (Set.Icc x y).Finite
⊢ (Set.Icc x y).Finite

Tactic:
rcases lt_trichotomy y x with hxy | rfl | hxy

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : y < x
inl : Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅
inl₁ : y < x
⊢ (Set.Icc x y).Finite

Tactic:
rw [Set.Icc_eq_empty_of_lt]

Premises used: Set.Icc_eq_empty_of_lt
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
Γ₀ : Type u_2
inst : Field K
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : Valued K Γ₀
hc : IsCompact (↑𝒪[K] : Set K)
this : ∀ (z : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ
hxy : y < x
⊢ Set.Finite.{u_2} (α := (↥(MonoidHom.mrange (F := Valuation K Γ₀) v))ˣ) ∅

Tactic:
Set.finite_empty

Premises used: Set.finite_empty