[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
⊢ ∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ¬∃ᶠ (m : ℕ) in atTop, ↑↑μ (s ∩ f^[m] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
simp only [not_frequently, eventually_atTop, Ne.def, Classical.not_not] at H
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
H : ∃ a, ∀ (b : ℕ), b ≥ a → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
rcases H with ⟨N, hN⟩
[GOAL]
case intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
induction' N with N ihN
[GOAL]
case intro.zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
apply h0
[GOAL]
case intro.zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.zero → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ ↑↑μ s = 0
[PROOFSTEP]
simpa using hN 0 le_rfl
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : (∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0) → False
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
rw [imp_false] at ihN
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
ihN : ¬∀ (b : ℕ), b ≥ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
⊢ False
[PROOFSTEP]
push_neg at ihN
[GOAL]
case intro.succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
ihN : ∃ b, b ≥ N ∧ ↑↑μ (s ∩ f^[b] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
rcases ihN with ⟨n, hn, hμn⟩
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
⊢ False
[PROOFSTEP]
set T := s ∩ ⋃ n ≥ N + 1, f^[n] ⁻¹' s
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
⊢ False
[PROOFSTEP]
have hT : MeasurableSet T := hs.inter (MeasurableSet.biUnion (to_countable _) fun _ _ => hf.measurable.iterate _ hs)
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ False
[PROOFSTEP]
have hμT : μ T = 0 := by
  convert (measure_biUnion_null_iff <| to_countable _).2 hN
  rw [← inter_iUnion₂]
  rfl
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ ↑↑μ T = 0
[PROOFSTEP]
convert (measure_biUnion_null_iff <| to_countable _).2 hN
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), s ∩ f^[i] ⁻¹' s
[PROOFSTEP]
rw [← inter_iUnion₂]
[GOAL]
case h.e'_2.h.e'_3
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
⊢ T = s ∩ ⋃ (i : ℕ) (_ : i ∈ fun i => Nat.le (Nat.succ N) i), f^[i] ⁻¹' s
[PROOFSTEP]
rfl
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ False
[PROOFSTEP]
have : μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0 := by rwa [measure_diff_null hμT]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
⊢ ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
[PROOFSTEP]
rwa [measure_diff_null hμT]
[GOAL]
case intro.succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
⊢ False
[PROOFSTEP]
rcases hf.exists_mem_image_mem ((hs.inter (hf.measurable.iterate n hs)).diff hT) this with
  ⟨x, ⟨⟨hxs, _⟩, hxT⟩, m, hm0, ⟨_, hxm⟩, _⟩
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ False
[PROOFSTEP]
refine' hxT ⟨hxs, mem_iUnion₂.2 ⟨n + m, _, _⟩⟩
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ n + m ≥ N + 1
[PROOFSTEP]
exact add_le_add hn (Nat.one_le_of_lt <| pos_iff_ne_zero.2 hm0)
[GOAL]
case intro.succ.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
h0 : ↑↑μ s ≠ 0
N✝ : ℕ
hN✝ : ∀ (b : ℕ), b ≥ N✝ → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
N : ℕ
hN : ∀ (b : ℕ), b ≥ Nat.succ N → ↑↑μ (s ∩ f^[b] ⁻¹' s) = 0
n : ℕ
hn : n ≥ N
hμn : ↑↑μ (s ∩ f^[n] ⁻¹' s) ≠ 0
T : Set α := s ∩ ⋃ (n : ℕ) (_ : n ≥ N + 1), f^[n] ⁻¹' s
hT : MeasurableSet T
hμT : ↑↑μ T = 0
this : ↑↑μ ((s ∩ f^[n] ⁻¹' s) \ T) ≠ 0
x : α
hxT : ¬x ∈ T
hxs : x ∈ s
right✝¹ : x ∈ f^[n] ⁻¹' s
m : ℕ
hm0 : m ≠ 0
right✝ : ¬f^[m] x ∈ T
left✝ : f^[m] x ∈ s
hxm : f^[m] x ∈ f^[n] ⁻¹' s
⊢ x ∈ f^[n + m] ⁻¹' s
[PROOFSTEP]
rwa [Set.mem_preimage, ← iterate_add_apply] at hxm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
[PROOFSTEP]
by_contra H
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ False
[PROOFSTEP]
have : MeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) :=
  by
  simp only [setOf_forall, ← compl_setOf]
  exact hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
[PROOFSTEP]
simp only [setOf_forall, ← compl_setOf]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
⊢ MeasurableSet (s ∩ ⋂ (i : ℕ) (_ : i ≥ n), {a | f^[i] a ∈ s}ᶜ)
[PROOFSTEP]
exact hs.inter (MeasurableSet.biInter (to_countable _) fun m _ => hf.measurable.iterate m hs.compl)
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
⊢ False
[PROOFSTEP]
rcases(hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
[GOAL]
case intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})) ≠ 0
⊢ False
[PROOFSTEP]
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
H : ¬↑↑μ {x | x ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} = 0
this : MeasurableSet (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})
m : ℕ
hmn : m > n
hm : ↑↑μ (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s} ∩ f^[m] ⁻¹' (s ∩ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s})) ≠ 0
x : α
left✝ : x ∈ s
hxn : x ∈ {x | ∀ (m : ℕ), m ≥ n → ¬f^[m] x ∈ s}
hxm : f^[m] x ∈ s
⊢ False
[PROOFSTEP]
exact hxn m hmn.lt.le hxm
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ i ∧ f^[b] a ∈ s
[PROOFSTEP]
intro n
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b, b ≥ n ∧ f^[b] a ∈ s
[PROOFSTEP]
filter_upwards [measure_zero_iff_ae_nmem.1 (hf.measure_mem_forall_ge_image_not_mem_eq_zero hs n)]
[GOAL]
case h
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ (m : ℕ), m ≥ n → ¬f^[m] a ∈ s) → a ∈ s → ∃ b, b ≥ n ∧ f^[b] a ∈ s
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
refine' ae_all_iff.2 fun k => _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
⊢ ∀ᵐ (a : α) ∂μ, f^[k] a ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] a ∈ s
[PROOFSTEP]
refine' (hf.ae_mem_imp_frequently_image_mem (hf.measurable.iterate k hs)).mono fun x hx hk => _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
rw [← map_add_atTop_eq_nat k, frequently_map]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
⊢ ∃ᶠ (a : ℕ) in atTop, f^[a + k] x ∈ s
[PROOFSTEP]
refine' (hx hk).mono fun n hn => _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : MeasurableSet s
k : ℕ
x : α
hx : x ∈ f^[k] ⁻¹' s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ f^[k] ⁻¹' s
hk : f^[k] x ∈ s
n : ℕ
hn : f^[n] x ∈ f^[k] ⁻¹' s
⊢ f^[n + k] x ∈ s
[PROOFSTEP]
rwa [add_comm, iterate_add_apply]
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
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).measurableSet
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∀ᵐ (x : α) ∂μ, ∀ (s : Set α), s ∈ 𝓝 x → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
refine' ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => _
[GOAL]
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ (i : Set α), i ∈ countableBasis α → x ∈ i → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ i
s : Set α
hs : s ∈ 𝓝 x
⊢ ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
[PROOFSTEP]
rcases(isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : MeasurableSpace α
f✝ : α → α
s✝ : Set α
μ✝ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : OpensMeasurableSpace α
f : α → α
μ : Measure α
h : Conservative f μ
this : ∀ (s : Set α), s ∈ countableBasis α → ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
x : α
hx : ∀ (i : Set α), 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
[PROOFSTEP]
exact (hx o hoS hxo).mono fun n hn => hos hn
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[n] μ
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
⊢ Conservative f^[Nat.zero] μ
[PROOFSTEP]
exact Conservative.id μ
[GOAL]
case succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
⊢ Conservative f^[Nat.succ n] μ
[PROOFSTEP]
refine' ⟨hf.1.iterate _, fun s hs hs0 => _⟩
[GOAL]
case succ
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rcases(hf.frequently_ae_mem_and_frequently_image_mem hs hs0).exists with
  ⟨x, _, hx⟩
    /- We take a point `x ∈ s` such that `f^[k] x ∈ s` for infinitely many values of `k`,
        then we choose two of these values `k < l` such that `k ≡ l [MOD (n + 1)]`.
        Then `f^[k] x ∈ s` and `f^[n + 1]^[(l - k) / (n + 1)] (f^[k] x) = f^[l] x ∈ s`. -/
[GOAL]
case succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rw [Nat.frequently_atTop_iff_infinite] at hx
[GOAL]
case succ.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
rcases Nat.exists_lt_modEq_of_infinite hx n.succ_pos with ⟨k, hk, l, hl, hkl, hn⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
set m := (l - k) / (n + 1)
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
have : (n + 1) * m = l - k := by
  apply Nat.mul_div_cancel'
  exact (Nat.modEq_iff_dvd' hkl.le).1 hn
[GOAL]
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ (n + 1) * m = l - k
[PROOFSTEP]
apply Nat.mul_div_cancel'
[GOAL]
case H
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
⊢ n + 1 ∣ l - k
[PROOFSTEP]
exact (Nat.modEq_iff_dvd' hkl.le).1 hn
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, f^[Nat.succ n]^[m] x ∈ s
[PROOFSTEP]
refine' ⟨f^[k] x, hk, m, _, _⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ m ≠ 0
[PROOFSTEP]
intro hm
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
hm : m = 0
⊢ False
[PROOFSTEP]
rw [hm, mul_zero, eq_comm, tsub_eq_zero_iff_le] at this
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : l ≤ k
hm : m = 0
⊢ False
[PROOFSTEP]
exact this.not_lt hkl
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ f^[Nat.succ n]^[m] (f^[k] x) ∈ s
[PROOFSTEP]
rwa [← iterate_mul, this, ← iterate_add_apply, tsub_add_cancel_of_le]
[GOAL]
case succ.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
α : Type u_2
inst✝ : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
hf : Conservative f μ
n : ℕ
s : Set α
hs : MeasurableSet s
hs0 : ↑↑μ s ≠ 0
x : α
left✝ : x ∈ s
hx : Set.Infinite {n | f^[n] x ∈ s}
k : ℕ
hk : k ∈ {n | f^[n] x ∈ s}
l : ℕ
hl : l ∈ {n | f^[n] x ∈ s}
hkl : k < l
hn : k ≡ l [MOD Nat.succ n]
m : ℕ := (l - k) / (n + 1)
this : (n + 1) * m = l - k
⊢ k ≤ l
[PROOFSTEP]
exact hkl.le


[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x => ϕ (m t) x) s ⊆ ω f₂ ϕ s
[PROOFSTEP]
refine' iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, _⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
rw [← image2_image_left]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ ((fun t => m t) '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')
[PROOFSTEP]
simp only [omegaLimit_def, mem_iInter, MapsTo]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ ∀ ⦃x : β⦄,
    (∀ (i : Set τ), i ∈ f → x ∈ closure (image2 ϕ i s)) → ∀ (i : Set τ), i ∈ f → gb x ∈ closure (image2 ϕ' i s')
[PROOFSTEP]
intro y hy u hu
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ (i : Set τ), i ∈ f → y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
⊢ gb y ∈ closure (image2 ϕ' u s')
[PROOFSTEP]
refine' map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_image2_iff.2 fun t ht x hx ↦ _)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ (i : Set τ), i ∈ f → y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x | (fun t => EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ gb (ϕ t x) ∈ image2 ϕ' u s'
[PROOFSTEP]
calc
  gb (ϕ t x) = ϕ' t (ga x) := ht.2 hx
  _ ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun t x => ϕ t (g x)) s
[PROOFSTEP]
simp only [omegaLimit, image2_image_right]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s ∩ ϕ t ⁻¹' n)
[PROOFSTEP]
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)) ↔
    ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
constructor
[GOAL]
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)) →
    ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
intro h _ hn _ hu
[GOAL]
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
⊢ ∃ x, x ∈ U✝ ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n✝)
[PROOFSTEP]
rcases h _ hu _ hn with ⟨_, _, _, _, ht, hx, hϕtx⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝² : β
left✝ : w✝² ∈ n✝
w✝¹ : τ
w✝ : α
ht : w✝¹ ∈ U✝
hx : w✝ ∈ s
hϕtx : ϕ w✝¹ w✝ = w✝²
⊢ ∃ x, x ∈ U✝ ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n✝)
[PROOFSTEP]
exact ⟨_, ht, _, hx, by rwa [mem_preimage, hϕtx]⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝² : β
left✝ : w✝² ∈ n✝
w✝¹ : τ
w✝ : α
ht : w✝¹ ∈ U✝
hx : w✝ ∈ s
hϕtx : ϕ w✝¹ w✝ = w✝²
⊢ w✝ ∈ ϕ w✝¹ ⁻¹' n✝
[PROOFSTEP]
rwa [mem_preimage, hϕtx]
[GOAL]
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)) →
    ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
[PROOFSTEP]
intro h _ hu _ hn
[GOAL]
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
⊢ Set.Nonempty (t✝ ∩ image2 ϕ i✝ s)
[PROOFSTEP]
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
[GOAL]
case mpr.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
w✝¹ : τ
ht : w✝¹ ∈ i✝
w✝ : α
hx : w✝ ∈ s
hϕtx : w✝ ∈ ϕ w✝¹ ⁻¹' t✝
⊢ Set.Nonempty (t✝ ∩ image2 ϕ i✝ s)
[PROOFSTEP]
exact ⟨_, hϕtx, _, _, ht, hx, rfl⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (ϕ t '' s ∩ n)
[PROOFSTEP]
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
[PROOFSTEP]
simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff, singleton_inter_nonempty, mem_preimage]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
⊢ ω f ϕ (s₁ ∪ s₂) = ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
ext y
[GOAL]
case h
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
constructor
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty, frequently_or_distrib]
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (n : Set β),
      n ∈ 𝓝 y → (∃ᶠ (x : τ) in f, Set.Nonempty (s₁ ∩ ϕ x ⁻¹' n)) ∨ ∃ᶠ (x : τ) in f, Set.Nonempty (s₂ ∩ ϕ x ⁻¹' n)) →
    (∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s₁ ∩ ϕ t ⁻¹' n)) ∨
      ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s₂ ∩ ϕ t ⁻¹' n)
[PROOFSTEP]
contrapose!
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ ((∃ n, n ∈ 𝓝 y ∧ ¬∃ᶠ (t : τ) in f, Set.Nonempty (s₁ ∩ ϕ t ⁻¹' n)) ∧
      ∃ n, n ∈ 𝓝 y ∧ ¬∃ᶠ (t : τ) in f, Set.Nonempty (s₂ ∩ ϕ t ⁻¹' n)) →
    ∃ n, n ∈ 𝓝 y ∧ (¬∃ᶠ (x : τ) in f, Set.Nonempty (s₁ ∩ ϕ x ⁻¹' n)) ∧ ¬∃ᶠ (x : τ) in f, Set.Nonempty (s₂ ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
simp only [not_frequently, not_nonempty_iff_eq_empty, ← subset_empty_iff]
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ ((∃ n, n ∈ 𝓝 y ∧ ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∃ n, n ∈ 𝓝 y ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅) →
    ∃ n, n ∈ 𝓝 y ∧ (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
[PROOFSTEP]
rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
⊢ ∃ n, n ∈ 𝓝 y ∧ (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
[PROOFSTEP]
refine' ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ _, h₂.mono fun t ↦ _⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro.refine'_1
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
case h.mp.intro.intro.intro.intro.intro.refine'_2
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
[PROOFSTEP]
exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_left _ _,
  Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_right _ _]
[GOAL]
case h.mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
[PROOFSTEP]
rintro (hy | hy)
[GOAL]
case h.mpr.inl
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₁
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)
case h.mpr.inr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₂
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)
[PROOFSTEP]
exacts [omegaLimit_mono_right _ _ (subset_union_left _ _) hy, omegaLimit_mono_right _ _ (subset_union_right _ _) hy]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ⋃ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
[PROOFSTEP]
rw [iUnion_subset_iff]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
[PROOFSTEP]
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
[PROOFSTEP]
rw [omegaLimit_eq_biInter_inter _ _ _ hv]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ (u : Set τ) (_ : u ∈ f), closure (image2 ϕ (u ∩ v) s) = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
[PROOFSTEP]
apply biInter_eq_iInter
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
rw [omegaLimit_eq_iInter]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
intro _ hx
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
[PROOFSTEP]
rw [mem_iInter] at hx
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
[PROOFSTEP]
exact hx ⟨u, hu⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v, v ∈ f ∧ closure (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
rcases hc₂ with ⟨v, hv₁, hv₂⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
let k := closure (image2 ϕ v s)
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hk : IsCompact (k \ n) := IsCompact.diff (isCompact_of_isClosed_subset hc₁ isClosed_closure hv₂) hn₁
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u :=
  by
  have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
  rw [this, diff_subset_comm, diff_iUnion]
  rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
  simp_rw [diff_compl]
  rw [← inter_iInter]
  exact Subset.trans (inter_subset_right _ _) hn₂
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
⊢ k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
[PROOFSTEP]
have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : ⋃ (u : Set τ) (_ : u ∈ f), j u = ⋃ (u : ↑f.sets), j ↑u
⊢ k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
[PROOFSTEP]
rw [this, diff_subset_comm, diff_iUnion]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : ⋃ (u : Set τ) (_ : u ∈ f), j u = ⋃ (u : ↑f.sets), j ↑u
⊢ ⋂ (i : ↑f.sets), k \ j ↑i ⊆ n
[PROOFSTEP]
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : ⋃ (u : Set τ) (_ : u ∈ f), j u = ⋃ (u : ↑f.sets), j ↑u
⊢ ⋂ (i : ↑f.sets), k \ j ↑i ⊆ n
[PROOFSTEP]
simp_rw [diff_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : ⋃ (u : Set τ) (_ : u ∈ f), j u = ⋃ (u : ↑f.sets), j ↑u
⊢ ⋂ (i : ↑f.sets), closure (image2 ϕ v s) ∩ closure (image2 ϕ (↑i ∩ v) s) ⊆ n
[PROOFSTEP]
rw [← inter_iInter]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : ⋃ (u : Set τ) (_ : u ∈ f), j u = ⋃ (u : ↑f.sets), j ↑u
⊢ closure (image2 ϕ v s) ∩ ⋂ (i : ↑f.sets), closure (image2 ϕ (↑i ∩ v) s) ⊆ n
[PROOFSTEP]
exact Subset.trans (inter_subset_right _ _) hn₂
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
let w := (⋂ u ∈ g, u) ∩ v
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hw₂ : w ∈ f := by simpa [*]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
⊢ w ∈ f
[PROOFSTEP]
simpa [*]
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ := by
  apply Subset.trans hg₃
  simp only [iUnion_subset_iff, compl_subset_compl]
  intros u hu
  mono
  refine' iInter_subset_of_subset u (iInter_subset_of_subset hu _)
  all_goals exact Subset.rfl
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ k \ n ⊆ (closure (image2 ϕ w s))ᶜ
[PROOFSTEP]
apply Subset.trans hg₃
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ⋃ (i : Set τ) (_ : i ∈ g), j i ⊆ (closure (image2 ϕ w s))ᶜ
[PROOFSTEP]
simp only [iUnion_subset_iff, compl_subset_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∀ (i : Set τ), i ∈ g → closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (i ∩ v) s)
[PROOFSTEP]
intros u hu
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (u ∩ v) s)
[PROOFSTEP]
mono
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ ⋂ (u : Set τ) (_ : u ∈ g), u ⊆ u
case h.hs.h₂
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v
case h.ht
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
[PROOFSTEP]
refine' iInter_subset_of_subset u (iInter_subset_of_subset hu _)
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u
case h.hs.h₂
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v
case h.ht
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
[PROOFSTEP]
all_goals exact Subset.rfl
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case h.hs.h₂
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case h.ht
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ :=
  by
  simp only [compl_subset_compl]
  exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
⊢ kᶜ ⊆ (closure (image2 ϕ w s))ᶜ
[PROOFSTEP]
simp only [compl_subset_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ v s)
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ
[PROOFSTEP]
rw [union_comm, ← inter_subset, diff_eq, inter_comm]
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
have hw : closure (image2 ϕ w s) ⊆ n := compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
hw : closure (image2 ϕ w s) ⊆ n
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
[PROOFSTEP]
exact ⟨_, hw₂, hw⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
[PROOFSTEP]
rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁ hc₂ hn₁ hn₂ with
  ⟨u, hu_mem, hu⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
[PROOFSTEP]
refine' mem_of_superset hu_mem fun t ht x hx ↦ _
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n
[PROOFSTEP]
exact hu (subset_closure <| mem_image2_of_mem ht hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
[PROOFSTEP]
rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ with ⟨u, hu_mem, hu⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
[PROOFSTEP]
refine' mem_of_superset hu_mem fun t ht x hx ↦ _
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v
[PROOFSTEP]
exact hu (subset_closure <| mem_image2_of_mem ht hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v, v ∈ f ∧ closure (image2 ϕ v s) ⊆ c
hs : Set.Nonempty s
⊢ Set.Nonempty (ω f ϕ s)
[PROOFSTEP]
rcases hc₂ with ⟨v, hv₁, hv₂⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (ω f ϕ s)
[PROOFSTEP]
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s))
[PROOFSTEP]
apply IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed
[GOAL]
case intro.intro.hZd
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => closure (image2 ϕ (↑i ∩ v) s)
[PROOFSTEP]
rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
[GOAL]
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z)
[PROOFSTEP]
use⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
[GOAL]
case h
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) }) ∧
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
[PROOFSTEP]
constructor
[GOAL]
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
[PROOFSTEP]
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑{ val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) } ⊆ ↑{ val := u₁, property := hu₁ }
[PROOFSTEP]
simp
[GOAL]
case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑{ val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) } ⊆ ↑{ val := u₂, property := hu₂ }
[PROOFSTEP]
simp
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), Set.Nonempty (closure (image2 ϕ (↑i ∩ v) s))
[PROOFSTEP]
intro u
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
[PROOFSTEP]
have hn : (image2 ϕ (u ∩ v) s).Nonempty := Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
hn : Set.Nonempty (image2 ϕ (↑u ∩ v) s)
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
[PROOFSTEP]
exact hn.mono subset_closure
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))
[PROOFSTEP]
intro
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure (image2 ϕ (↑i✝ ∩ v) s))
[PROOFSTEP]
apply isCompact_of_isClosed_subset hc₁ isClosed_closure
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ closure (image2 ϕ (↑i✝ ∩ v) s) ⊆ c
[PROOFSTEP]
calc
  _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
  _ ⊆ c := hv₂
