case intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
case intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
rcases hs r hr with ⟨k, fk, ks⟩
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
let u := k ∩ { y | ∃ x ∈ s, (x, y) ∈ r }
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
choose f hfs hfr using fun x : u => x.coe_prop.2
case intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ range f ⊆ s

case intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ Set.Finite (range f)

case intro.intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ s ⊆ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), {x | (x, y) ∈ U}
refine' ⟨range f, _, _, _⟩
no goals
case intro.intro.intro.intro.intro.refine'_1
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ range f ⊆ s
exact range_subset_iff.2 hfs
case intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
this : Fintype ↑u
⊢ Set.Finite (range f)
case intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ Set.Finite (range f)
haveI : Fintype u := (fk.inter_of_left _).fintype
no goals
case intro.intro.intro.intro.intro.refine'_2
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
this : Fintype ↑u
⊢ Set.Finite (range f)
exact finite_range f
case intro.intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
case intro.intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
⊢ s ⊆ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
intro x xs
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
case intro.intro.intro.intro.intro.refine'_3
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
obtain ⟨y, hy, xy⟩ := mem_iUnion₂.1 (ks xs)
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ range f), {x | (x, y) ∈ U}
rw [biUnion_range, mem_iUnion]
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
z : ↑u := { val := y, property := (_ : y ∈ k ∧ y ∈ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}) }
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}
set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩
no goals
case intro.intro.intro.intro.intro.refine'_3.intro.intro
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
hs : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : Set.Finite k
ks : s ⊆ ⋃ (y : α) (_ : y ∈ k), {x | (x, y) ∈ r}
u : Set α := k ∩ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}
f : ↑u → α
hfs : ∀ (x : ↑u), f x ∈ s
hfr : ∀ (x : ↑u), (f x, ↑x) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : x ∈ {x | (x, y) ∈ r}
z : ↑u := { val := y, property := (_ : y ∈ k ∧ y ∈ {y | ∃ x, x ∈ s ∧ (x, y) ∈ r}) }
⊢ ∃ i, x ∈ {x | (x, f i) ∈ U}
exact ⟨z, rU <| mem_compRel.2 ⟨y, xy, rs (hfr z)⟩⟩