case intro
α : Type u_1
β : Type ?u.275571
γ : Type ?u.275574
δ : Type ?u.275577
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ Set.univ < ↑N * ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[m]) x ∈ s
α : Type u_1
β : Type ?u.275571
γ : Type ?u.275574
δ : Type ?u.275577
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[m]) x ∈ s
rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.275571
γ : Type ?u.275574
δ : Type ?u.275577
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ Set.univ < ↑N * ↑↑μ s
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Set.Ioo 0 N
hmx : (f^[m]) x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[m]) x ∈ s
case intro
α : Type u_1
β : Type ?u.275571
γ : Type ?u.275574
δ : Type ?u.275577
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ Set.univ < ↑N * ↑↑μ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[m]) x ∈ s
rcases hf.exists_mem_image_mem_of_volume_lt_mul_volume hs hN with ⟨x, hx, m, hm, hmx⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.275571
γ : Type ?u.275574
δ : Type ?u.275577
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
μ : Measure α
f : α → α
s : Set α
inst✝ : IsFiniteMeasure μ
hf : MeasurePreserving f
hs : MeasurableSet s
hs' : ↑↑μ s ≠ 0
N : ℕ
hN : ↑↑μ Set.univ < ↑N * ↑↑μ s
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Set.Ioo 0 N
hmx : (f^[m]) x ∈ s
⊢ ∃ x, x ∈ s ∧ ∃ m x_1, (f^[m]) x ∈ s
exact ⟨x, hx, m, hm.1.ne', hmx⟩