Theorem: Base.yt (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
m : z ∈ b.t
⊢ z ∈ Metric.ball (↑(b.y m)) (b.r (b.y m))
Tactic:
simp only [Base.t, Base.y, mem_iUnion₂, mem_iUnion] at 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
m✝ : z ∈ b.t
m : ∃ i, ∃ (_ : i ∈ b.c), z ∈ Metric.ball (↑i) (b.r i)
⊢ z ∈ Metric.ball (↑(choose ⋯)) (b.r (choose ⋯))

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
m✝ : z ∈ b.t
m : ∃ i, ∃ (_ : i ∈ b.c), z ∈ Metric.ball (↑i) (b.r i)
⊢ z ∈ Metric.ball (↑(choose ⋯)) (b.r (choose ⋯))
Tactic:
exact choose_spec (choose_spec m)
State after:
no goals