awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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∞)
inr : (μ : (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

Tactic:
right
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 ∈ s,
    ∀ {ι' : 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)

Tactic:
exists_mem_of_measure_ne_zero_of_ae h
      (IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div μ s 1)

Premises used: IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div, MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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∞)
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
⊢ (μ : (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)

Premises used: IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div, MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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) : ℝ)
j : ι
hj : 0 < n j
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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) : ℝ)
⊢ ∀ᶠ (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
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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)

Tactic:
tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
refine : Tendsto δ l (𝓝 0)
⊢ Tendsto δ l (𝓝[>] 0)

Tactic:
refine tendsto_nhdsWithin_iff.mpr ⟨?_, hδ₀⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, And.intro
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ 0 < T⁻¹ * 2

Tactic:
positivity
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 (β := ℝ) (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)
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 (β := ℝ) (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹ l (𝓝 0)

Tactic:
hu₂.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
h₁ : δ = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹
⊢ Tendsto δ l (𝓝 0)

Tactic:
convert! hu₂.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
h₁ : ∀ (j : ι), δ j = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹ j
⊢ δ = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹

Tactic:
ext j
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
j : ι
⊢ δ j = (fun (j : ι) ↦ T⁻¹ * 2 * (↑(n j) : ℝ))⁻¹ j

Tactic:
simp only [δ, Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]

Premises used: mul_assoc, inv_inv, mul_inv_rev, div_eq_inv_mul, Pi.inv_apply
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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)

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]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
simp : 0 ≤ δ j
⊢ d ∈ closedBall d (1 * δ j)

Tactic:
simp only [one_mul, mem_closedBall, dist_self]

Premises used: dist_self, Metric.mem_closedBall, one_mul
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ 0 ≤ δ j

Tactic:
apply hj.le

Premises used: LT.lt.le
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : ι) 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
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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)
hw : ∀ᶠ (j : ι) in l, d ∈ closedBall d (1 * δ 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)

Tactic:
hd _ δ hδ₁ hw
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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)
hw : ∀ᶠ (j : ι) in l, d ∈ closedBall d (1 * δ 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)

Tactic:
exact hd _ δ hδ₁ hw