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 : ℕ)
h_mono : Monotone (α := { p : ℕ // Nat.Prime p }) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p))
⊢ Tendsto (α := Nat.Primes) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p)) atTop atTop
have refine : ∀ (n : ℕ), ∃ (a : { p : ℕ // Nat.Prime p }), n ≤ (↑a : ℕ)
Tactic: refine h_mono.tendsto_atTop_atTop fun n => ?_
-- 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 : ℕ)
h_mono : Monotone (α := { p : ℕ // Nat.Prime p }) (Subtype.val (p := fun (p : ℕ) ↦ Nat.Prime p))
n : ℕ
⊢ ∃ (a : { p : ℕ // Nat.Prime p }), n ≤ (↑a : ℕ)
have obtain : ∀ (p : ℕ) (hp : n ≤ p) (hp' : Nat.Prime p), ∃ (a : { p : ℕ // Nat.Prime p }), n ≤ (↑a : ℕ)
Tactic: obtain ⟨p, hp, hp'⟩ := n.exists_infinite_primes
-- 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 : ℕ)
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ (x : 𝕊) ∂μ, addWellApproximable 𝕊 δ x
have hu : Tendsto (addOrderOf ∘ u) atTop atTop
Tactic: have hu : Tendsto (addOrderOf ∘ u) atTop atTop := by
    rw [(funext hu₀ : addOrderOf ∘ u = (↑))]
    have h_mono : Monotone ((↑) : Nat.Primes → ℕ) := fun p q hpq => hpq
    refine h_mono.tendsto_atTop_atTop fun n => ?_
    obtain ⟨p, hp, hp'⟩ := n.exists_infinite_primes
    exact ⟨⟨p, hp'⟩, hp⟩
-- 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
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
have hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
Tactic: have hA₀ : ∀ p, MeasurableSet (A p) := fun p =>
    MeasurableSet.measurableSet_blimsup fun n _ => isOpen_thickening.measurableSet
-- 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)
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
have hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
Tactic: have hB₀ : ∀ p, MeasurableSet (B p) := fun p =>
    MeasurableSet.measurableSet_blimsup fun n _ => isOpen_thickening.measurableSet
-- 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)
⊢ NullMeasurableSet E μ
have refine : ∀ (n : ℕ) (hn : 0 < n), IsOpen (X := 𝕊) (approxAddOrderOf 𝕊 n (δ n))
Tactic: refine (MeasurableSet.measurableSet_blimsup fun n hn =>
      IsOpen.measurableSet ?_).nullMeasurableSet
-- 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)
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x
have hE₀ : NullMeasurableSet E μ
Tactic: have hE₀ : NullMeasurableSet E μ := by
    refine (MeasurableSet.measurableSet_blimsup fun n hn =>
      IsOpen.measurableSet ?_).nullMeasurableSet
    exact isOpen_thickening
-- 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 μ
p : ℕ
⊢ E = A p ∪ B p ∪ C p
have simp : (blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)) atTop fun (n : ℕ) ↦ 0 < n) =
  blimsup X atTop fun (x : ℕ) ↦ 0 < x ∧ ((¬p ∣ x ∨ p ∣ x ∧ ¬p * p ∣ x) ∨ p * p ∣ x)
Tactic: simp only [E, A, B, C, addWellApproximable, ← blimsup_or_eq_sup, ← and_or_left, ← sup_eq_union,
      sq]
-- 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 μ
p : ℕ
⊢ (blimsup (fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)) atTop fun (n : ℕ) ↦ 0 < n) =
    blimsup X atTop fun (x : ℕ) ↦ 0 < x ∧ ((¬p ∣ x ∨ p ∣ x ∧ ¬p * p ∣ x) ∨ p * p ∣ x)
have e_p : Eq (α := ℕ → Prop) (fun (n : ℕ) ↦ 0 < n) fun (x : ℕ) ↦ 0 < x ∧ ((¬p ∣ x ∨ p ∣ x ∧ ¬p * p ∣ x) ∨ p * p ∣ x)
Tactic: congr
-- 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 μ
p : ℕ
⊢ Eq (α := ℕ → Prop) (fun (n : ℕ) ↦ 0 < n) fun (x : ℕ) ↦ 0 < x ∧ ((¬p ∣ x ∨ p ∣ x ∧ ¬p * p ∣ x) ∨ p * p ∣ x)
have e_p : ∀ (n : ℕ), 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
Tactic: ext n
-- 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 μ
p n : ℕ
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₄ : 0 < n → 0 < n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₆ : 0 < n → ¬p ∣ n → 0 < n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
e_p₆ : 0 < n → ¬p ∣ n → 0 < n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₇ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
e_p₆ : 0 < n → ¬p ∣ n → 0 < n
e_p₇ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₈ : 0 < n → p * p ∣ n → 0 < n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
e_p₆ : 0 < n → ¬p ∣ n → 0 < n
e_p₇ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₈ : 0 < n → p * p ∣ n → 0 < n
e_p₉ : 0 < n → ¬p ∣ n → 0 < n
e_p₁₀ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₁₁ : 0 < n → p * p ∣ n → 0 < n
e_p₁₂ : 0 < n → ¬p ∣ n → 0 < n
e_p₁₃ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₁₄ : 0 < n → p * p ∣ n → 0 < n
e_p₁₅ e_p₁₆ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₁₇ : 0 < n → ¬(¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) → p * p ∣ n
Tactic: tauto
-- 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 μ
p n : ℕ
e_p : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₁ : 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n) → 0 < n
e_p₂ e_p₃ : 0 < n → 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
e_p₄ : 0 < n → 0 < n
e_p₅ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
e_p₆ : 0 < n → ¬p ∣ n → 0 < n
e_p₇ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₈ : 0 < n → p * p ∣ n → 0 < n
e_p₉ : 0 < n → ¬p ∣ n → 0 < n
e_p₁₀ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₁₁ : 0 < n → p * p ∣ n → 0 < n
e_p₁₂ : 0 < n → ¬p ∣ n → 0 < n
e_p₁₃ : 0 < n → p ∣ n → ¬p * p ∣ n → 0 < n
e_p₁₄ : 0 < n → p * p ∣ n → 0 < n
e_p₁₅ e_p₁₆ : 0 < n → (¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n
e_p₁₇ : 0 < n → ¬(¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) → p * p ∣ n
⊢ 0 < n ↔ 0 < n ∧ ((¬p ∣ n ∨ p ∣ n ∧ ¬p * p ∣ n) ∨ p * p ∣ n)
have e_p₁₈ : 0 < n → ¬¬p ∣ n → ¬(p ∣ n ∧ ¬p * p ∣ n) → p * p ∣ n
Tactic: tauto