awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
h : n - 1 ≠ 0
hnx :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
y : AddCircle T
⊢ @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      (-@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) + -x +
          n • y +
        x) =
    n • y

Tactic:
abel
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℕ
h : 1 < n
⊢ LT.lt (α := ℤ) 1 |(↑n : ℤ)|

Tactic:
simp [h]
-- Module: Mathlib.Dynamics.Ergodic.AddCircleAdd
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
rw :
  Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ a + x) volume ↔
    DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a
rw₁ rw₂ : (DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a) ↔ DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ a + x) volume ↔ addOrderOf a = 0

Tactic:
rw [← denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul]

Premises used: AddCircle.denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul
-- Module: Mathlib.Dynamics.Ergodic.AddCircleAdd
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ x + a) volume ↔ addOrderOf a = 0

Tactic:
simp only [add_comm, ← ergodic_add_left]

Premises used: AddCircle.ergodic_add_left, add_comm
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ : Measure α
inst_1 : IsFiniteMeasure μ
h : MeasurePreserving f μ μ
⊢ Conservative f μ

Tactic:
⟨h.quasiMeasurePreserving, fun _ hsm h0 => h.exists_mem_iterate_mem hsm.nullMeasurableSet h0⟩

Premises used: MeasureTheory.MeasurePreserving.exists_mem_iterate_mem, MeasurableSet.nullMeasurableSet, MeasureTheory.Conservative.mk, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
x : Set α
h : MeasurableSet x
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) x : ENNReal) (0 : ENNReal)
⊢ ∃ x_1 ∈ x, ∃ (m : ℕ), m ≠ 0 ∧ id^[m] x_1 ∈ x

Tactic:
simpa [exists_ne] using nonempty_of_measure_ne_zero h0

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, exists_ne
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ ν : Measure α
h : Conservative f μ
hν : ν ≪ μ
h' : QuasiMeasurePreserving f ν ν
⊢ Conservative f ν

Tactic:
⟨h', fun _ hsm h0 ↦ h.exists_mem_iterate_mem' hsm (mt (@hν _) h0)⟩

Premises used: mt, MeasureTheory.Conservative.mk, MeasureTheory.Conservative.exists_mem_iterate_mem'
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
h : Conservative f μ
hs : MapsTo f s s
⊢ Conservative f (μ.restrict s)

Tactic:
.of_absolutelyContinuous h (absolutelyContinuous_of_le restrict_le_self) <|
    h.toQuasiMeasurePreserving.restrict hs

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.restrict, MeasureTheory.Conservative.of_absolutelyContinuous, MeasureTheory.Conservative.toQuasiMeasurePreserving, MeasureTheory.Measure.restrict_le_self, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ ν : Measure α
hf : Conservative f μ
h : ae μ = ae ν
⊢ Conservative f ν

Tactic:
.of_absolutelyContinuous hf h.ge.absolutelyContinuous_of_ae <|
    hf.toQuasiMeasurePreserving.mono h.ge.absolutelyContinuous_of_ae h.le.absolutelyContinuous_of_ae

Premises used: Eq.ge, MeasureTheory.Conservative.of_absolutelyContinuous, MeasureTheory.Conservative.toQuasiMeasurePreserving, LE.le.absolutelyContinuous_of_ae, Eq.le, MeasureTheory.Measure.QuasiMeasurePreserving.mono
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
μ ν : Measure α
h : ae μ = ae ν
⊢ Conservative f μ ↔ Conservative f ν

Tactic:
⟨(congr_ae · h), (congr_ae · h.symm)⟩

Premises used: MeasureTheory.Conservative.congr_ae, Iff.intro, Eq.symm
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
rcases :
  ∀ (t : Set α) (hsub : t ⊆ s) (htm : MeasurableSet t) (hts : t =ᶠ[ae μ] s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)

Tactic:
rwa [measure_congr hts]

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
rcases : ∀ (x : α) (hxt : x ∈ t) (m : ℕ) (hm₀ : m ≠ 0) (hmt : f^[m] x ∈ t), ∃ 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' htm (by rwa [measure_congr hts]) with ⟨x, hxt, m, hm₀, hmt⟩

Premises used: MeasureTheory.Conservative.exists_mem_iterate_mem'
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
x : α
hxt : x ∈ t
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ t
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
⟨x, hsub hxt, m, hm₀, hsub hmt⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hsm : NullMeasurableSet s μ
hs₀ : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : Set α
hsub : t ⊆ s
htm : MeasurableSet t
hts : t =ᶠ[ae μ] s
x : α
hxt : x ∈ t
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ t
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

Tactic:
exact ⟨x, hsub hxt, m, hm₀, hsub hmt⟩
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
by_contra :
  ∀
    (H :
      ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)),
    False
⊢ ∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)

