awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this_1 : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
this :
  LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n))
    ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
⊢ n = addOrderOf x * (n / p)
have h : n = (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) * (n / p)
Tactic: rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this_1 : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
this :
  LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n))
    ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
h : n = (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) * (n / p)
⊢ n = addOrderOf x * (n / p)
have h₁ : n = p * (n / p)
Tactic: rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this_1 : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
this :
  LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n))
    ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
h : n = (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) * (n / p)
h₁ : n = p * (n / p)
⊢ n = addOrderOf x * (n / p)
have h₂ : n = n / p * p
Tactic: rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this_1 : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
n : ℕ
hn : 0 < n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
h_div : n / p * p = n
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
this :
  LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n))
    ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
h : n = (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) * (n / p)
h₁ : n = p * (n / p)
h₂ : n = n / p * p
⊢ n = addOrderOf x * (n / p)
have h₃ : n = n
Tactic: rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
have hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
Tactic: have hB : ∀ p : Nat.Primes, B p =ᵐ[μ] (∅ : Set 𝕊) ∨ B p =ᵐ[μ] univ := by
    rintro ⟨p, hp⟩
    let x := u ⟨p, hp⟩
    let f : 𝕊 → 𝕊 := fun y => p • y + x
    suffices
      f '' B p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (p * δ n)) atTop fun n => 0 < n ∧ p∣∣n by
      apply (ergodic_nsmul_add x hp.one_lt).ae_empty_or_univ_of_image_ae_le
        (hB₀ p).nullMeasurableSet
      apply (HasSubset.Subset.eventuallyLE this).congr EventuallyEq.rfl
      exact blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∣∣n) (fun n => {y | addOrderOf y = n})
        (Nat.cast_pos.mpr hp.pos) _ hδ
    refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)
    rintro n ⟨hn, h_div, h_ndiv⟩
    have h_cop : (addOrderOf x).Coprime (n / p) := by
      obtain ⟨q, rfl⟩ := h_div
      rw [hu₀, Subtype.coe_mk, hp.coprime_iff_not_dvd, q.mul_div_cancel_left hp.pos]
      exact fun contra => h_ndiv (mul_dvd_mul_left p contra)
    replace h_div : n / p * p = n := Nat.div_mul_cancel h_div
    have hf : f = (fun y => x + y) ∘ fun y => p • y := by
      ext; simp [f, add_comm x]
    simp_rw [Function.comp_apply, le_eq_subset]
    rw [sSupHom.setImage_toFun, hf, image_comp]
    have := @monotone_image 𝕊 𝕊 fun y => x + y
    specialize this (approxAddOrderOf.image_nsmul_subset (δ n) (n / p) hp.pos)
    simp only [h_div] at this ⊢
    refine this.trans ?_
    convert! approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop
    rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
have change : (∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae (F := Measure 𝕊) volume
Tactic: change (∀ᵐ x, x ∉ E) ∨ E ∈ ae volume
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
⊢ (∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae (F := Measure 𝕊) volume
have rw : E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rw [← eventuallyEq_empty, ← eventuallyEq_univ]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
have change : (e : (a : Set 𝕊) → Set 𝕊) (C (↑p : ℕ)) = C (↑p : ℕ)
Tactic: change e (C p) = C p
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ (e : (a : Set 𝕊) → Set 𝕊) (C (↑p : ℕ)) = C (↑p : ℕ)
have rw : (blimsup ((⇑e : (a : Set 𝕊) → Set 𝕊) ∘ X) atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) (addOrderOf (u p)) 2 ∣ n) =
  C (addOrderOf (u p))
Tactic: rw [OrderIso.apply_blimsup e, ← hu₀ p]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
Tactic: have hC : ∀ p : Nat.Primes, u p +ᵥ C p = C p := by
    intro p
    let e := (AddAction.toPerm (u p) : Equiv.Perm 𝕊).toOrderIsoSet
    change e (C p) = C p
    rw [OrderIso.apply_blimsup e, ← hu₀ p]
    exact blimsup_congr (Eventually.of_forall fun n hn =>
      approxAddOrderOf.vadd_eq_of_mul_dvd (δ n) hn.1 hn.2)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have pos : ∀ (h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅),
  E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: by_cases! +distrib h : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
pos :
  ∀ (h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅),
    E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : ∀ (h : ∃ (p : Nat.Primes), ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅),
  E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: by_cases! +distrib h : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊)
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅
p : Nat.Primes
⊢ u p +ᵥ E =ᶠ[ae μ] E
have hE₃ : E =ᶠ[ae μ] C (↑p : ℕ)
Tactic: replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)
Cleared hypotheses: hE₂
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅
p : Nat.Primes
hE₂ : E =ᶠ[ae μ] C (↑p : ℕ)
⊢ u p +ᵥ E =ᶠ[ae μ] E
have h_qmp : Measure.QuasiMeasurePreserving (fun (x : 𝕊) ↦ -u p +ᵥ x) μ μ
Tactic: have h_qmp : Measure.QuasiMeasurePreserving (-u p +ᵥ ·) μ μ :=
        (measurePreserving_vadd _ μ).quasiMeasurePreserving