[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
hs : NullMeasurableSet s
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
u : ι → AddCircle T
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae volume] s
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
set μ := (volume : Measure <| AddCircle T)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
u : ι → AddCircle T
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
set n : ι → ℕ := addOrderOf ∘ u
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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
[PROOFSTEP]
have hT₀ : 0 < T := hT.out
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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
[PROOFSTEP]
have hT₁ : ENNReal.ofReal T ≠ 0 := by simpa
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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
⊢ ENNReal.ofReal T ≠ 0
[PROOFSTEP]
simpa
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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
[PROOFSTEP]
rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 = 0 ∨ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
cases' eq_or_ne (μ s) 0 with h h
[GOAL]
case inl
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s = 0
⊢ ↑↑μ s = 0 ∨ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
exact Or.inl h
[GOAL]
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
⊢ ↑↑μ s = 0 ∨ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
right
[GOAL]
case inr.h
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
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)
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
let I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
replace hd : Tendsto (fun j => μ (s ∩ I j) / μ (I j)) l (𝓝 1)
[GOAL]
case hd
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
⊢ Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
[PROOFSTEP]
let δ : ι → ℝ := fun j => T / (2 * ↑(n j))
[GOAL]
case hd
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
⊢ Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
[PROOFSTEP]
have hδ₀ : ∀ᶠ j in l, 0 < δ j := (hu₂.eventually_gt_atTop 0).mono fun j hj => div_pos hT₀ <| by positivity
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
j : ι
hj : 0 < n j
⊢ 0 < 2 * ↑(n j)
[PROOFSTEP]
positivity
[GOAL]
case hd
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
[PROOFSTEP]
have hδ₁ : Tendsto δ l (𝓝[>] 0) := by
  refine' tendsto_nhdsWithin_iff.mpr ⟨_, hδ₀⟩
  replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
    (tendsto_nat_cast_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]
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝[Ioi 0] 0)
[PROOFSTEP]
refine' tendsto_nhdsWithin_iff.mpr ⟨_, hδ₀⟩
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ Tendsto δ l (𝓝 0)
[PROOFSTEP]
replace hu₂ : Tendsto (fun j => T⁻¹ * 2 * n j) l atTop :=
  (tendsto_nat_cast_atTop_iff.mpr hu₂).const_mul_atTop (by positivity : 0 < T⁻¹ * 2)
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
⊢ 0 < T⁻¹ * 2
[PROOFSTEP]
positivity
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hu₂ : Tendsto (fun j => T⁻¹ * 2 * ↑(n j)) l atTop
⊢ Tendsto δ l (𝓝 0)
[PROOFSTEP]
convert hu₂.inv_tendsto_atTop
[GOAL]
case h.e'_3
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (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))⁻¹
[PROOFSTEP]
ext j
[GOAL]
case h.e'_3.h
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (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
[PROOFSTEP]
simp only [Pi.inv_apply, mul_inv_rev, inv_inv, div_eq_inv_mul, ← mul_assoc]
[GOAL]
case hd
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[Ioi 0] 0)
⊢ Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
[PROOFSTEP]
have hw : ∀ᶠ j in l, d ∈ closedBall d (1 * δ j) :=
  hδ₀.mono fun j hj => by
    simp only [comp_apply, one_mul, mem_closedBall, dist_self]
    apply hj.le
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[Ioi 0] 0)
j : ι
hj : 0 < δ j
⊢ d ∈ closedBall d (1 * δ j)
[PROOFSTEP]
simp only [comp_apply, one_mul, mem_closedBall, dist_self]
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[Ioi 0] 0)
j : ι
hj : 0 < δ j
⊢ 0 ≤ T / (2 * ↑(addOrderOf (u j)))
[PROOFSTEP]
apply hj.le
[GOAL]
case hd
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
hd :
  ∀ {ι' : Type ?u.5513} {l : Filter ι'} (w : ι' → AddCircle T) (δ : ι' → ℝ),
    Tendsto δ l (𝓝[Ioi 0] 0) →
      (∀ᶠ (j : ι') in l, d ∈ closedBall (w j) (1 * δ j)) →
        Tendsto (fun j => ↑↑μ (s ∩ closedBall (w j) (δ j)) / ↑↑μ (closedBall (w j) (δ j))) l (𝓝 1)
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
δ : ι → ℝ := fun j => T / (2 * ↑(n j))
hδ₀ : ∀ᶠ (j : ι) in l, 0 < δ j
hδ₁ : Tendsto δ l (𝓝[Ioi 0] 0)
hw : ∀ᶠ (j : ι) in l, d ∈ closedBall d (1 * δ j)
⊢ Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
[PROOFSTEP]
exact hd _ δ hδ₁ hw
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
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
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
this : ∀ᶠ (j : ι) in l, ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
replace hd := hd.congr' this
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
this : ∀ᶠ (j : ι) in l, ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
hd : Tendsto (fun x => ↑↑μ s / ENNReal.ofReal T) l (𝓝 1)
⊢ ↑↑μ s = ENNReal.ofReal T
[PROOFSTEP]
rwa [tendsto_const_nhds_iff, ENNReal.div_eq_one_iff hT₁ ENNReal.ofReal_ne_top] at hd
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
⊢ ∀ᶠ (j : ι) in l, ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
refine' (hu₂.eventually_gt_atTop 0).mono fun j hj => _
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
have : addOrderOf (u j) = n j := rfl
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
have huj : IsOfFinAddOrder (u j) := addOrderOf_pos_iff.mp hj
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
have huj' : 1 ≤ (↑(n j) : ℝ) := by norm_cast
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
⊢ 1 ≤ ↑(n j)
[PROOFSTEP]
norm_cast
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
have hI₀ : μ (I j) ≠ 0 := (measure_closedBall_pos _ d <| by positivity).ne.symm
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
⊢ 0 < T / (2 * ↑(n j))
[PROOFSTEP]
positivity
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : ↑↑μ (I j) ≠ 0
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
have hI₁ : μ (I j) ≠ ⊤ := measure_ne_top _ _
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : ↑↑μ (I j) ≠ 0
hI₁ : ↑↑μ (I j) ≠ ⊤
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
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'
[GOAL]
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : ↑↑μ (I j) ≠ 0
hI₁ : ↑↑μ (I j) ≠ ⊤
⊢ ↑↑μ (I j) * ↑(n j) = ENNReal.ofReal T
[PROOFSTEP]
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']
[GOAL]
case hb
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : ↑↑μ (I j) ≠ 0
hI₁ : ↑↑μ (I j) ≠ ⊤
⊢ ↑(n j) ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr hj.ne'
[GOAL]
case inr.h.intro.intro
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : NeBot l
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 : ↑↑μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j => closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j => ↑↑μ (s ∩ I j) / ↑↑μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
hI₀ : ↑↑μ (I j) ≠ 0
hI₁ : ↑↑μ (I j) ≠ ⊤
hI₂ : ↑↑μ (I j) * ↑(n j) = ENNReal.ofReal T
⊢ ↑↑μ (s ∩ I j) / ↑↑μ (I j) = ↑↑μ s / ENNReal.ofReal T
[PROOFSTEP]
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₂]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
let u : ℕ → AddCircle T := fun j => ↑((↑1 : ℝ) / ↑(n.natAbs ^ j) * T)
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
replace hn : 1 < n.natAbs := by rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
⊢ 1 < Int.natAbs n
[PROOFSTEP]
rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
have hu₀ : ∀ j, addOrderOf (u j) = n.natAbs ^ j := fun j =>
  by
  convert addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
  norm_cast
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
j : ℕ
⊢ addOrderOf (u j) = Int.natAbs n ^ j
[PROOFSTEP]
convert addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
[GOAL]
case h.e'_2.h.e'_3.h.h.e'_4.h.e'_5.h.e'_5
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
j : ℕ
e_1✝ : AddCircle T = (ℝ ⧸ AddSubgroup.zmultiples T)
⊢ 1 = ↑1
[PROOFSTEP]
norm_cast
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
have hnu : ∀ j, n ^ j • u j = 0 := fun j => by
  rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.coe_nat_pow, Int.coe_natAbs, ← abs_pow, abs_dvd]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
