-- Mathlib/Dynamics/Ergodic/Conservative.lean
theorem ae_frequently_mem_of_mem_nhds [TopologicalSpace α] [SecondCountableTopology α]
    [OpensMeasurableSpace α] {f : α → α} {μ : Measure α} (h : Conservative f μ) :
    ∀ᵐ x ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ n in atTop, f^[n] x ∈ s

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
exact (hx o hoS hxo).mono fun n hn => hos hn

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ i ∈ countableBasis α, x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
o : Set α
hoS : o ∈ countableBasis α
hxo : x ∈ o
hos : o ⊆ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := fun s hs =>
  h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).nullMeasurableSet

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ s ∈ countableBasis α, ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s