R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
⊢ {y | ↑v y = ↑v x} ∈ 𝓝 x
rw [mem_nhds]
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
rcases Units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
use γ
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑v x} ⊆ {y | ↑v y = ↑v x}
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
rw [hx]
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
y : R
y_in : y ∈ {y | ↑v (y - x) < ↑v x}
⊢ y ∈ {y | ↑v y = ↑v x}
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑v x} ⊆ {y | ↑v y = ↑v x}
intro y y_in
no goals
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
y : R
y_in : y ∈ {y | ↑v (y - x) < ↑v x}
⊢ y ∈ {y | ↑v y = ↑v x}
exact Valuation.map_eq_of_sub_lt _ y_in