awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
rw : Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
⊢ Subset (α := Set 𝕊) ((sSupHom.setImage f : (a : Set 𝕊) → Set 𝕊) (X n) : Set 𝕊)
    (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n) : Set 𝕊)

Tactic:
rw [sSupHom.setImage_toFun, hf, image_comp]

Premises used: sSupHom.setImage_toFun, Set.image_comp
-- 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
hf : f = (fun (y : 𝕊) ↦ x + y) ∘ fun (y : 𝕊) ↦ p • y
⊢ Monotone (α := Set 𝕊) (β := Set 𝕊) (image fun (y : 𝕊) ↦ x + y)

Tactic:
have := @monotone_image 𝕊 𝕊 fun y => x + y
-- 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
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)
⊢ 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)

Premises used: HDiv.hDiv, Nat.Prime.pos, approxAddOrderOf.image_nsmul_subset
-- 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
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))
⊢ 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 ⊢
-- 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
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))

Tactic:
this.trans ?_

Premises used: LE.le.trans
-- 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
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))
refine :
  LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
    (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))
⊢ Subset (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' (fun (y : 𝕊) ↦ p • y) '' X n) (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- 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
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))
⊢ HVAdd.hVAdd (β := Set 𝕊) x (approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n)) ⊆
    approxAddOrderOf 𝕊 (addOrderOf x * (n / p)) ((↑p : ℝ) * δ n)

Tactic:
approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop

Premises used: HMul.hMul, Nat.cast, approxAddOrderOf.vadd_subset_of_coprime
-- 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
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 = addOrderOf x * (n / p)
⊢ LE.le (α := Set 𝕊) ((fun (y : 𝕊) ↦ x + y) '' approxAddOrderOf 𝕊 (n / p) ((↑p : ℝ) * δ n))
    (approxAddOrderOf 𝕊 n ((↑p : ℝ) * δ n))

Tactic:
convert! approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop

Premises used: HMul.hMul, Nat.cast, approxAddOrderOf.vadd_subset_of_coprime
-- 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
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
h₃ h₄ : n = n
⊢ n = addOrderOf x * (n / p)

Tactic:
rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]

Premises used: Subtype.coe_mk, mul_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 : 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]
-- 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
change : (∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae (F := Measure 𝕊) volume
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x

Tactic:
change (∀ᵐ x, x ∉ E) ∨ E ∈ ae volume

Premises used: MeasureTheory.ae, Filter.Eventually, Membership.mem, MeasureTheory.MeasureSpace.volume, 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
rw : E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ (∀ᵐ (x : 𝕊), x ∉ E) ∨ E ∈ ae (F := Measure 𝕊) volume

Tactic:
rw [← eventuallyEq_empty, ← eventuallyEq_univ]

Premises used: Filter.eventuallyEq_empty, Filter.eventuallyEq_univ
-- 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
change : (e : (a : Set 𝕊) → Set 𝕊) (C (↑p : ℕ)) = C (↑p : ℕ)
⊢ u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)

Tactic:
change e (C p) = C p

Premises used: Subtype.val, DFunLike.coe