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

Proof state:
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
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x

Tactic:
have hA : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∨ A p =ᵐ[μ] univ := by
  rintro ⟨p, hp⟩
  let f : 𝕊 → 𝕊 := fun y => (p : ℕ) • y
  suffices
    f '' A p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (p * δ n)) atTop fun n => 0 < n ∧ p∤n by
    apply (ergodic_nsmul hp.one_lt).ae_empty_or_univ_of_image_ae_le (hA₀ 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 fun n hn => ?_)
  replace hn := Nat.coprime_comm.mp (hp.coprime_iff_not_dvd.2 hn.2)
  exact approxAddOrderOf.image_nsmul_subset_of_coprime (δ n) hp.pos hn

Result:
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
⊢ (∀ᵐ (x : 𝕊) ∂μ, ¬E x) ∨ ∀ᵐ (x : 𝕊) ∂μ, E x

Proof state:
case neg
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] ∅ ∨ E =ᶠ[ae volume] univ

Tactic:
right

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 : ¬∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∧ B ↑p =ᶠ[ae μ] ∅
⊢ E =ᶠ[ae volume] univ

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_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
⊢ (⇑(sSupHom.setImage f) ∘ X) n ≤ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
simp_rw [Function.comp_apply, le_eq_subset]

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
hf : f = (fun y => x + y) ∘ fun y => p • y
⊢ (sSupHom.setImage f) (X n) ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)