-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
refine₁ refine₂ :
  ∀ (h₁ : ¬D = 0), ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₃ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
refine₄ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D),
    ¬∃ c > 0,
        ∀ᶠ (x : ℝ) in atTop,
          c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
refine₅ refine₆ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0),
    ∃ᶠ (x : ℝ) in atTop,
      Norm.norm (E := ℝ) (1 x) < a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
refine₇ refine₈ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b : ℝ),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
refine₉ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b c : ℝ)
    (hc :
      ∀ b ≥ c,
        Norm.norm (E := ℝ) (1 b) ≤
          a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
refine₁₀ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b c : ℝ)
    (hc :
      ∀ b ≥ c,
        Norm.norm (E := ℝ) (1 b) ≤
          a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
refine₁₁ :
  ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b c : ℝ)
    (hc :
      ∀ b ≥ c,
        Norm.norm (E := ℝ) (1 b) ≤
          a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
    let ℓ := 1 + max ‖e‖ (max |b| |c|);
    ∀ (h₁ℓ : c ≤ ℓ), ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
have refine₁₂ : ∀ (h₁ : ¬D = 0) (e : E) (he : single e 1 ≤ D) (a : ℝ) (ha : a > 0) (b c : ℝ)
  (hc :
    ∀ b ≥ c,
      Norm.norm (E := ℝ) (1 b) ≤
        a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
  let ℓ := 1 + max ‖e‖ (max |b| |c|);
  ∀ (h₁ℓ : c ≤ ℓ) (h₂ℓ : 1 ≤ ℓ),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
Tactic: classical
  refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
  contrapose
  intro h₁
  obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))
  rw [isBigO_iff'']
  push Not
  intro a ha
  simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]
  intro b
  obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)
  let ℓ := 1 + max ‖e‖ (max |b| |c|)
  have h₁ℓ : c ≤ ℓ := by grind
  have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
  use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
  calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind