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

Proof state:
case neg.h.intro.inr
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
p : Nat.Primes
h✝ : ¬B ↑p =ᶠ[ae μ] ∅
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᶠ[ae volume] univ

Tactic:
rcases hB p with _ | h

Result:
case neg.h.intro.inr.inl
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
p : Nat.Primes
h✝¹ : ¬B ↑p =ᶠ[ae μ] ∅
h✝ : B ↑p =ᶠ[ae μ] ∅
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᶠ[ae volume] univ

case neg.h.intro.inr.inr
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
p : Nat.Primes
h✝ : ¬B ↑p =ᶠ[ae μ] ∅
h : B ↑p =ᶠ[ae μ] univ
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᶠ[ae volume] univ

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
hA : ∀ (p : Nat.Primes), A ↑p =ᶠ[ae μ] ∅ ∨ A ↑p =ᶠ[ae μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ u p +ᵥ C ↑p = C ↑p

Tactic:
change e (C p) = C p

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
hB : ∀ (p : Nat.Primes), B ↑p =ᶠ[ae μ] ∅ ∨ B ↑p =ᶠ[ae μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ e (C ↑p) = C ↑p

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
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y => p • y
this : f '' A p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n => 0 < n ∧ ¬p ∣ n
⊢ A ↑⟨p, hp⟩ =ᶠ[ae μ] ∅ ∨ A ↑⟨p, hp⟩ =ᶠ[ae μ] univ

Tactic:
apply (ergodic_nsmul hp.one_lt).ae_empty_or_univ_of_image_ae_le (hA₀ p).nullMeasurableSet

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
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y => p • y
this : f '' A p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (↑p * δ n)) atTop fun n => 0 < n ∧ ¬p ∣ n
⊢ (fun y => p • y) '' A p ≤ᶠ[ae volume] A p