[GOAL]
case intro.intro.hZcl
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed (closure (image2 ϕ (↑i ∩ v) s))
[PROOFSTEP]
exact fun _ ↦ isClosed_closure
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)
[PROOFSTEP]
refine' fun t ↦ MapsTo.mono_right _ (omegaLimit_subset_of_tendsto ϕ s (hf t))
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
t : τ
⊢ MapsTo (toFun ϕ t) (ω f ϕ.toFun s) (ω f (fun t_1 x => toFun ϕ ((fun x x_1 => x + x_1) t t_1) x) s)
[PROOFSTEP]
exact mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm) (continuous_const.flow ϕ continuous_id)
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f ϕ.toFun (toFun ϕ t '' s) ⊆ ω f ϕ.toFun s
[PROOFSTEP]
simp only [omegaLimit_image_eq, ← map_add]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => toFun ϕ (t_1 + t) x) s ⊆ ω f ϕ.toFun s
[PROOFSTEP]
exact omegaLimit_subset_of_tendsto ϕ s ht
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => x + t) f f
t : τ
⊢ ω f ϕ.toFun s = ω f ϕ.toFun (toFun ϕ (-t) '' (toFun ϕ t '' s))
[PROOFSTEP]
simp [image_image, ← map_add]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s
[PROOFSTEP]
simp only [subset_def, mem_omegaLimit_iff_frequently₂, frequently_iff]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ ∀ (x : α),
    (∀ (n : Set α), n ∈ 𝓝 x → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)) →
      ∀ (n : Set α), n ∈ 𝓝 x → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
