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
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅
p : Nat.Primes
hE₂ : E =ᶠ[ae μ] C (↑p : ℕ)
h_qmp : Measure.QuasiMeasurePreserving (fun (x : 𝕊) ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ E =ᶠ[ae μ] E
have refine : u p +ᵥ C (↑p : ℕ) =ᶠ[ae μ] C (↑p : ℕ)
Tactic: refine (h_qmp.vadd_ae_eq_of_ae_eq (u p) hE₂).trans (ae_eq_trans ?_ hE₂.symm)
-- 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
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅
p : Nat.Primes
hE₂ : E =ᶠ[ae μ] C (↑p : ℕ)
h_qmp : Measure.QuasiMeasurePreserving (fun (x : 𝕊) ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ C (↑p : ℕ) =ᶠ[ae μ] C (↑p : ℕ)
have rw : C (↑p : ℕ) =ᶠ[ae μ] C (↑p : ℕ)
Tactic: rw [hC]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have h₁ : ∀ (p : Nat.Primes), u p +ᵥ E =ᶠ[ae μ] E
Tactic: replace h : ∀ p : Nat.Primes, (u p +ᵥ E : Set _) =ᵐ[μ] E := by
      intro p
      replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)
      have h_qmp : Measure.QuasiMeasurePreserving (-u p +ᵥ ·) μ μ :=
        (measurePreserving_vadd _ μ).quasiMeasurePreserving
      refine (h_qmp.vadd_ae_eq_of_ae_eq (u p) hE₂).trans (ae_eq_trans ?_ hE₂.symm)
      rw [hC]
Cleared hypotheses: 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∃ (p : Nat.Primes), ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] ∅ ∨ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : E =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
h : ∃ (p : Nat.Primes), ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : ∀ (p : Nat.Primes) (hp : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅), E =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: obtain ⟨p, hp⟩ := h
Cleared hypotheses: 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
hp : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rw [hE₁ p]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
hp : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: cases hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
hp : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
neg : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg₁ : ¬B (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: cases hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun (p : ℕ) ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 :=
  fun (p : Nat.Primes) ↦ (↑(HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(↑p : ℕ) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = (↑p : ℕ)
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun (n : ℕ) ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun (p : ℕ) ↦ blimsup X atTop fun (n : ℕ) ↦ 0 < n ∧ HPow.hPow (β := ℕ) p 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∧ B (↑p : ℕ) =ᶠ[ae μ] ∅ → E =ᶠ[ae μ] C (↑p : ℕ)
hA : ∀ (p : Nat.Primes), A (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ A (↑p : ℕ) =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : A (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rcases hA p with _ | 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅
neg : A (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg₁ : ∀ (h : A (↑p : ℕ) =ᶠ[ae μ] univ), A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rcases hA p with _ | 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h : ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg : B (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rcases hB p with _ | 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
hB : ∀ (p : Nat.Primes), B (↑p : ℕ) =ᶠ[ae μ] ∅ ∨ B (↑p : ℕ) =ᶠ[ae μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h : ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
neg : B (↑p : ℕ) =ᶠ[ae μ] ∅ → A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
have neg₁ : ∀ (h : B (↑p : ℕ) =ᶠ[ae μ] univ), A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
Tactic: rcases hB p with _ | h
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
have hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
Tactic: have hB : ∀ j, IsClosed (B j) := fun j ↦ isClosed_closedBall
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
have obtain : ∀ (i j : (↑(Icc 0 n) : Type)) (hij : i < j) (x : A) (hx : x ∈ B i ∩ B j), ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
Tactic: obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
have refine_1 : (↑j : ℕ) - (↑i : ℕ) ≤ n
Tactic: refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
refine_1 : (↑j : ℕ) - (↑i : ℕ) ≤ n
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
have refine_2 : ‖((↑j : ℕ) - (↑i : ℕ)) • ξ‖ ≤ δ
Tactic: refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ ‖((↑j : ℕ) - (↑i : ℕ)) • ξ‖ ≤ δ
have refine_2 : dist ((↑j : ℕ) • ξ) ((↑i : ℕ) • ξ) ≤ δ
Tactic: rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.WellApproximable (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : CompactSpace A
inst_2 : PreconnectedSpace A
inst_3 : MeasurableSpace A
inst_4 : BorelSpace A
μ : Measure A
inst_5 : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ :
  (μ : (a : Set A) → ENNReal) univ ≤
    HSMul.hSMul (β := ENNReal) (n + 1) ((μ : (a : Set A) → ENNReal) (closedBall 0 (δ / 2)) : ENNReal)
B : (↑(Icc 0 n) : Type) → Set A := fun (j : (↑(Icc 0 n) : Type)) ↦ closedBall ((↑j : ℕ) • ξ) (δ / 2)
hB : ∀ (j : (↑(Icc 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
this : ¬Pairwise (Disjoint on B)
i j : (↑(Icc 0 n) : Type)
hij : i < j
x : A
hx : x ∈ B i ∩ B j
⊢ dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) ≤ δ
have linarith : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
Tactic: linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2]