j : ℕ
⊢ n ^ j • u j = 0
[PROOFSTEP]
rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.coe_nat_pow, Int.coe_natAbs, ← abs_pow, abs_dvd]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
have hu₁ : ∀ j, (u j +ᵥ s : Set _) =ᵐ[volume] s := fun j => by rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
j : ℕ
⊢ u j +ᵥ s =ᶠ[ae volume] s
[PROOFSTEP]
rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
have hu₂ : Tendsto (fun j => addOrderOf <| u j) atTop atTop := by simp_rw [hu₀];
  exact Nat.tendsto_pow_atTop_atTop_of_one_lt hn
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ Tendsto (fun j => addOrderOf (u j)) atTop atTop
[PROOFSTEP]
simp_rw [hu₀]
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
⊢ Tendsto (fun j => Int.natAbs n ^ j) atTop atTop
[PROOFSTEP]
exact Nat.tendsto_pow_atTop_atTop_of_one_lt hn
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
src✝ : MeasurePreserving fun g => n • g := measurePreserving_zsmul volume (Iff.mp abs_pos (lt_trans zero_lt_one hn✝))
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(Int.natAbs n ^ j) * T)
hn : 1 < Int.natAbs n
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = Int.natAbs n ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae volume] s
hu₂ : Tendsto (fun j => addOrderOf (u j)) atTop atTop
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ
[PROOFSTEP]
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂
[GOAL]
T : ℝ
hT : Fact (0 < T)
n : ℕ
hn : 1 < n
⊢ 1 < |↑n|
[PROOFSTEP]
simp [hn]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
⊢ Ergodic fun y => n • y + x
[PROOFSTEP]
set f : AddCircle T → AddCircle T := fun y => n • y + x
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
⊢ Ergodic f
[PROOFSTEP]
let e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x <| n - 1)
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
⊢ Ergodic f
[PROOFSTEP]
have he : MeasurePreserving e volume volume := measurePreserving_add_left volume (DivisibleBy.div x <| n - 1)
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
⊢ Ergodic f
[PROOFSTEP]
suffices e ∘ f ∘ e.symm = fun y => n • y by rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
this : ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = fun y => n • y
⊢ Ergodic f
[PROOFSTEP]
rw [← he.ergodic_conjugate_iff, this]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
this : ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = fun y => n • y
⊢ Ergodic fun y => n • y
[PROOFSTEP]
exact ergodic_zsmul h
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
⊢ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = fun y => n • y
[PROOFSTEP]
replace h : n - 1 ≠ 0
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
⊢ n - 1 ≠ 0
[PROOFSTEP]
rw [← abs_one] at h
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
⊢ n - 1 ≠ 0
[PROOFSTEP]
rw [sub_ne_zero]
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
⊢ n ≠ 1
[PROOFSTEP]
exact ne_of_apply_ne _ (ne_of_gt h)
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
⊢ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = fun y => n • y
[PROOFSTEP]
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]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
[PROOFSTEP]
conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
| x + DivisibleBy.div x (n - 1)
[PROOFSTEP]
congr; rw [← DivisibleBy.div_cancel x h]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
| x + DivisibleBy.div x (n - 1)
[PROOFSTEP]
congr; rw [← DivisibleBy.div_cancel x h]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
| x + DivisibleBy.div x (n - 1)
[PROOFSTEP]
congr
[GOAL]
case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
| x
case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)
[PROOFSTEP]
rw [← DivisibleBy.div_cancel x h]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = (n - 1) • DivisibleBy.div x (n - 1) + DivisibleBy.div x (n - 1)
[PROOFSTEP]
rw [sub_smul, one_smul, sub_add_cancel]
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
⊢ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = fun y => n • y
[PROOFSTEP]
ext y
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) y = n • y
[PROOFSTEP]
simp only [hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply, smul_add, zsmul_neg', neg_smul,
  neg_add_rev]
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y
[PROOFSTEP]
abel
[GOAL]
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving ↑e
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y
[PROOFSTEP]
abel
[GOAL]
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℕ
h : 1 < n
⊢ 1 < |↑n|
[PROOFSTEP]
simp [h]


[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
have := ofNat_pos.2 <| Nat.le_of_ble_eq_true hn
[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
have nonneg := emod_nonneg a <| Int.ne_of_gt this
[GOAL]
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ 0 ≤ toNat (a % ↑n) ∧ toNat (a % ↑n) < n ∧ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
refine ⟨Nat.zero_le _, ?_, ?_⟩
[GOAL]
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ toNat (a % ↑n) < n
[PROOFSTEP]
rw [Int.toNat_lt nonneg]
[GOAL]
case refine_1
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a % ↑n < ↑n
[PROOFSTEP]
exact Int.emod_lt_of_pos _ this
[GOAL]
case refine_2
p : Sort u_1
a : ℤ
n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
this : 0 < ↑n
nonneg : 0 ≤ a % ↑n
⊢ a ≡ ↑(toNat (a % ↑n)) [ZMOD ↑n]
[PROOFSTEP]
rw [Int.ModEq, Int.toNat_of_nonneg nonneg, emod_emod]