-- Mathlib/NumberTheory/WellApproximable.lean
theorem addWellApproximable_ae_empty_or_univ (δ : ℕ → ℝ) (hδ : Tendsto δ atTop (𝓝 0)) :
    (∀ᵐ x, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ x, addWellApproximable 𝕊 δ x

Proof state:
case mk.intro.intro
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * 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 ∧ 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 ⟨p, hp⟩
f : 𝕊 → 𝕊 := fun y => p • y + x
n : ℕ
hn : 0 < n
h_div : p ∣ n
h_ndiv : ¬p * p ∣ n
h_cop : (addOrderOf x).Coprime (n / p)
⊢ (⇑(sSupHom.setImage f) ∘ X) n ≤ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
replace h_div : n / p * p = n := Nat.div_mul_cancel h_div

Result:
case mk.intro.intro
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * 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 ∧ 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 ⟨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
⊢ (⇑(sSupHom.setImage f) ∘ X) n ≤ approxAddOrderOf 𝕊 n (↑p * δ n)

Proof state:
case neg.h
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * 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 ∧ 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 volume] univ

Tactic:
simp only [not_forall, not_and_or] at h

Result:
case neg.h
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup Irreducible
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p => ↑(↑1 / ↑↑p * 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 ∧ 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 : ∃ x, ¬A ↑x =ᶠ[ae μ] ∅ ∨ ¬B ↑x =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae volume] univ