[GOAL]
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
[PROOFSTEP]
letI := B.uniformSpace
[GOAL]
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
[PROOFSTEP]
haveI := B.uniformAddGroup
[GOAL]
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
[PROOFSTEP]
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]]
[GOAL]
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
[PROOFSTEP]
constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this]; rwa [this]]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
case mp
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
[PROOFSTEP]
rintro ⟨h', h⟩
[GOAL]
case mpr
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
⊢ (NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U) → Cauchy F
[PROOFSTEP]
rintro ⟨h', h⟩
[GOAL]
case mp.intro
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
h' : NeBot F
h : F ×ˢ F ≤ uniformity G
⊢ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
refine' ⟨h', _⟩
[GOAL]
case mpr.intro
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
h' : NeBot F
h : ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F
[PROOFSTEP]
refine' ⟨h', _⟩
[GOAL]
case mp.intro
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
h' : NeBot F
h : F ×ˢ F ≤ uniformity G
⊢ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
rwa [← this]
[GOAL]
case mpr.intro
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
h' : NeBot F
h : ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ F ×ˢ F ≤ uniformity G
[PROOFSTEP]
rwa [this]
[GOAL]
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
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
[GOAL]
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
[PROOFSTEP]
change Tendsto _ _ _ ↔ _
[GOAL]
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
[PROOFSTEP]
simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_swap (_ ∈ _) G]
