-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
lemma measure_symmDiff_preimage_iterate_le
    (hf : MeasurePreserving f μ μ) (hs : NullMeasurableSet s μ) (n : ℕ) :
    μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
⊢ μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))

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

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))

Tactic:
refine le_trans (measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n+1] ⁻¹' s)) (add_le_add ih ?_)

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ (n + 1) • μ (s ∆ (f ⁻¹' s))

Tactic:
simp only [add_smul, one_smul, ← n.add_one]

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) + μ (s ∆ (f ⁻¹' s))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
⊢ μ (s ∆ (f^[0] ⁻¹' s)) ≤ 0 • μ (s ∆ (f ⁻¹' s))

case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ (s ∆ (f^[n + 1] ⁻¹' s)) ≤ (n + 1) • μ (s ∆ (f ⁻¹' s))

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
⊢ μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))

Tactic:
replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
  hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
n : ℕ
ih : μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s))
hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ
⊢ μ ((f^[n] ⁻¹' s) ∆ (f^[n + 1] ⁻¹' s)) ≤ μ (s ∆ (f ⁻¹' s))

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → α
s : Set α
hf : MeasurePreserving f μ μ
hs : NullMeasurableSet s μ
⊢ μ (s ∆ (f^[0] ⁻¹' s)) ≤ 0 • μ (s ∆ (f ⁻¹' s))

Tactic:
simp

Result:
no goals