Theorem: mem_iff_eventually_subset (RMT4/hurwitz.lean)

State before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∀ᶠ (t : ℝ) in 𝓝[>] 0, φ t ⊆ s
Tactic:
rw [(nhdsWithin_hasBasis nhds_basis_closedBall (Ioi (0 : ℝ))).eventually_iff]
State after:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s

State before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s
Tactic:
simp_rw [hp.mem_iff, ← exists_prop, mem_inter_iff, mem_closedBall_zero_iff]
State after:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ (∃ i, ∃ (_ : 0 < i), φ i ⊆ s) ↔ ∃ i, ∃ (_ : 0 < i), ∀ ⦃x : ℝ⦄, ‖x‖ ≤ i ∧ x ∈ Ioi 0 → φ x ⊆ s

State before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ (∃ i, ∃ (_ : 0 < i), φ i ⊆ s) ↔ ∃ i, ∃ (_ : 0 < i), ∀ ⦃x : ℝ⦄, ‖x‖ ≤ i ∧ x ∈ Ioi 0 → φ x ⊆ s
Tactic:
refine exists₂_congr (λ ε hε => ⟨λ h r h' => (hφ (le_of_abs_le h'.1)).trans h,
  λ h => h ⟨Eq.le (abs_eq_self.mpr hε.le), hε⟩⟩)
State after:
no goals