awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
z : (↑u : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ u) y ⋯
⊢ Membership.mem (γ := Set α) {a : α | ∃ (i : (↑u : Type u)), (a, g i) ∈ U} x

Tactic:
⟨z, rU ⟨y, xy, rs (hgr z)⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
z : (↑u : Type u) := Subtype.mk (p := fun (x : α) ↦ x ∈ u) y ⋯
⊢ Membership.mem (γ := Set α) {a : α | ∃ (i : (↑u : Type u)), (a, g i) ∈ U} x

Tactic:
exact ⟨z, rU ⟨y, xy, rs (hgr z)⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
rw :
  ∀ (hs : (𝓟 s).TotallyBounded) {U : SetRel α α} (hU : U ∈ 𝓤 α), ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
rw [← Filter.totallyBounded_principal_iff] at hs

Premises used: Filter.totallyBounded_principal_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
simp_rw : ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U}

Tactic:
simp_rw [← SetRel.preimage_eq_biUnion]

Premises used: SetRel.preimage_eq_biUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t

Tactic:
hs.exists_subset_of_mem (Filter.mem_principal_self s) hU

Premises used: Filter.mem_principal_self, Set.Mem, setOf, Filter.TotallyBounded.exists_subset_of_mem, Set.Subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ U.preimage t

Tactic:
exact hs.exists_subset_of_mem (Filter.mem_principal_self s) hU

Premises used: Filter.mem_principal_self, Filter.TotallyBounded.exists_subset_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}

Tactic:
⟨fun H _ hd ↦ H.exists_subset hd, fun H d hd ↦ let ⟨t, _, ht⟩ := H d hd; ⟨t, ht⟩⟩

Premises used: setOf, Set.Finite, Membership.mem, Exists, Prod.mk, HasSubset.Subset, And, _private.0.totallyBounded_iff_subset.match_1, Iff.intro, Exists.intro, TotallyBounded.exists_subset, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
U : ι → SetRel α α
H : (𝓤 α).HasBasis p U
s : Set α
⊢ TotallyBounded s ↔ ∀ (i : ι), p i → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

Tactic:
H.forall_iff fun _ _ hUV h =>
    h.imp fun _ ht => ⟨ht.1, ht.2.trans <| iUnion₂_mono fun _ _ _ hy => hUV hy⟩

Premises used: TotallyBounded, setOf, Exists.imp, And.intro, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
U : ι → SetRel α α
H : (𝓤 α).HasBasis p U
f : Filter α
x x_1 : Set (α × α)
h_1 : x ⊆ x_1
h : ∃ (t : Set α), t.Finite ∧ SetRel.preimage x t ∈ f
x_2 : Set α
ht : x_2.Finite ∧ SetRel.preimage x x_2 ∈ f
⊢ SetRel.preimage x x_2 ⊆ SetRel.preimage x_1 x_2

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : ∀ V ∈ 𝓤 α, SetRel.IsSymm V → ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y V
V : SetRel α α
h_1 : V ∈ 𝓤 α ∧ V.IsSymm
left : V ∈ 𝓤 α
right : V.IsSymm
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ id V}

Tactic:
simpa only [ball_eq_of_symmetry] using h V ‹_› ‹_›

Premises used: UniformSpace.ball_eq_of_symmetry
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s₁ s₂ : Set α
hs : s₁ ⊆ s₂
h : TotallyBounded s₂
⊢ TotallyBounded s₁

Tactic:
fun d hd =>
  let ⟨t, ht₁, ht₂⟩ := h d hd
  ⟨t, ht₁, Subset.trans hs ht₂⟩

Premises used: TotallyBounded, Set.Subset.trans, setOf, Set.Finite, Membership.mem, Exists, Prod.mk, HasSubset.Subset, And, _private.0.TotallyBounded.subset.match_1, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
h : f ≤ g
hg : g.TotallyBounded
⊢ f.TotallyBounded

Tactic:
fun U hU => (hg U hU).imp fun _ => And.imp_right (@h _)

Premises used: Exists.imp, Filter.TotallyBounded, And.imp_right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
⊢ TotallyBounded.{u} (α := α) {x : α | ClusterPt x f}

Tactic:
uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV => ?_

Premises used: Iff.mpr, uniformity_hasBasis_closed, Filter.HasBasis.totallyBounded_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
refine :
  ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V),
    ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
