awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α ≃ᵐ β
hf : MeasurePreserving (⇑f : (a : α) → β) μa μb
s : Set β
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_preimage_emb hf f.measurableEmbedding s

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.measure_preimage_emb
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
rw :
  LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← hf.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_map_apply hf.aemeasurable _

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.Measure.le_map_apply
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ LE.le (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((map f μa : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact le_map_apply hf.aemeasurable _

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.Measure.le_map_apply
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : Eq (α := ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μa : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hf.quasiMeasurePreserving.preimage_null hs

Premises used: MeasureTheory.MeasurePreserving.quasiMeasurePreserving, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
inst_3 : MeasurableSingletonClass γ
f : α → β
hf : MeasurePreserving f μa μb
g : β → γ
hg : NullMeasurable g μb
s : Set γ
hs : s.Subsingleton
⊢ s ∈ Filter.map (g ∘ f) (ae μa) ↔ s ∈ Filter.map g (ae μb)

Tactic:
simp only [Filter.mem_map, mem_ae_iff, ← hf.measure_preimage (hg hs.measurableSet).compl,
      preimage_comp, preimage_compl]

Premises used: MeasureTheory.NullMeasurableSet.compl, Set.preimage_comp, Set.Subsingleton.measurableSet, MeasureTheory.mem_ae_iff, Set.preimage_compl, Filter.mem_map, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
⊢ Filter.EventuallyConst (f ⁻¹' s) (ae μa) ↔ Filter.EventuallyConst s (ae μb)

Tactic:
aeconst_comp hf hs.mem

Premises used: MeasurableSet.mem, Set.Mem, setOf, Set.preimage, MeasureTheory.MeasurePreserving.aeconst_comp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
rw : HAdd.hAdd (α := Measure β) (map f μa) (map f μa') = μb + μb'
rw₁ : μb + map f μa' = μb + μb'
rw₂ rw₃ : μb + μb' = μb + μb'
⊢ map f (μa + μa') = μb + μb'

Tactic:
rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]

Premises used: MeasureTheory.Measure.map_add, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μa : Measure α
μb : Measure β
R : Type u_5
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α → β
hf : MeasurePreserving f μa μb
c : R
rw : HSMul.hSMul (β := Measure β) c (map f μa) = c • μb
rw₁ rw₂ : c • μb = c • μb
⊢ map f (c • μa) = c • μb

Tactic:
rw [Measure.map_smul, hf.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.map_smul
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[0] ⁻¹' s)) ≤
    HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 0 ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HAdd.hAdd (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) (n + 1) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)

Tactic:
simp only [add_smul, one_smul]

Premises used: one_smul, add_smul
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
    HAdd.hAdd (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)

Tactic:
grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]

Premises used: MeasureTheory.measure_symmDiff_le, Nat.iterate, Set.preimage, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ NullMeasurableSet (s ∆ (f ⁻¹' s)) μ

Tactic:
replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
      hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
succ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f ∘ f^[n] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n] ⁻¹' f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (f^[n] ⁻¹' s ∆ (f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ₃ succ₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)

Tactic:
rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]

Premises used: Function.iterate_succ', MeasureTheory.MeasurePreserving.iterate, Set.preimage_comp, Set.preimage_symmDiff, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
zero :
  (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[0] ⁻¹' s)) ≤
    HSMul.hSMul (α := ℕ) (β := ℝ≥0∞) 0 ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
succ :
  ∀ (n : ℕ)
    (ih :
      (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
        HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)),
    (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n + 1] ⁻¹' s)) ≤
      HSMul.hSMul (β := ℝ≥0∞) (n + 1) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ (f^[n] ⁻¹' s)) ≤
    HSMul.hSMul (β := ℝ≥0∞) n ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (f ⁻¹' s)) : ℝ≥0∞)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp only [add_smul, one_smul]
    grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
    replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
      hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
    rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]

Premises used: Function.iterate_succ', MeasureTheory.measure_symmDiff_le, MeasureTheory.MeasurePreserving.iterate, Set.preimage_comp, Nat.iterate, one_smul, add_smul, Set.preimage, HAdd.hAdd, Set.preimage_symmDiff, OfNat.ofNat, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ

Tactic:
have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦
    hs.preimage (hf.iterate m).quasiMeasurePreserving
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
⊢ ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)

Tactic:
simpa [B]
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)

Tactic:
have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
⊢ ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty

Tactic:
simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this

Premises used: MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
obtain :
  ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (x : α) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s),
    ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
obtain ⟨i, hi, j, hj, hij, x, hxi : f^[i] x ∈ s, hxj : f^[j] x ∈ s⟩ :
      ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty := by
    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
inr :
  ∀
    (this :
      ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
        ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s)
    (hlt : ¬i < j), ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
wlog :
  ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
    ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
wlog hlt : i < j generalizing i j
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
this :
  ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
    ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
hlt : ¬i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
this j hj i hi hij.symm hxj hxi (hij.lt_or_gt.resolve_left hlt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
x : α
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
this :
  ∀ (i : ℕ) (hi : i < n) (j : ℕ) (hj : j < n) (hij : i ≠ j) (hxi : f^[i] x ∈ s) (hxj : f^[j] x ∈ s) (hlt : i < j),
    ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s
hlt : ¬i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
exact this j hj i hi hij.symm hxj hxi (hij.lt_or_gt.resolve_left hlt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩

Premises used: lt_of_le_of_lt, HSub.hSub, Nat.sub_le, Nat.iterate, And.intro, Exists.intro, tsub_pos_of_lt
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
refine : f^[j - i] (f^[i] x) ∈ s
⊢ ∃ x ∈ s, ∃ m ∈ Ioo 0 n, f^[m] x ∈ s

Tactic:
refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
hvol :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
A : ∀ (m : ℕ), NullMeasurableSet (f^[m] ⁻¹' s) μ
B : ∀ (m : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
this :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (∑ m ∈ Finset.range n, (μ : (a : Set α) → ℝ≥0∞) (f^[m] ⁻¹' s) : ℝ≥0∞)
x : α
i : ℕ
hi : i < n
j : ℕ
hj : j < n
hij : i ≠ j
hxi : f^[i] x ∈ s
hxj : f^[j] x ∈ s
hlt : i < j
rwa : f^[j - i + i] x ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : f^[j] x ∈ s
⊢ f^[j - i] (f^[i] x) ∈ s

Tactic:
rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]

Premises used: Function.iterate_add_apply, tsub_add_cancel_of_le, LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rcases :
  ∀ (N : ℕ)
    (hN :
      (μ : (a : Set α) → ℝ≥0∞) univ <
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩

Premises used: ENNReal.exists_nat_mul_gt, Set.univ, MeasureTheory.measure_ne_top
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
N : ℕ
hN :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rcases : ∀ (x : α) (hx : x ∈ s) (m : ℕ) (hm : m ∈ Ioo 0 N) (hmx : f^[m] x ∈ s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hf.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure hs hN with ⟨x, hx, m, hm, hmx⟩

Premises used: MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
N : ℕ
hN :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Ioo 0 N
hmx : f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
⟨x, hx, m, hm.1.ne', hmx⟩

Premises used: LT.lt.ne', And.left, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.Ergodic.MeasurePreserving
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
inst_1 : IsFiniteMeasure μ
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
N : ℕ
hN :
  (μ : (a : Set α) → ℝ≥0∞) univ <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
x : α
hx : x ∈ s
m : ℕ
hm : m ∈ Ioo 0 N
hmx : f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
exact ⟨x, hx, m, hm.1.ne', hmx⟩