awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℝ))
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have hd₁ : 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)
Tactic: replace hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1) := by
    let δ : ι → ℝ := fun j => T / (2 * ↑(n j))
    have hδ₀ : ∀ᶠ j in l, 0 < δ j :=
      (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
    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]
    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
    exact hd _ δ hδ₁ hw
Cleared hypotheses: hd
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
this :
  ∀ᶠ (j : ι) in l,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have hd₁ : Tendsto (β := ℝ≥0∞)
  (fun (x : ι) ↦ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)) l (𝓝 1)
Tactic: replace hd := hd.congr' this
Cleared hypotheses: hd
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
this :
  ∀ᶠ (j : ι) in l,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
hd :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ι) ↦ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)) l (𝓝 1)
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have rwa : ∀ (hd : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T) = 1),
  (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
Cleared hypotheses: hd
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
this :
  ∀ᶠ (j : ι) in l,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
hd :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ι) ↦ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)) l (𝓝 1)
rwa :
  ∀ (hd : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T) = 1),
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have rwa₁ : ∀ (hd : (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T),
  (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
Tactic: rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
Cleared hypotheses: hd
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
⊢ (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
have inr : ∀ᶠ (j : ι) in l,
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
Tactic: suffices ∀ᶠ j in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T by
    replace hd := hd.congr' this
    rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
⊢ ∀ᶠ (j : ι) in l,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr : ∀ (j : ι) (hj : 0 < n j),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
Tactic: refine (hu₂.eventually_gt_atTop 0).mono fun j hj => ?_
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have this : addOrderOf (u j) = n j
Tactic: have : addOrderOf (u j) = n j := rfl
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have huj : IsOfFinAddOrder (u j)
Tactic: have huj : IsOfFinAddOrder (u j) := addOrderOf_pos_iff.mp hj
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
⊢ LE.le (α := ℝ) 1 (↑(n j) : ℝ)
have norm_cast : 1 ≤ n j
Tactic: norm_cast
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
Tactic: have huj' : 1 ≤ (↑(n j) : ℝ) := by norm_cast
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hI₀ : μ (I j) ≠ 0 := (measure_closedBall_pos _ d <| by positivity).ne.symm
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
have hb : Ne (α := ℝ) (↑(n j) : ℝ) 0
Tactic: rw [volume_closedBall, mul_div, mul_div_mul_left T _ two_ne_zero,
      min_eq_right (div_le_self hT₀.le huj'), mul_comm, ← nsmul_eq_mul, ← ENNReal.ofReal_nsmul,
      nsmul_eq_mul, mul_div_cancel₀]
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have hI₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
  ENNReal.ofReal T
Tactic: have hI₂ : μ (I j) * ↑(n j) = ENNReal.ofReal T := by
    rw [volume_closedBall, mul_div, mul_div_mul_left T _ two_ne_zero,
      min_eq_right (div_le_self hT₀.le huj'), mul_comm, ← nsmul_eq_mul, ← ENNReal.ofReal_nsmul,
      nsmul_eq_mul, mul_div_cancel₀]
    exact Nat.cast_ne_zero.mpr hj.ne'
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
hI₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
    ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]
-- 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
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  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)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
hI₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
inr :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr₁ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
    (HSMul.hSMul (β := ℝ≥0∞) (addOrderOf (u j))
      ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
          (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
        ℝ≥0∞))
Tactic: rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]