⊢ TotallyBounded.{u} (α := α) {x : α | ClusterPt x f}

Tactic:
refine uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV => ?_

Premises used: Iff.mpr, uniformity_hasBasis_closed, Filter.HasBasis.totallyBounded_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
obtain :
  ∀ (t : Set α) (htf : t.Finite) (hst : V.preimage t ∈ f),
    ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})
⊢ ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})

Tactic:
obtain ⟨t, htf, hst⟩ := h V hV.1

Premises used: And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
⊢ ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})

Tactic:
⟨t, htf, fun x hx => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
refine :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x),
    Membership.mem (γ := Set α) (⋃ y ∈ t, {x : α | (x, y) ∈ id V}) x
⊢ ∃ (t : Set α), t.Finite ∧ Subset.{u} (α := Set α) {x : α | ClusterPt x f} (⋃ y ∈ t, {x : α | (x, y) ∈ id V})

Tactic:
refine ⟨t, htf, fun x hx => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x
rw : x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)
⊢ Membership.mem (γ := Set α) (⋃ y ∈ t, {x : α | (x, y) ∈ id V}) x

Tactic:
rw [← SetRel.preimage_eq_biUnion, id, ← (hV.2.relPreimage_of_finite htf).closure_eq]

Premises used: SetRel.preimage_eq_biUnion, IsClosed.closure_eq, id, And.right, IsClosed.relPreimage_of_finite
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)

Tactic:
hx.mem_closure_of_mem _ hst

Premises used: ClusterPt.mem_closure_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : Membership.mem (γ := Set α) {x : α | ClusterPt x f} x
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)

Tactic:
exact hx.mem_closure_of_mem _ hst

Premises used: ClusterPt.mem_closure_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
rw : TotallyBounded.{u} (α := α) {a : α | ClusterPt a (𝓟 s)}
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] s)

Tactic:
rw [closure_eq_cluster_pts]

Premises used: closure_eq_cluster_pts
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded.{u} (α := α) {a : α | ClusterPt a (𝓟 s)}

Tactic:
(Filter.totallyBounded_principal_iff.mpr h).totallyBounded_setOf_clusterPt

Premises used: Iff.mpr, Filter.totallyBounded_principal_iff, Filter.TotallyBounded.totallyBounded_setOf_clusterPt
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded.{u} (α := α) {a : α | ClusterPt a (𝓟 s)}

Tactic:
exact (Filter.totallyBounded_principal_iff.mpr h).totallyBounded_setOf_clusterPt

Premises used: Iff.mpr, Filter.totallyBounded_principal_iff, Filter.TotallyBounded.totallyBounded_setOf_clusterPt
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] s) ↔ TotallyBounded s

Tactic:
⟨fun h ↦ h.subset subset_closure, TotallyBounded.closure⟩

Premises used: TotallyBounded.subset, subset_closure, Iff.intro, TotallyBounded.closure
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ (i : ι), f i) ↔ ∀ (i : ι), (f i).TotallyBounded

Tactic:
⟨fun h i ↦ h.mono (le_iSup _ _), fun h U hU ↦ ?_⟩

Premises used: Filter.TotallyBounded.mono, le_iSup, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
refine :
  ∀ (h : ∀ (i : ι), (f i).TotallyBounded) (U : SetRel α α) (hU : U ∈ 𝓤 α),
    ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ (i : ι), f i) ↔ ∀ (i : ι), (f i).TotallyBounded

Tactic:
refine ⟨fun h i ↦ h.mono (le_iSup _ _), fun h U hU ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
choose :
  ∀ (t : ι → Set α) (htf : ∀ (x : ι), (t x).Finite) (ht : ∀ (x : ι), U.preimage (t x) ∈ f x),
    ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)
⊢ ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)

Tactic:
choose t htf ht using (h · U hU)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
⊢ ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)

Tactic:
⟨⋃ i, t i, finite_iUnion htf, ?_⟩

Premises used: Set.finite_iUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
refine : Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage (⋃ (i : ι), t i))
⊢ ∃ (t : Set α), t.Finite ∧ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage t)

Tactic:
refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), U.preimage (t x) ∈ f x
simp_rw :
  ∀ (ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))),
    LE.le.{u} (α := Filter α) (⨆ (i : ι), f i) (⨆ (x : ι), 𝓟 (U.preimage (t x)))
