-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma coe_span_singleton_eq_closedBall (x : 𝒪[K]) :
    (Ideal.span {x} : Set 𝒪[K]) = Metric.closedBall 0 ‖x‖

Proof state:
case inr.h.mp.intro
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
z : ↥𝒪[K]
⊢ ‖↑(z * x)‖ ≤ ‖↑x‖

Tactic:
simpa using mul_le_mul_of_nonneg_right (norm_le_one z) (_root_.norm_nonneg x)

Result:
no goals

Proof state:
case inr.h.mpr.refine_1
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ↑y / ↑x ∈ 𝒪[K]

Tactic:
simpa [mem_iff] using div_le_one_of_le₀ h (_root_.norm_nonneg _)

Result:
no goals

Proof state:
case inr.h.mp
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ (∃ a, a * x = y) → ‖↑y‖ ≤ ‖↑x‖

Tactic:
rintro ⟨z, rfl⟩

Result:
case inr.h.mp.intro
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
z : ↥𝒪[K]
⊢ ‖↑(z * x)‖ ≤ ‖↑x‖

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ↑x ≠ 0

Tactic:
simpa using hx

Result:
no goals

Proof state:
case inr.h.mpr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ∃ a, a * x = y

Tactic:
refine ⟨⟨y / x, ?_⟩, ?_⟩

Result:
case inr.h.mpr.refine_1
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ↑y / ↑x ∈ 𝒪[K]

case inr.h.mpr.refine_2
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ⟨↑y / ↑x, ?inr.h.mpr.refine_1⟩ * x = y

Proof state:
case inr.h
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ (∃ a, a * x = y) ↔ ‖↑y‖ ≤ ‖↑x‖

Tactic:
constructor

Result:
case inr.h.mp
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ (∃ a, a * x = y) → ‖↑y‖ ≤ ‖↑x‖

case inr.h.mpr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ ‖↑y‖ ≤ ‖↑x‖ → ∃ a, a * x = y

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
⊢ ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖

Tactic:
rcases eq_or_ne x 0 with rfl|hx

Result:
case inl
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
⊢ ↑(Ideal.span {0}) = Metric.closedBall 0 ‖0‖

case inr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
⊢ ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖

Proof state:
case inr.h
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ Metric.closedBall 0 ‖x‖

Tactic:
simp only [SetLike.mem_coe, Ideal.mem_span_singleton', AddSubgroupClass.coe_norm,
  Metric.mem_closedBall, dist_zero_right]

Result:
case inr.h
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ (∃ a, a * x = y) ↔ ‖↑y‖ ≤ ‖↑x‖

Proof state:
case inr.h.mpr.refine_2
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ⟨↑y / ↑x, ⋯⟩ * x = y

Tactic:
simpa only [Subtype.ext_iff] using div_mul_cancel₀ (y : K) (by simpa using hx)

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
⊢ ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖

Tactic:
ext y

Result:
case inr.h
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ y ∈ ↑(Ideal.span {x}) ↔ y ∈ Metric.closedBall 0 ‖x‖

Proof state:
case inl
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
⊢ ↑(Ideal.span {0}) = Metric.closedBall 0 ‖0‖

Tactic:
simp [Set.singleton_zero, Ideal.span_zero]

Result:
no goals

Proof state:
case inr.h.mpr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
⊢ ‖↑y‖ ≤ ‖↑x‖ → ∃ a, a * x = y

Tactic:
intro h

Result:
case inr.h.mpr
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
hx : x ≠ 0
y : ↥𝒪[K]
h : ‖↑y‖ ≤ ‖↑x‖
⊢ ∃ a, a * x = y