chore(Cauchy): drop Nonempty/Inhabited assumptions (#10871)

Use `haveI` to drop unneeded `Nonempty`/`Inhabited` assumptions.
leanprover-community · Feb 27, 2024 · 5d73e33 · 5d73e33
1 parent 65d37dc
commit 5d73e33
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 7 deletions.
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -477,14 +477,14 @@ theorem cauchySeq_tendsto_of_isComplete [Preorder β] {K : Set α} (h₁ : IsCom
     ⟨univ, univ_mem, by rwa [image_univ, range_subset_iff]⟩
 #align cauchy_seq_tendsto_of_is_complete cauchySeq_tendsto_of_isComplete
 
-theorem Cauchy.le_nhds_lim [CompleteSpace α] [Nonempty α] {f : Filter α} (hf : Cauchy f) :
-    f ≤ 𝓝 (lim f) :=
+theorem Cauchy.le_nhds_lim [CompleteSpace α] {f : Filter α} (hf : Cauchy f) :
+    haveI := hf.1.nonempty; f ≤ 𝓝 (lim f) :=
   _root_.le_nhds_lim (CompleteSpace.complete hf)
 set_option linter.uppercaseLean3 false in
 #align cauchy.le_nhds_Lim Cauchy.le_nhds_lim
 
-theorem CauchySeq.tendsto_limUnder [Preorder β] [CompleteSpace α] [Nonempty α] {u : β → α}
-    (h : CauchySeq u) : Tendsto u atTop (𝓝 <| limUnder atTop u) :=
+theorem CauchySeq.tendsto_limUnder [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) :
+    haveI := h.1.nonempty; Tendsto u atTop (𝓝 <| limUnder atTop u) :=
   h.le_nhds_lim
 #align cauchy_seq.tendsto_lim CauchySeq.tendsto_limUnder
 

diff --git a/Mathlib/Topology/UniformSpace/Completion.lean b/Mathlib/Topology/UniformSpace/Completion.lean
@@ -281,9 +281,10 @@ end Extend
 
 end
 
-theorem cauchyFilter_eq {α : Type*} [Inhabited α] [UniformSpace α] [CompleteSpace α]
-    [SeparatedSpace α] {f g : CauchyFilter α} :
-    lim f.1 = lim g.1 ↔ (f, g) ∈ separationRel (CauchyFilter α) := by
+theorem cauchyFilter_eq {α : Type*} [UniformSpace α] [CompleteSpace α] [SeparatedSpace α]
+    {f g : CauchyFilter α} :
+    haveI := f.2.1.nonempty; lim f.1 = lim g.1 ↔ (f, g) ∈ separationRel (CauchyFilter α) := by
+  haveI := f.2.1.nonempty
   constructor
   · intro e s hs
     rcases CauchyFilter.mem_uniformity'.1 hs with ⟨t, tu, ts⟩