⊢ Membership.mem (γ := Filter α) (⨆ (i : ι), f i) (U.preimage (⋃ (i : ι), t i))

Tactic:
simp_rw [U.preimage_iUnion, ← le_principal_iff, ← iSup_principal] at ht ⊢

Premises used: Filter.le_principal_iff, SetRel.preimage_iUnion, Filter.iSup_principal
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
h₁ : ∀ (i : ι), f i ≤ 𝓟 (U.preimage (t i))
⊢ LE.le.{u} (α := Filter α) (⨆ (i : ι), f i) (⨆ (x : ι), 𝓟 (U.preimage (t x)))

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
f : ι → Filter α
h : ∀ (i : ι), (f i).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
t : ι → Set α
htf : ∀ (x : ι), (t x).Finite
ht : ∀ (x : ι), f x ≤ 𝓟 (U.preimage (t x))
i : ι
⊢ f i ≤ 𝓟 (U.preimage (t i))

Tactic:
apply ht
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
⊢ Finite.{u_1 + 1} (↑I : Type u_1)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : Filter.TotallyBounded.{u} (α := α) (⨆ (x : Subtype (Membership.mem I)), f (↑x : ι)) ↔ ∀ i ∈ I, (f i).TotallyBounded
rw₁ : (∀ (i : Subtype (Membership.mem I)), (f (↑i : ι)).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded
rw₂ rw₃ :
  (∀ (a : ι) (b : a ∈ I), (f (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι)).TotallyBounded) ↔
    ∀ i ∈ I, (f i).TotallyBounded
⊢ Filter.TotallyBounded.{u} (α := α) (⨆ i ∈ I, f i) ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]

Premises used: iSup_subtype', Filter.totallyBounded_iSup, Subtype.forall
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
rw : Filter.TotallyBounded.{u} (α := α) (⨆ a ∈ S, a) ↔ ∀ f ∈ S, f.TotallyBounded
rw₁ rw₂ : (∀ i ∈ S, i.TotallyBounded) ↔ ∀ f ∈ S, f.TotallyBounded
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded

Tactic:
rw [sSup_eq_iSup, totallyBounded_biSup hS]

Premises used: sSup_eq_iSup, Filter.totallyBounded_biSup
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst : Finite ι
s : ι → Set α
simp_rw : Filter.TotallyBounded.{u} (α := α) (𝓟 (⋃ (i : ι), s i)) ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded
simp_rw₁ : Filter.TotallyBounded.{u} (α := α) (⨆ (x : ι), 𝓟 (s x)) ↔ ∀ (i : ι), (𝓟 (s i)).TotallyBounded
⊢ TotallyBounded.{u} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), TotallyBounded (s i)

Tactic:
simp_rw [← Filter.totallyBounded_principal_iff, ← Filter.iSup_principal,
    Filter.totallyBounded_iSup]

Premises used: Filter.totallyBounded_principal_iff, Filter.totallyBounded_iSup, Filter.iSup_principal
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ Finite.{u_1 + 1} (↑I : Type u_1)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite.{u_1 + 1} (↑I : Type u_1)
rw : TotallyBounded.{u} (α := α) (⋃ (x : (↑I : Type u_1)), s (↑x : ι)) ↔ ∀ i ∈ I, TotallyBounded (s i)
rw₁ : (∀ (i : (↑I : Type u_1)), TotallyBounded (s (↑i : ι))) ↔ ∀ i ∈ I, TotallyBounded (s i)
rw₂ rw₃ :
  (∀ (a : ι) (b : a ∈ I), TotallyBounded (s (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι))) ↔
    ∀ i ∈ I, TotallyBounded (s i)
⊢ TotallyBounded.{u} (α := α) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]

Premises used: Subtype.forall, Set.biUnion_eq_iUnion, totallyBounded_iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
rw : TotallyBounded.{u} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, TotallyBounded s
rw₁ rw₂ : (∀ i ∈ S, TotallyBounded i) ↔ ∀ s ∈ S, TotallyBounded s
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

Premises used: totallyBounded_biUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : s.Finite
⊢ TotallyBounded s

Tactic:
fun _U hU ↦
  ⟨s, hs, fun _x hx ↦ mem_biUnion hx <| refl_mem_uniformity hU⟩

