awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.WellApproximable
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
this :
  f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
apply :
  (blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦
      0 < n ∧ p ∣ n ∧ ¬p * p ∣ n) =ᶠ[ae (F := Measure 𝕊) volume]
    B p
⊢ (fun (y : 𝕊) ↦ p • y + x) '' B p ≤ᶠ[ae (F := Measure 𝕊) volume] B p

Tactic:
apply (HasSubset.Subset.eventuallyLE this).congr EventuallyEq.rfl

Premises used: HasSubset.Subset.eventuallyLE, Filter.EventuallyLE.congr, Filter.EventuallyEq.rfl
-- Module: Mathlib.NumberTheory.WellApproximable
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
this :
  f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
⊢ (blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦
      0 < n ∧ p ∣ n ∧ ¬p * p ∣ n) =ᶠ[ae (F := Measure 𝕊) volume]
    B p

Tactic:
blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∣∣n) (fun n => {y | addOrderOf y = n})
        (Nat.cast_pos.mpr hp.pos) _ hδ

Premises used: Iff.mpr, Dvd.dvd, Nat.cast_pos, HMul.hMul, addOrderOf, setOf, Nat.Prime.pos, And, approxAddOrderOf, LT.lt, blimsup_thickening_mul_ae_eq, OfNat.ofNat, Eq, Not
-- Module: Mathlib.NumberTheory.WellApproximable
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
this :
  f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
⊢ (blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦
      0 < n ∧ p ∣ n ∧ ¬p * p ∣ n) =ᶠ[ae (F := Measure 𝕊) volume]
    B p

Tactic:
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δ

Premises used: Iff.mpr, Dvd.dvd, Nat.cast_pos, HMul.hMul, addOrderOf, setOf, Nat.Prime.pos, And, LT.lt, blimsup_thickening_mul_ae_eq, OfNat.ofNat, Eq, Not
-- Module: Mathlib.NumberTheory.WellApproximable
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₁ :
  f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
⊢ 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

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δ
-- Module: Mathlib.NumberTheory.WellApproximable
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

Tactic:
(sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)

Premises used: sSupHom.setImage, Set.Mem, setOf, Filter.mono_blimsup, Set.image, LE.le.trans, sSupHom.apply_blimsup_le
-- Module: Mathlib.NumberTheory.WellApproximable
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
refine :
  ∀ (x : ℕ),
    0 < x ∧ p ∣ x ∧ ¬p * p ∣ x →
      LE.le (α := Set 𝕊) (((⇑(sSupHom.setImage f) : (a : Set 𝕊) → Set 𝕊) ∘ X) x) (approxAddOrderOf 𝕊 x ((↑p : ℝ) * δ x))
⊢ f '' B p ⊆
    blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n)) atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n

Tactic:
refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)

Premises used: sSupHom.setImage, Filter.mono_blimsup, LE.le.trans, sSupHom.apply_blimsup_le
-- Module: Mathlib.NumberTheory.WellApproximable
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
obtain : ∀ (q : ℕ) (hn : 0 < p * q) (h_ndiv : ¬p * p ∣ p * q), (addOrderOf x).Coprime (p * q / p)
⊢ (addOrderOf x).Coprime (n / p)

Tactic:
obtain ⟨q, rfl⟩ := h_div

Premises used: rfl
-- Module: Mathlib.NumberTheory.WellApproximable
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
rw : ¬p ∣ q
⊢ (addOrderOf x).Coprime (p * q / p)

Tactic:
rw [hu₀, Subtype.coe_mk, hp.coprime_iff_not_dvd, q.mul_div_cancel_left hp.pos]

Premises used: Subtype.coe_mk, Nat.mul_div_cancel_left, Nat.Prime.pos, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ ¬p ∣ q

Tactic:
fun contra => h_ndiv (mul_dvd_mul_left p contra)

Premises used: mul_dvd_mul_left, Not
-- Module: Mathlib.NumberTheory.WellApproximable
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
⊢ ¬p ∣ q

Tactic:
exact fun contra => h_ndiv (mul_dvd_mul_left p contra)

Premises used: mul_dvd_mul_left
-- Module: Mathlib.NumberTheory.WellApproximable
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)

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)
-- Module: Mathlib.NumberTheory.WellApproximable
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)
⊢ n / p * p = n

Tactic:
replace h_div : n / p * p = n := Nat.div_mul_cancel h_div
-- Module: Mathlib.NumberTheory.WellApproximable
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
h : ∀ (x_1 : 𝕊), f x_1 = ((fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y) x_1
⊢ f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y

Tactic:
ext
-- Module: Mathlib.NumberTheory.WellApproximable
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
x_1 : 𝕊
⊢ f x_1 = ((fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y) x_1

Tactic:
simp [f, add_comm x]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.WellApproximable
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

Tactic:
have hf : f = (fun y => x + y) ∘ fun y => p • y := by
      ext; simp [f, add_comm x]