[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i j : Γ₀ˣ), ∃ k, ltAddSubgroup v k ≤ ltAddSubgroup v i ⊓ ltAddSubgroup v j
[PROOFSTEP]
rintro γ₀ γ₁
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∃ k, ltAddSubgroup v k ≤ ltAddSubgroup v γ₀ ⊓ ltAddSubgroup v γ₁
[PROOFSTEP]
use min γ₀ γ₁
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ltAddSubgroup v (min γ₀ γ₁) ≤ ltAddSubgroup v γ₀ ⊓ ltAddSubgroup v γ₁
[PROOFSTEP]
simp [Valuation.ltAddSubgroup]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∀ (a : R), ↑v a < ↑γ₀ → ↑v a < ↑γ₁ → ↑v a < ↑γ₀
[PROOFSTEP]
tauto
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
cases' exists_square_le γ with γ₀ h
[GOAL]
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γ₀
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ↑(ltAddSubgroup v γ₀) * ↑(ltAddSubgroup v γ₀) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro - ⟨r, s, r_in, s_in, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r s : R
r_in : r ∈ ↑(ltAddSubgroup v γ₀)
s_in : s ∈ ↑(ltAddSubgroup v γ₀)
⊢ (fun x x_1 => x * x_1) r s ∈ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
calc
  (v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
  _ < γ₀ * γ₀ := (mul_lt_mul₀ r_in s_in)
  _ ≤ γ := by exact_mod_cast h
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r s : R
r_in : r ∈ ↑(ltAddSubgroup v γ₀)
s_in : s ∈ ↑(ltAddSubgroup v γ₀)
⊢ ↑γ₀ * ↑γ₀ ≤ ↑γ
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro x γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
[GOAL]
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use(1 : Γ₀ˣ)
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ↑(ltAddSubgroup v 1) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change v (x * y) < _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ ↑v (x * y) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, zero_mul]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ 0 < ↑γ
[PROOFSTEP]
exact Units.zero_lt γ
[GOAL]
case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γx⁻¹ * γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ↑(ltAddSubgroup v (γx⁻¹ * γ)) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change (v (x * y) : Γ₀) < γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v (x * y) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, mul_comm]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
rw [Units.val_mul, mul_comm] at vy_lt 
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑γ * ↑γx⁻¹
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro x γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
[GOAL]
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ↑(ltAddSubgroup v 1) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change v (y * x) < _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ ↑v (y * x) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, mul_zero]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ 0 < ↑γ
[PROOFSTEP]
exact Units.zero_lt γ
[GOAL]
case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γx⁻¹ * γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ↑(ltAddSubgroup v (γx⁻¹ * γ)) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change (v (y * x) : Γ₀) < γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v (y * x) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
rw [Units.val_mul, mul_comm] at vy_lt 
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑γ * ↑γx⁻¹
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
letI := @TopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
intro s
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
⊢ (∃ i, True ∧ ↑(ltAddSubgroup v i) ⊆ s) ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
exact exists_congr fun γ => by rw [true_and]; rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
γ : Γ₀ˣ
⊢ True ∧ ↑(ltAddSubgroup v γ) ⊆ s ↔ {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rw [true_and]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
γ : Γ₀ˣ
⊢ ↑(ltAddSubgroup v γ) ⊆ s ↔ {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (𝓝 0) (fun x => True) fun γ => {x | ↑v x < ↑γ}
[PROOFSTEP]
simp [Filter.hasBasis_iff, is_topological_valuation]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (uniformity R) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (Filter.comap (fun x => x.snd - x.fst) (𝓝 0)) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
[PROOFSTEP]
exact (hasBasis_nhds_zero R Γ₀).comap _
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ s
[PROOFSTEP]
simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
  ((hasBasis_nhds_zero R Γ₀).comap fun y => y - x).mem_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
simp only [mem_nhds, sub_zero]
[GOAL]
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
[PROOFSTEP]
rw [mem_nhds]
[GOAL]
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}
[PROOFSTEP]
rcases Units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩
[GOAL]
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}
[PROOFSTEP]
use γ
[GOAL]
case h
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}
[PROOFSTEP]
rw [hx]
[GOAL]
case h
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}
[PROOFSTEP]
intro y y_in
[GOAL]
case h
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}
[PROOFSTEP]
exact Valuation.map_eq_of_sub_lt _ y_in
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ Filter.NeBot F ∧ ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (Filter.NeBot F ∧
      ∀ (U : Set R),
        U ∈ RingFilterBasis.toAddGroupFilterBasis → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    Filter.NeBot F ∧ ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
apply and_congr Iff.rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R),
      U ∈ RingFilterBasis.toAddGroupFilterBasis → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) →
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
intro h γ
[GOAL]
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U
γ : Γ₀ˣ
⊢ ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis _)
[GOAL]
case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ) →
    ∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U
[PROOFSTEP]
rintro h - ⟨γ, rfl⟩
[GOAL]
case mpr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
γ : Γ₀ˣ
⊢ ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
exact h γ