Premises used: TotallyBounded, refl_mem_uniformity, Set.mem_biUnion, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : s.Subsingleton
⊢ TotallyBounded s

Tactic:
hs.finite.totallyBounded

Premises used: Set.Finite.totallyBounded, Set.Subsingleton.finite
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
⊢ TotallyBounded (α := α) {a}

Tactic:
(finite_singleton a).totallyBounded

Premises used: Set.Finite.totallyBounded, Set.finite_singleton
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded.{u} (α := α) ∅

Tactic:
finite_empty.totallyBounded

Premises used: Set.finite_empty, Set.Finite.totallyBounded
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
rw : TotallyBounded.{u} (α := α) ∅
⊢ Filter.TotallyBounded.{u} (α := α) ⊥

Tactic:
rw [← principal_empty, totallyBounded_principal_iff]

Premises used: Filter.totallyBounded_principal_iff, Filter.principal_empty
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded.{u} (α := α) ∅

Tactic:
totallyBounded_empty

Premises used: totallyBounded_empty
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ TotallyBounded.{u} (α := α) ∅

Tactic:
exact totallyBounded_empty

Premises used: totallyBounded_empty
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
rw : (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
rw [union_eq_iUnion, totallyBounded_iUnion]

Premises used: totallyBounded_iUnion, Set.union_eq_iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ (∀ (i : Bool), TotallyBounded (bif i then s else t)) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : TotallyBounded s
ht : TotallyBounded t
⊢ TotallyBounded (s ∪ t)

Tactic:
totallyBounded_union.2 ⟨hs, ht⟩

Premises used: Iff.mpr, totallyBounded_union, And.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
simp_rw : TotallyBounded ({a} ∪ s) ↔ TotallyBounded s
simp_rw₁ : TotallyBounded (α := α) {a} ∧ TotallyBounded s ↔ TotallyBounded s
simp_rw₂ : True ∧ TotallyBounded s ↔ TotallyBounded s
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s

Tactic:
simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]

Premises used: Set.singleton_union, totallyBounded_union, totallyBounded_singleton, true_and
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
rw : (∀ (i : Bool), (bif i then f else g).TotallyBounded) ↔ f.TotallyBounded ∧ g.TotallyBounded
⊢ (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded

Tactic:
rw [sup_eq_iSup, totallyBounded_iSup]

Premises used: sup_eq_iSup, Filter.totallyBounded_iSup
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
⊢ (∀ (i : Bool), (bif i then f else g).TotallyBounded) ↔ f.TotallyBounded ∧ g.TotallyBounded

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
hf : f.TotallyBounded
hg : g.TotallyBounded
⊢ (f ⊔ g).TotallyBounded

Tactic:
totallyBounded_sup.2 ⟨hf, hg⟩

Premises used: Iff.mpr, Filter.totallyBounded_sup, And.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : α → β
g : Filter α
hg : g.TotallyBounded
hf : UniformContinuous f
t : SetRel β β
ht : t ∈ 𝓤 β
c : Set α
hfc : c.Finite
hct : SetRel.preimage ((fun (x : α × α) ↦ (f x.1, f x.2)) ⁻¹' t) c ∈ g
⊢ t.preimage (f '' c) ∈ Filter.map f g

Tactic:
simpa [SetRel.preimage]

Premises used: SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : α → β
s : Set α
hs : TotallyBounded s
hf : UniformContinuous f
simp : ∀ (hs : (𝓟 s).TotallyBounded), (map f (𝓟 s)).TotallyBounded
⊢ TotallyBounded (f '' s)

Tactic:
simp only [← Filter.totallyBounded_principal_iff, ← Filter.map_principal] at hs ⊢

Premises used: Filter.totallyBounded_principal_iff, Filter.map_principal
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : α → β
s : Set α
hf : UniformContinuous f
hs : (𝓟 s).TotallyBounded
⊢ (map f (𝓟 s)).TotallyBounded

Tactic:
hs.map hf

Premises used: Filter.TotallyBounded.map
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
f : α → β
s : Set α
hf : UniformContinuous f
hs : (𝓟 s).TotallyBounded
⊢ (map f (𝓟 s)).TotallyBounded

Tactic:
exact hs.map hf

Premises used: Filter.TotallyBounded.map