Tactic:
by_contra H
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
⊢ Set.Finite (α := ℕ)
    {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)}

Tactic:
rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H

Premises used: Nat.frequently_atTop_iff_infinite, Set.not_infinite
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H :
  Set.Finite (α := ℕ)
    {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)}
⊢ Membership.mem (γ := Set ℕ)
    {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} 0

Tactic:
simpa
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H :
  Set.Finite (α := ℕ)
    {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)}
h :
  ∀ (x a : ℕ),
    a > x → Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) ↔
      Membership.mem (γ := Set ℕ)
          {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} a →
        a ≤ x
⊢ ∃ (N : ℕ),
    Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal) ∧
      ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)

Tactic:
convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4

Premises used: Set.exists_max_image, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H :
  Set.Finite (α := ℕ)
    {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)}
x a : ℕ
h :
  x < a → Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) ↔
    Membership.mem (γ := Set ℕ)
        {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} a →
      a ≤ x
h₁ :
  ¬a ≤ x → Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) ↔
    Membership.mem (γ := Set ℕ)
        {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} a →
      a ≤ x
h₂ :
  ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) → a ≤ x ↔
    Membership.mem (γ := Set ℕ)
        {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} a →
      a ≤ x
h₃ h₄ :
  ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) → a ≤ x ↔
    Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[a] ⁻¹' s) : ENNReal) (0 : ENNReal) → a ≤ x
⊢ a > x → Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t a) : ENNReal) (0 : ENNReal) ↔
    Membership.mem (γ := Set ℕ)
        {n : ℕ | Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[n] ⁻¹' s) : ENNReal) (0 : ENNReal)} a →
      a ≤ x

Tactic:
rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]

Premises used: not_le, not_imp_comm, Set.mem_setOf, gt_iff_lt
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
obtain :
  ∀ (N : ℕ) (hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal))
    (hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)), False
⊢ False

Tactic:
obtain ⟨N, hN, hmax⟩ : ∃ N, μ (t N) ≠ 0 ∧ ∀ n > N, μ (t n) = 0 := by
    rw [Nat.frequently_atTop_iff_infinite, not_infinite] at H
    convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4
    rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
⊢ ∀ {n : ℕ}, NullMeasurableSet (t n) μ

Tactic:
have htm {n : ℕ} : NullMeasurableSet (t n) μ :=
    hs.inter <| hs.preimage <| hf.toQuasiMeasurePreserving.iterate n
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
⊢ let T := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n;
  T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n

Tactic:
set T := t N \ ⋃ n > N, t n with hT
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
rwa : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋃ (n : ℕ), ⋃ (_ : n > N), t n) : ENNReal) (0 : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)

Tactic:
rwa [hT, measure_diff_null]

Premises used: MeasureTheory.measure_diff_null
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋃ (n : ℕ), ⋃ (_ : n > N), t n) : ENNReal) (0 : ENNReal)

Tactic:
(measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax

Premises used: Iff.mpr, Set.Mem, setOf, LT.lt, Set.to_countable, MeasureTheory.measure_biUnion_null_iff, Nat.lt
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋃ (n : ℕ), ⋃ (_ : n > N), t n) : ENNReal) (0 : ENNReal)

Tactic:
exact (measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax

Premises used: Iff.mpr, setOf, LT.lt, Set.to_countable, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)

Tactic:
have hμT : μ T ≠ 0 := by
    rwa [hT, measure_diff_null]
    exact (measure_biUnion_null_iff {n | N < n}.to_countable).2 hmax
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
⊢ NullMeasurableSet T μ

Tactic:
have hTm : NullMeasurableSet T μ := htm.diff <| .biUnion {n | N < n}.to_countable fun _ _ ↦ htm
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
rcases : ∀ (x : α) (hxt : x ∈ T) (m : ℕ) (hm₀ : m ≠ 0) (hmt : f^[m] x ∈ T), False
⊢ False

Tactic:
rcases hf.exists_mem_iterate_mem hTm hμT with ⟨x, hxt, m, hm₀, hmt⟩

Premises used: MeasureTheory.Conservative.exists_mem_iterate_mem
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ False

Tactic:
hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, And.right, And.left, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
refine_1 : N + m > N
refine_2 : x ∈ f^[N + m] ⁻¹' s
⊢ False

Tactic:
refine hxt.2 <| mem_iUnion₂.2 ⟨N + m, ?_, hxt.1.1, ?_⟩

Premises used: And.right
-- Module: Mathlib.Dynamics.Ergodic.Conservative
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
t : ℕ → Set α := fun (n : ℕ) ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
N : ℕ
hN : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal)
hmax : ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ (n : ℕ), ⋃ (_ : n > N), t n
hμT : Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) T : ENNReal) (0 : ENNReal)
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ N + m > N

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero