awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have rcases : ∀ (l : ℤ) (hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))), ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
Tactic: rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have this₁ : m < l ∧ l < m + 1
Tactic: have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
⊢ ∃ (a_1 : ℤ), (fun (x : ℤ) ↦ a ^ x) a_1 = b
have inr : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
Tactic: suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty by
    rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
    have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
    lia
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
have inr : ∀ (hlt : b < a ^ (m - 1)), (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
Tactic: rcases hne.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
inr : ∀ (hlt : b < a ^ (m - 1)), (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
have inr₁ : ∀ (hlt : a ^ (m - 1) < b), (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
Tactic: rcases hne.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : b < a ^ (m - 1)
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
have inr : b * a * a < a ^ (m + 1)
Tactic: refine ⟨b * a * a, hm', ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
have h₁ : b * a ∈ Ioo (a ^ m) (a ^ (m + 1))
Tactic: use b * a
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Group (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : CommGroup G
inst_2 : LinearOrder G
inst_3 : IsOrderedMonoid G
inst_4 : OrderTopology G
a : G
h : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
hlt : a ^ (m - 1) < b
⊢ b * a ∈ Ioo (a ^ m) (a ^ (m + 1))
have h₁ : ∀ (hlt : a ^ m / a < b), a ^ m < b * a ∧ b < a ^ m
Tactic: simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformConvergence (goal)
Goal:
α : Type u_1
G : Type u_2
ι : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (α := α →ᵤ G) (𝓝 1) p fun (i : ι) ↦
    {f : α →ᵤ G | ∀ (x : α), Membership.mem (α := G) (b i) ((toFun : (a : α →ᵤ G) → α → G) f x : G)}
have h₁ : ∀ (x : ι) (x_1 : α →ᵤ G),
  (∀ (x_2 : α), Membership.mem (α := G) (b x) ((toFun : (a : α →ᵤ G) → α → G) x_1 x_2 : G)) ↔
    (1, x_1) ∈ UniformFun.gen α G {x_2 : G × G | x_2.2 / x_2.1 ∈ b x}
Tactic: convert! UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) h.uniformity_of_nhds_one
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformConvergence (goal)
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
⊢ 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)}
have 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)
Tactic: convert!
    UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
      h.uniformity_of_nhds_one_swapped
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
Goal:
K : Type u_1
inst : NontriviallyNormedField K
inst_1 : IsUltrametricDist K
⊢ ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1
have obtain : ∀ (x : K) (hx : 0 < ‖x‖) (hx' : ‖x‖ < 1), ∃ (x : ↥𝒪[K]), 0 < ‖(↑x : K)‖ ∧ ‖(↑x : K)‖ < 1
Tactic: obtain ⟨x, hx, hx'⟩ := NormedField.exists_norm_lt_one K
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
have refine : 0 < ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x sorry) : K)‖ ∧
  ‖(↑(Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subring K) 𝒪[K] x) x sorry) : K)‖ < 1
Tactic: refine ⟨⟨x, hx'.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) (β := ℕ) 𝓂[K] 0)
have zero : Finite.{u_1 + 1} (HasQuotient.Quotient ↥𝒪[K] (B := Ideal ↥𝒪[K]) ⊤)
Tactic: simp only [pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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)
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
have 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)))
Tactic: replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] (n + 1))
have 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))
Tactic: suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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 : ℕ
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
have zero : Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) (β := ℕ) 𝓂[K] 0)
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))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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)
⊢ Finite.{u_1 + 1} (↥𝒪[K] ⧸ HPow.hPow (α := Ideal ↥𝒪[K]) 𝓂[K] n)
have 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))
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))
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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]
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ↔ Finite.{u_1 + 1} 𝓀[K]
have mp : TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ → Finite.{u_1 + 1} 𝓀[K]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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]
⊢ TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ ↔ Finite.{u_1 + 1} 𝓀[K]
have mpr : Finite.{u_1 + 1} 𝓀[K] → TotallyBounded.{u_1} (α := ↥𝒪[K]) Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ Finite.{u_1 + 1} 𝓀[K]
have mp : ∀ (p : ↥𝒪[K]) (hp : Irreducible p), Finite.{u_1 + 1} 𝓀[K]
Tactic: obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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
⊢ Finite.{u_1 + 1} 𝓀[K]
have this : ∃ 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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‖)
⊢ Finite.{u_1 + 1} 𝓀[K]
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ Finite.{u_1 + 1} 𝓀[K]
have 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]
Tactic: obtain ⟨t, ht, ht'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
⊢ Finite.{u_1 + 1} 𝓀[K]
have mp : Set.Finite.{u_1} (α := 𝓀[K]) Set.univ
Tactic: rw [← Set.finite_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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
have mp : Subset (α := Set (IsLocalRing.ResidueField ↥𝒪[K])) Set.univ
  ((⇑(IsLocalRing.residue ↥𝒪[K]) : (a : ↥𝒪[K]) → IsLocalRing.ResidueField ↥𝒪[K]) '' t)
Tactic: refine (ht.image (IsLocalRing.residue _)).subset ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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 (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)
have ht'₁ : Membership.mem (γ := Set ↥𝒪[K]) (⋃ y ∈ t, Metric.ball y ‖p‖) x
Tactic: replace ht' := ht'.ge (Set.mem_univ x)
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (hypothesis)
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
⊢ 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)
have ht'₁ : ∃ i ∈ t, dist x i < ‖p‖
Tactic: simp only [Set.mem_iUnion, Metric.mem_ball, exists_prop] at ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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‖
⊢ 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)
have 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)
Tactic: obtain ⟨y, hy, hy'⟩ := ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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‖
⊢ 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)
have 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]))
Tactic: simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Set.mem_univ,
      IsLocalRing.residue, Set.mem_image, true_implies]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.LocallyCompact (goal)
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]))
have 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]))
Tactic: refine ⟨y, hy, ?_⟩