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) < ↑γ
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) < ↑γ
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
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) < ↑γ
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) < ↑γ
apply and_congr Iff.rfl
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) < ↑γ
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) < ↑γ
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
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) < ↑γ

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
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) < ↑γ
constructor
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) < ↑γ
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) < ↑γ
intro h γ
no goals
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) < ↑γ
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis _)
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 γ)
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
rintro h - ⟨γ, rfl⟩
no goals
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 γ)
exact h γ