intro _ h
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
⊢ ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rintro n hn u hu
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩
[GOAL]
case intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases h o (IsOpen.mem_nhds ho₂ ho₃) hu with ⟨t, _ht₁, ht₂⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₁ : (ω f ϕ s ∩ o).Nonempty :=
  ht₂.mono (inter_subset_inter_left _ ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
  l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_fw_image _ _ _ hu hb.1, hb.2⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₃ : (o ∩ image2 ϕ u s).Nonempty := by
  rcases l₂ with ⟨b, hb₁, hb₂⟩
  exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
⊢ Set.Nonempty (o ∩ image2 ϕ.toFun u s)
[PROOFSTEP]
rcases l₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
b : α
hb₁ : b ∈ closure (image2 ϕ.toFun u s)
hb₂ : b ∈ o
⊢ Set.Nonempty (o ∩ image2 ϕ.toFun u s)
[PROOFSTEP]
exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
l₃ : Set.Nonempty (o ∩ image2 ϕ.toFun u s)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases l₃ with ⟨ϕra, ho, ⟨_, _, hr, ha, hϕra⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
ϕra : α
ho : ϕra ∈ o
w✝¹ : τ
w✝ : α
hr : w✝¹ ∈ u
ha : w✝ ∈ s
hϕra : toFun ϕ w✝¹ w✝ = ϕra
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩


[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 0 x = 0
[PROOFSTEP]
simp [birkhoffAverage]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 1 x = g x
[PROOFSTEP]
simp [birkhoffAverage]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁶ : DivisionSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
F : Type u_5
N : Type u_6
inst✝³ : DivisionSemiring S
inst✝² : AddCommMonoid N
inst✝¹ : Module S N
inst✝ : AddMonoidHomClass F M N
g' : F
f : α → α
g : α → M
n : ℕ
x : α
⊢ ↑g' (birkhoffAverage R f g n x) = birkhoffAverage S f (↑g' ∘ g) n x
[PROOFSTEP]
simp only [birkhoffAverage, map_inv_nat_cast_smul g' R S, map_birkhoffSum]
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
⊢ birkhoffAverage R = birkhoffAverage S
[PROOFSTEP]
ext
[GOAL]
case h.h.h.h
R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : DivisionSemiring S
inst✝ : Module S M
x✝³ : α → α
x✝² : α → M
x✝¹ : ℕ
x✝ : α
⊢ birkhoffAverage R x✝³ x✝² x✝¹ x✝ = birkhoffAverage S x✝³ x✝² x✝¹ x✝
[PROOFSTEP]
apply birkhoffAverage_congr_ring
[GOAL]
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ birkhoffAverage R f g n x = g x
[PROOFSTEP]
rw [birkhoffAverage, h.birkhoffSum_eq, nsmul_eq_smul_cast R, inv_smul_smul₀]
[GOAL]
case hc
R : Type u_1
α : Type u_2
M : Type u_3
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : CharZero R
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
rwa [Nat.cast_ne_zero]
[GOAL]
M : Type u_2
α : Type u_3
R : Type u_1
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)
[PROOFSTEP]
simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]


[GOAL]
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
g : α → M
m n : ℕ
x : α
⊢ birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
[PROOFSTEP]
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
⊢ birkhoffSum f g n x = n • g x
[PROOFSTEP]
simp [birkhoffSum, (h.iterate _).eq]
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
[PROOFSTEP]
rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x), ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x), ← sub_add, ←
  sub_add, sub_add_comm]