awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have a : (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: congr; rw [← DivisibleBy.div_cancel x h]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
a : (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have a₁ : @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: congr; rw [← DivisibleBy.div_cancel x h]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have conv_rhs : n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
  (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
    @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have rw : n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
      HSMul.hSMul (α := ℤ) 1
        (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)) +
    @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: rw [sub_smul, one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
rw :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
        HSMul.hSMul (α := ℤ) 1
          (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have rw₁ : n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
    @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: rw [sub_smul, one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
rw :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
        HSMul.hSMul (α := ℤ) 1
          (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
rw₁ :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
        @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have rw₂ : n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: rw [sub_smul, one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
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
⊢ Eq (α := AddCircle T → AddCircle T)
    ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) fun (y : AddCircle T) ↦
    n • y
have 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)
Tactic: have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) := by
    conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
    rw [sub_smul, one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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)
⊢ Eq (α := AddCircle T → AddCircle T)
    ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) fun (y : AddCircle T) ↦
    n • y
have h₁ : ∀ (y : AddCircle T),
  ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) y = n • y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
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
⊢ ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) y = n • y
have h₁ : @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: simp only [f, e, hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply,
    smul_add, zsmul_neg', neg_smul, neg_add_rev]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircleAdd (goal)
Goal:
p : ℝ
inst : Fact (0 < p)
a : AddCircle p
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ a + x) volume ↔ addOrderOf a = 0
have rw : Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ a + x) volume ↔
  DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a
Tactic: rw [← denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircleAdd (goal)
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
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (x : AddCircle p) ↦ a + x) volume ↔ addOrderOf a = 0
have rw₁ : (DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a) ↔ DenseRange (X := AddCircle p) fun (x : ℤ) ↦ x • a
Tactic: rw [← denseRange_zsmul_iff, ergodic_add_left_iff_denseRange_zsmul]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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)
⊢ ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
have rcases : ∀ (t : Set α) (hsub : t ⊆ s) (htm : MeasurableSet t) (hts : t =ᶠ[ae μ] s), ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
Tactic: rcases hsm.exists_measurable_subset_ae_eq with ⟨t, hsub, htm, hts⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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 ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
have rcases : ∀ (x : α) (hxt : x ∈ t) (m : ℕ) (hm₀ : m ≠ 0) (hmt : f^[m] x ∈ t), ∃ 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⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ ∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)
have by_contra : ∀ (H : ¬∃ᶠ (m : ℕ) in atTop, Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ f^[m] ⁻¹' s) : ENNReal) (0 : ENNReal)),
  False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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 : ℕ),
    Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal) ∧
      ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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)}
⊢ ∃ (N : ℕ),
    Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t N) : ENNReal) (0 : ENNReal) ∧
      ∀ n > N, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (t n) : ENNReal) (0 : ENNReal)
have 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
Tactic: convert! exists_max_image _ (·) H ⟨0, by simpa⟩ using 4
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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 : ℕ
⊢ 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
have 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
Tactic: rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ 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
have 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
Tactic: rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ 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
have 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
Tactic: rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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
⊢ 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
have 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
Tactic: rw [gt_iff_lt, ← not_le, not_imp_comm, mem_setOf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (goal)
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)
⊢ False
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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)
⊢ False
have htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
Tactic: have htm {n : ℕ} : NullMeasurableSet (t n) μ :=
    hs.inter <| hs.preimage <| hf.toQuasiMeasurePreserving.iterate n
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Conservative (hypothesis)
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) μ
⊢ False
have hT : 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