G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this : UniformSpace G := AddGroupFilterBasis.uniformSpace B
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
letI := B.uniformSpace
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this : UniformSpace G := AddGroupFilterBasis.uniformSpace B
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
haveI := B.uniformAddGroup
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ (x) (_ : x ∈ M) (y) (_ : y ∈ M), y - x ∈ U by
  constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this]; rwa [this]]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ map (fun x => x.snd - x.fst) (F ×ˢ F) ≤ nhds 0 ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Tendsto (fun x => x.snd - x.fst) (F ×ˢ F) (nhds 0) ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ map (fun x => x.snd - x.fst) (F ×ˢ F) ≤ nhds 0 ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
change Tendsto _ _ _ ↔ _
no goals
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Tendsto (fun x => x.snd - x.fst) (F ×ˢ F) (nhds 0) ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_swap (_ ∈ _) G]
no goals
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this]; rwa [this]]