awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)
have suffices : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
Tactic: suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s
have refine : ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s
Tactic: refine (hμs.and_eventually ?_).exists
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s
have rw : ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s
Tactic: rw [ae_ae_comm]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
rw : ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s
have rw₁ : MeasurableSet.{u_1} (α := G × G) {x : G × G | x.2 * x.1 ∈ s ↔ x.1 ∈ s}
Tactic: rw [ae_ae_comm]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s
have obtain : ∀ (a : G) (has : a ∈ s) (ha : ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s), ∀ᵐ (x : G) ∂μ, x ∈ s
Tactic: obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (b * a ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs b).mem_iff
    · exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
⊢ ErgodicSMul Gᵐᵒᵖ G μ
have refine : ∀ {s : Set G} (hsm : MeasurableSet s) (hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s),
  EventuallyConst s (ae μ)
Tactic: refine ⟨fun {s} hsm hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)
have simp : (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s
Tactic: simp only [eventuallyConst_set, ← not_frequently]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)
have suffices : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
Tactic: suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s
have refine : ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s
Tactic: refine (hμs.and_eventually ?_).exists
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s
have rw : ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s
Tactic: rw [ae_ae_comm]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
rw : ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s
⊢ ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s
have rw₁ : MeasurableSet.{u_1} (α := G × G) {x : G × G | x.1 * x.2 ∈ s ↔ x.1 ∈ s}
Tactic: rw [ae_ae_comm]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s
have obtain : ∀ (a : G) (has : a ∈ s) (ha : ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s), ∀ᵐ (x : G) ∂μ, x ∈ s
Tactic: obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (a * b ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff
    · exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
hs : NullMeasurableSet s volume
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
⊢ s =ᶠ[ae (F := Measure (AddCircle T)) volume] ∅ ∨ s =ᶠ[ae (F := Measure (AddCircle T)) volume] univ
have set : let μ : Measure (AddCircle T) := volume;
∀ (hs : NullMeasurableSet s μ) (hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s), s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
Tactic: set μ := (volume : Measure <| AddCircle T)
Cleared hypotheses: hs, hu₁
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
have hT₀ : 0 < T
Tactic: have hT₀ : 0 < T := hT.out
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
have hT₁ : ENNReal.ofReal T ≠ 0
Tactic: have hT₁ : ENNReal.ofReal T ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: rcases eq_or_ne (μ s) 0 with h | h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
inl :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have inr : ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: rcases eq_or_ne (μ s) 0 with h | h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have inr : (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: right
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have inr : ∀ (d : AddCircle T)
  (hd :
    ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
          Tendsto (β := ℝ≥0∞)
            (fun (j : ι') ↦
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
                ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
            l (𝓝 1)),
  (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: obtain ⟨d, -, hd⟩ : ∃ d, d ∈ s ∧ ∀ {ι'} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) → (∀ᶠ j in l, d ∈ closedBall (w j) (1 * δ j)) →
      Tendsto (fun j => μ (s ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1) :=
    exists_mem_of_measure_ne_zero_of_ae h
      (IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div μ s 1)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
have hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
Tactic: have hδ₀ : ∀ᶠ j in l, 0 < δ j :=
      (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝[>] 0)
have refine : Tendsto δ l (𝓝 0)
Tactic: refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝 0)
have hu₃ : Tendsto (β := ℝ) (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ)) l atTop
Tactic: replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
        (tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
Cleared hypotheses: hu₂
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hu₂ : Tendsto (β := ℝ) (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ)) l atTop
⊢ Tendsto δ l (𝓝 0)
have h₁ : δ = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹
Tactic: convert! hu₂.inv_tendsto_atTop
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hu₂ : Tendsto (β := ℝ) (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ)) l atTop
⊢ δ = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹
have h₁ : ∀ (j : ι), δ j = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹ j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
have hδ₁ : Tendsto δ l (𝓝[>] 0)
Tactic: have hδ₁ : Tendsto δ l (𝓝[>] 0) := by
      refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩
      replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
        (tendsto_natCast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
      convert! hu₂.inv_tendsto_atTop
      ext j
      simp only [δ, Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[>] 0)
j : ι
hj : 0 < δ j
⊢ d ∈ closedBall d (1 * δ j)
have simp : 0 ≤ δ j
Tactic: simp only [one_mul, mem_closedBall, dist_self]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
hd :
  ∀ {ι' : Type u_1} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι') ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
δ : ι → ℝ := fun (j : ι) ↦ T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[>] 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
have hw : ∀ᶠ (j : ι) in l, d ∈ closedBall d (1 * δ j)
Tactic: have hw : ∀ᶠ j in l, d ∈ closedBall d (1 * δ j) := hδ₀.mono fun j hj => by
      simp only [one_mul, mem_closedBall, dist_self]
      apply hj.le