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 : 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
⊢ B (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) =ᶠ[ae μ] ∅ ∨
    B (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp) : ℕ) =ᶠ[ae μ] univ
have f₁ : f '' B p ⊆ blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
Tactic: 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δ
-- 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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
⊢ f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
have refine : ∀ (x : ℕ),
  0 < x ∧ p ∣ x ∧ ¬p * p ∣ x →
    LE.le (α := Set 𝕊) (((⇑(sSupHom.setImage f) : (a : Set 𝕊) → Set 𝕊) ∘ X) x) (approxAddOrderOf 𝕊 x ((↑p : ℝ) * δ x))
Tactic: refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)
-- 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
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_div : p ∣ n
h_ndiv : ¬p * p ∣ n
⊢ (addOrderOf x).Coprime (n / p)
have obtain : ∀ (q : ℕ) (hn : 0 < p * q) (h_ndiv : ¬p * p ∣ p * q), (addOrderOf x).Coprime (p * q / p)
Tactic: obtain ⟨q, rfl⟩ := h_div
Cleared hypotheses: n, hn, h_div, h_ndiv
-- 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
p : ℕ
hp : Nat.Prime p
x : 𝕊 := u (Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp)
f : 𝕊 → 𝕊 := fun (y : 𝕊) ↦ p • y + x
q : ℕ
hn : 0 < p * q
h_ndiv : ¬p * p ∣ p * q
⊢ (addOrderOf x).Coprime (p * q / p)
have rw : ¬p ∣ q
Tactic: rw [hu₀, Subtype.coe_mk, hp.coprime_iff_not_dvd, q.mul_div_cancel_left hp.pos]
-- 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
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_div : p ∣ n
h_ndiv : ¬p * p ∣ n
⊢ LE.le (α := Set 𝕊) (((⇑(sSupHom.setImage f) : (a : Set 𝕊) → Set 𝕊) ∘ X) n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have h_cop : (addOrderOf x).Coprime (n / p)
Tactic: 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)
-- 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
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_div : p ∣ n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
⊢ LE.le (α := Set 𝕊) (((⇑(sSupHom.setImage f) : (a : Set 𝕊) → Set 𝕊) ∘ X) n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have h_div₁ : n / p * p = n
Tactic: replace h_div : n / p * p = n := Nat.div_mul_cancel h_div
Cleared hypotheses: 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
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
⊢ f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
have h : ∀ (x_1 : 𝕊), f x_1 = ((fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y) x_1
Tactic: ext
-- 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
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
⊢ LE.le (α := Set 𝕊) (((⇑(sSupHom.setImage f) : (a : Set 𝕊) → Set 𝕊) ∘ X) n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
Tactic: have hf : f = (fun y => x + y) ∘ fun y => p • y := by
      ext; simp [f, add_comm x]
-- 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
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
⊢ Subset (α := Set 𝕊) ((sSupHom.setImage f : (a : Set 𝕊) → Set 𝕊) (X n) : Set 𝕊)
    (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n) : Set 𝕊)
have rw : Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
Tactic: rw [sSupHom.setImage_toFun, hf, image_comp]
-- 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
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
⊢ Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have this₁ : Monotone (α := Set 𝕊) (β := Set 𝕊) (image fun (y : 𝕊) ↦ x + y)
Tactic: have := @monotone_image 𝕊 𝕊 fun y => x + y
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
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 : Monotone (α := Set 𝕊) (β := Set 𝕊) (image fun (y : 𝕊) ↦ x + y)
⊢ Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have this₁ : LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 (n / p * p) (δ n))
  ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
Tactic: specialize this (approxAddOrderOf.image_nsmul_subset (δ n) (n / p) hp.pos)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
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 / p * p) (δ n))
    ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
⊢ Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have this₁ : LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' approxAddOrderOf 𝕊 n (δ n))
  ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
Tactic: simp only [h_div] at this ⊢
Cleared hypotheses: this
-- 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))
⊢ Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have refine : LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
  (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
Tactic: refine this.trans ?_
-- 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))
⊢ LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
    (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
have h : n = addOrderOf x * (n / p)
Tactic: convert! approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop