awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
h₁ :
  ∀ (x : Prod.{u_1, u_3} (Set α) ι) (x_1 : α →ᵤ[𝔖] G),
    (∀ x_2 ∈ x.1, Membership.mem (α := G) (b x.2) ((toFun 𝔖 : (a : α →ᵤ[𝔖] G) → α → G) x_1 x_2 : G)) ↔
      Membership.mem (γ := Set ((α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G)))
        (UniformOnFun.gen 𝔖 x.1 {x_2 : G × G | x_2.1 / x_2.2 ∈ b x.2}) (x_1, 1)
⊢ HasBasis (α := α →ᵤ[𝔖] G) (𝓝 1) (fun (Si : Prod.{u_1, u_3} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2)
    fun (Si : Prod.{u_1, u_3} (Set α) ι) ↦
    {f : α →ᵤ[𝔖] G | ∀ x ∈ Si.1, Membership.mem (α := G) (b Si.2) ((toFun 𝔖 : (a : α →ᵤ[𝔖] G) → α → G) f x : G)}

Tactic:
convert!
    UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
      h.uniformity_of_nhds_one_swapped

Premises used: UniformOnFun.hasBasis_nhds_of_basis, Filter.HasBasis.uniformity_of_nhds_one_swapped, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
x : Prod.{u_1, u_3} (Set α) ι
x_1 : α →ᵤ[𝔖] G
⊢ (∀ x_2 ∈ x.1, Membership.mem (α := G) (b x.2) ((toFun 𝔖 : (a : α →ᵤ[𝔖] G) → α → G) x_1 x_2 : G)) ↔
    Membership.mem (γ := Set ((α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G))) (UniformOnFun.gen 𝔖 x.1 {x_2 : G × G | x_2.1 / x_2.2 ∈ b x.2})
      (x_1, 1)

Tactic:
simp [UniformOnFun.gen]

Premises used: UniformOnFun.gen
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
G : Type u_2
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
⊢ HasBasis (α := α →ᵤ[𝔖] G) (𝓝 1)
    (fun (SV : Prod.{u_1, u_2} (Set α) (Set G)) ↦ SV.1 ∈ 𝔖 ∧ Membership.mem (γ := Filter G) (𝓝 1) SV.2)
    fun (SV : Prod.{u_1, u_2} (Set α) (Set G)) ↦ {f : α →ᵤ[𝔖] G | ∀ x ∈ SV.1, f x ∈ SV.2}

Tactic:
UniformOnFun.hasBasis_nhds_one_of_basis 𝔖 h𝔖₁ h𝔖₂ (basis_sets _)

Premises used: Set.Mem, setOf, Filter.basis_sets, UniformOnFun.hasBasis_nhds_one_of_basis
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
ι : Type u_3
𝔖 : Set (Set α)
β : Type u_4
inst : CommMonoid β
f : ι → α → β
I : Finset ι
⊢ Eq (α := α →ᵤ[𝔖] β) ((ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) (∏ i ∈ I, f i))
    (∏ i ∈ I, (ofFun 𝔖 : (a : α → β) → α →ᵤ[𝔖] β) (f i))

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, UniformOnFun, rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
ι : Type u_3
𝔖 : Set (Set α)
β : Type u_4
inst : CommMonoid β
f : ι → α → β
I : Finset ι
⊢ Eq (α := α → β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (∏ i ∈ I, f i) : α → β)
    (∏ i ∈ I, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f i))

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, UniformOnFun, rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
ι : Type u_3
β : Type u_4
inst : CommMonoid β
f : ι → α → β
I : Finset ι
⊢ Eq (α := α →ᵤ β) ((ofFun : (a : α → β) → α →ᵤ β) (∏ i ∈ I, f i)) (∏ i ∈ I, (ofFun : (a : α → β) → α →ᵤ β) (f i))

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, UniformFun, rfl
-- Module: Mathlib.Topology.Algebra.UniformConvergence
Goal:
α : Type u_1
ι : Type u_3
β : Type u_4
inst : CommMonoid β
f : ι → α → β
I : Finset ι
⊢ Eq (α := α → β) ((toFun : (a : α →ᵤ β) → α → β) (∏ i ∈ I, f i) : α → β)
    (∏ i ∈ I, (toFun : (a : α →ᵤ β) → α → β) (f i))

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, UniformFun, rfl
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : K
⊢ Eq (α := ℝ≥0) (((Valued.v : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x : ℝ≥0)
    (((valuation : Valuation K ℝ≥0) : (a : K) → ℝ≥0) x : ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : K
⊢ Membership.mem (γ := Subring K) 𝒪[K] x ↔ ‖x‖ ≤ 1

Tactic:
simp [Valuation.mem_integer_iff, ← NNReal.coe_le_coe]

Premises used: Valuation.mem_integer_iff, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : ↥𝒪[K]
⊢ ‖x‖ ≤ 1

Tactic:
mem_iff.mp x.prop

Premises used: Subtype.prop, Iff.mp, Valued.integer.mem_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖(↑(↑u : ↥𝒪[K]) : K)‖ = 1

Tactic:
simpa [← NNReal.coe_inj] using
    (Valuation.integer.integers (NormedField.valuation (K := K))).valuation_unit u

Premises used: Valuation.integer.integers, Valuation.Integers.valuation_unit, NormedField.valuation, NNReal.coe_inj
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖(↑u : ↥𝒪[K])‖ = 1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
u : ↥𝒪[K]
⊢ IsUnit u ↔ ‖u‖ = 1

Tactic:
simpa [← NNReal.coe_inj] using
    (Valuation.integer.integers (NormedField.valuation (K := K))).isUnit_iff_valuation_eq_one

Premises used: Valuation.integer.integers, NormedField.valuation, Valuation.Integers.isUnit_iff_valuation_eq_one, NNReal.coe_inj
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ ‖ϖ‖ < 1

Tactic:
Valuation.integer.v_irreducible_lt_one h

Premises used: Valuation.integer.v_irreducible_lt_one
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ 0 < ‖ϖ‖

Tactic:
Valuation.integer.v_irreducible_pos h

Premises used: Valuation.integer.v_irreducible_pos
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : ↥𝒪[K]
⊢ (↑(Ideal.span {x}) : Set ↥𝒪[K]) = Metric.closedBall 0 ‖x‖

Tactic:
simp [Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Set.ext_iff, ← NNReal.coe_le_coe]

Premises used: Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Set.ext_iff, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
inst_2 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
⊢ (↑𝓂[K] : Set ↥𝒪[K]) = Metric.closedBall 0 ‖ϖ‖

Tactic:
simp [h.maximalIdeal_eq_setOf_le_v_coe, Set.ext_iff, ← NNReal.coe_le_coe]

Premises used: Irreducible.maximalIdeal_eq_setOf_le_v_coe, Set.ext_iff, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
inst_2 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
ϖ : ↥𝒪[K]
h : Irreducible ϖ
n : ℕ
⊢ (↑(HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n) : Set ↥𝒪[K]) = Metric.closedBall 0 (‖ϖ‖ ^ n)

Tactic:
simp [h.maximalIdeal_pow_eq_setOf_le_v_coe_pow, Set.ext_iff, ← NNReal.coe_le_coe]

Premises used: Set.ext_iff, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, NNReal.coe_le_coe
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
obtain : ∀ (x : K) (hx : 0 < ‖x‖) (hx' : ‖x‖ < 1), ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1

Tactic:
obtain ⟨x, hx, hx'⟩ := NormedField.exists_norm_lt_one K

Premises used: NormedField.exists_norm_lt_one
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : K
hx : 0 < ‖x‖
hx' : ‖x‖ < 1
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1

Tactic:
⟨⟨x, hx'.le⟩, ?_⟩

Premises used: LT.lt.le, Subtype.mk, Exists.intro
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : K
hx : 0 < ‖x‖
hx' : ‖x‖ < 1
refine :
  0 < ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x ⋯) : K)‖ ∧
    ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x ⋯) : K)‖ < 1
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1

Tactic:
refine ⟨⟨x, hx'.le⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
x : K
hx : 0 < ‖x‖
hx' : ‖x‖ < 1
⊢ 0 < ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x ⋯) : K)‖ ∧
    ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x ⋯) : K)‖ < 1

Tactic:
simpa [hx', Subtype.ext_iff] using hx

Premises used: Subtype.ext_iff
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖x‖ ∧ ‖x‖ < 1

Tactic:
exists_norm_coe_lt_one K

Premises used: Valued.integer.exists_norm_coe_lt_one
-- Module: Mathlib.Topology.Algebra.Valued.LocallyCompact
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖x‖₊ ∧ ‖x‖₊ < 1

Tactic:
exists_norm_coe_lt_one K

Premises used: Valued.integer.exists_norm_coe_lt_one
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
zero : Finite.{u_1 + 1} (HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) ⊤)
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) (β := ℕ) 𝓂[K] 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) ⊤)

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

Premises used: Valued.integer, Membership.mem, Subtype, Finite.of_fintype, HasQuotient.Quotient, Top.top
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) ⊤)

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

Premises used: Valued.integer, Membership.mem, Subtype, Finite.of_fintype, HasQuotient.Quotient, Top.top
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
ih : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ n ≤ n + 1

Tactic:
simp
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
ih : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
⊢ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1) ≤ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n

Tactic:
have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
ih : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
this : HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1) ≤ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
⊢ Finite.{u_1 + 1}
    (HasQuotient.Quotient (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)) (B :=
      Ideal (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)))
      (Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)))

Tactic:
replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
this : HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1) ≤ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
ih :
  Finite.{u_1 + 1}
    (HasQuotient.Quotient (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)) (B :=
      Ideal (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)))
      (Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)))
succ :
  Finite.{u_1 + 1}
    ↥(Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))

Tactic:
suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
this : HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1) ≤ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
ih :
  Finite.{u_1 + 1}
    (HasQuotient.Quotient (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)) (B :=
      Ideal (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)))
      (Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)))
