Theorem: Base.exists_cover (Ray/Misc/Continuation.lean)

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ ∃ c, closure s ⊆ ⋃ x ∈ c, Metric.ball (↑x) (b.r x)
Tactic:
refine b.compact.elim_finite_subcover (fun x : closure s ↦ Metric.ball (x : E) (b.r x))
  (fun _ ↦ isOpen_ball) ?_
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ closure s ⊆ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
⊢ closure s ⊆ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Tactic:
intro x m
State after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ x ∈ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i

State before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
α : Type
p : (E → α) → E → Prop
s : Set E
f : E → α
z : E
b : Base p s f
x : E
m : x ∈ closure s
⊢ x ∈ ⋃ i, (fun x => Metric.ball (↑x) (b.r x)) i
Tactic:
exact mem_iUnion_of_mem ⟨x, m⟩ (mem_ball_self (b.rp ⟨x, m⟩))
State after:
no goals