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
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 : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ E =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
rw [hE₁ p]

Premises used: Subtype.val
-- 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
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
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

Tactic:
cases hp
-- 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
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
neg₁ : ∀ (h : A (↑p : ℕ) =ᶠ[ae μ] univ), A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
rcases hA p with _ | 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
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 μ] ∅
h_1 : A (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
contradiction
-- 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
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h_1 : ¬A (↑p : ℕ) =ᶠ[ae μ] ∅
h : A (↑p : ℕ) =ᶠ[ae μ] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left]

Premises used: MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_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
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
neg₁ : ∀ (h : B (↑p : ℕ) =ᶠ[ae μ] univ), A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
rcases hB p with _ | 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
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 μ] ∅
h_1 : B (↑p : ℕ) =ᶠ[ae μ] ∅
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
contradiction
-- 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
hC : ∀ (p : Nat.Primes), u p +ᵥ C (↑p : ℕ) = C (↑p : ℕ)
p : Nat.Primes
h_1 : ¬B (↑p : ℕ) =ᶠ[ae μ] ∅
h : B (↑p : ℕ) =ᶠ[ae μ] univ
⊢ A (↑p : ℕ) ∪ B (↑p : ℕ) ∪ C (↑p : ℕ) =ᶠ[ae (F := Measure 𝕊) volume] univ

Tactic:
simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left,
        union_ae_eq_univ_of_ae_eq_univ_right]

Premises used: MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left, MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right
-- Module: Mathlib.NumberTheory.WellApproximable
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 0 n) : Type)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)

Tactic:
have hB : ∀ j, IsClosed (B j) := fun j ↦ isClosed_closedBall
-- Module: Mathlib.NumberTheory.WellApproximable
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)
obtain : ∀ (i j : (↑(Icc 0 n) : Type)) (hij : i < j) (x : A) (hx : x ∈ B i ∩ B j), ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this

Premises used: exists_lt_mem_inter_of_not_pairwise_disjoint
-- Module: Mathlib.NumberTheory.WellApproximable
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 • ξ‖ ≤ δ

Tactic:
⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩

Premises used: le_tsub_of_add_le_left, HSub.hSub, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.NumberTheory.WellApproximable
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
refine_2 : ‖((↑j : ℕ) - (↑i : ℕ)) • ξ‖ ≤ δ
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.WellApproximable
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 : ℕ) ≤ n

Tactic:
simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add

Premises used: tsub_le_iff_right, And.right, LE.le.trans, le_self_add, Subtype.property
-- Module: Mathlib.NumberTheory.WellApproximable
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_2 : dist ((↑j : ℕ) • ξ) ((↑i : ℕ) • ξ) ≤ δ
⊢ ‖((↑j : ℕ) - (↑i : ℕ)) • ξ‖ ≤ δ

Tactic:
rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]

Premises used: Iff.mpr, dist_eq_norm, sub_eq_add_neg, Subtype.coe_le_coe, LT.lt.le, sub_nsmul
-- Module: Mathlib.NumberTheory.WellApproximable
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
linarith : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
linarith₁ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
linarith₃ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → 2 / 2 = 1
linarith₄ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
linarith₆ :
  δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) →
    2 * (δ - (dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ))) + (2 * dist x ((↑i : ℕ) • ξ) - 1 * δ) +
        (2 * dist ((↑j : ℕ) • ξ) x - 1 * δ) =
      0
linarith₇ : δ < dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) → GT.gt (α := ℝ) 2 0
⊢ dist ((↑j : ℕ) • ξ) x + dist x ((↑i : ℕ) • ξ) ≤ δ

Tactic:
linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2]

Premises used: Metric.mem_closedBall', And.right, And.left, Iff.mp, Metric.mem_closedBall
-- Module: Mathlib.NumberTheory.WellApproximable
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 : ℕ) • ξ) ((↑i : ℕ) • ξ) ≤ δ

Tactic:
exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])

Premises used: dist_triangle, HSMul.hSMul, LE.le.trans, Subtype.val
-- Module: Mathlib.NumberTheory.WellApproximable
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)
suffices : ¬Pairwise (Disjoint on B)
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
suffices ¬ Pairwise (Disjoint on B) by
    obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])
-- Module: Mathlib.NumberTheory.WellApproximable
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)
by_contra : ∀ (h : Pairwise (Disjoint on B)), False
⊢ ¬Pairwise (Disjoint on B)

Tactic:
by_contra h
-- Module: Mathlib.NumberTheory.WellApproximable
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)
h : Pairwise (Disjoint on B)
apply : n = 0
⊢ False

Tactic:
apply hn.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.WellApproximable
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)
h : Pairwise (Disjoint on B)
rw :
  Eq (α := ENNReal) ((μ : (a : Set A) → ENNReal) (⋃ (i : (↑(Icc 0 n) : Type)), B i) : ENNReal)
    ((μ : (a : Set A) → ENNReal) univ : ENNReal)
⊢ Eq.{u_1 + 1} (α := Set A) (⋃ (j : (↑(Icc 0 n) : Type)), B j) univ

Tactic:
rw [← (isClosed_iUnion_of_finite hB).measure_eq_univ_iff_eq (μ := μ)]

Premises used: isClosed_iUnion_of_finite, IsClosed.measure_eq_univ_iff_eq