⊢ Finite.{u_1 + 1}
    ↥(Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))

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

Premises used: Ideal.quotEquivPowQuotPowSuccEquiv, Finite.of_equiv, Equiv.trans, IsDiscreteValuationRing.not_a_field, Valued.maximalIdeal, Ideal.powQuotPowSuccEquivMapMkPowSuccPow, IsPrincipalIdealRing.principal
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
this : HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1) ≤ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n
ih :
  Finite.{u_1 + 1}
    (HasQuotient.Quotient (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)) (B :=
      Ideal (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1)))
      (Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)))
⊢ Finite.{u_1 + 1}
    ↥(Ideal.map (F := ↥𝒪[K] →+* ↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
        (Ideal.Quotient.mk (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))) (HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n))

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

Premises used: Ideal.quotEquivPowQuotPowSuccEquiv, Finite.of_equiv, Equiv.trans, IsDiscreteValuationRing.not_a_field, Valued.maximalIdeal, Ideal.powQuotPowSuccEquivMapMkPowSuccPow, IsPrincipalIdealRing.principal
-- 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 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
h : Finite.{u_1 + 1} 𝓀[K]
n : ℕ
zero : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) (β := ℕ) 𝓂[K] 0)
succ :
  ∀ (n : ℕ) (ih : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)),
    Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[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
      .of_ideal_quotient (.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))

Premises used: Ideal.quotEquivPowQuotPowSuccEquiv, Finite.of_equiv, Ideal.one_eq_top, Valued.integer, Equiv.trans, Membership.mem, Subtype, IsDiscreteValuationRing.not_a_field, Finite.of_fintype, pow_zero, HasQuotient.Quotient, Valued.maximalIdeal, Top.top, Ideal.powQuotPowSuccEquivMapMkPowSuccPow, IsPrincipalIdealRing.principal
-- 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]
mp : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ → Finite.{u_1 + 1} 𝓀[K]
mpr : Finite.{u_1 + 1} 𝓀[K] → TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ↔ Finite.{u_1 + 1} 𝓀[K]

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 Γ₀
inst_3 : Valuation.RankOne.{u_1, u_2} (R := K) v
inst_4 : IsDiscreteValuationRing.{u_1} ↥𝒪[K]
H : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
mp : ∀ (p : ↥𝒪[K]) (hp : Irreducible p), Finite.{u_1 + 1} 𝓀[K]
⊢ Finite.{u_1 + 1} 𝓀[K]

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 : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
p : ↥𝒪[K]
hp : Irreducible p
⊢ ∃ t ⊆ Set.univ, t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ‖p‖)

Tactic:
have := Metric.finite_approx_of_totallyBounded H ‖p‖ (norm_pos_iff.mpr hp.ne_zero)
-- 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
this : ∃ t ⊆ Set.univ, t.Finite ∧ Subset.{u_1} (α := Set ↥𝒪[K]) Set.univ (⋃ y ∈ t, Metric.ball y ‖p‖)
⊢ ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ

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

Premises used: Set.univ_subset_iff, Set.subset_univ, true_and
-- 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
this : ∃ (t : Set ↥𝒪[K]), t.Finite ∧ Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ
mp :
  ∀ (t : Set ↥𝒪[K]) (ht : t.Finite) (ht' : Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ),
    Finite.{u_1 + 1} 𝓀[K]
⊢ Finite.{u_1 + 1} 𝓀[K]

Tactic:
obtain ⟨t, ht, ht'⟩ := this
-- 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
ht' : Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ
mp : Set.Finite.{u_1} (α := 𝓀[K]) Set.univ
⊢ Finite.{u_1 + 1} 𝓀[K]

Tactic:
rw [← Set.finite_univ_iff]

Premises used: Set.finite_univ_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 : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
ht' : Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ
⊢ Set.Finite.{u_1} (α := 𝓀[K]) Set.univ

Tactic:
(ht.image (IsLocalRing.residue _)).subset ?_

Premises used: IsLocalRing.residue, Set.Finite.subset, Set.Finite.image, DFunLike.coe
-- 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
ht' : Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ
mp :
  Subset (α := Set (IsLocalRing.ResidueField ↥𝒪[K])) Set.univ
    ((⇑(IsLocalRing.residue ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) '' t)
⊢ Set.Finite.{u_1} (α := 𝓀[K]) Set.univ

Tactic:
refine (ht.image (IsLocalRing.residue _)).subset ?_

Premises used: IsLocalRing.residue, Set.Finite.subset, Set.Finite.image, DFunLike.coe
-- 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
ht' : Eq.{u_1 + 1} (α := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) Set.univ
a : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
⊢ Membership.mem (γ := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) x

Tactic:
replace ht' := ht'.ge (Set.mem_univ x)
-- 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' : Membership.mem (γ := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) x
⊢ ∃ i ∈ t, dist x i < ‖p‖

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

Premises used: Set.mem_iUnion, exists_prop, Metric.mem_ball