Theorem: BrunTitchmarsh.IsBigO.nat_Top_of_atTop (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ f =O[⊤] g
Tactic:
simp only [Asymptotics.isBigO_top, Real.norm_eq_abs]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : f =O[atTop] g
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
rw [Asymptotics.isBigO_atTop_iff_eventually_exists] at h
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : ∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h : ∀ᶠ (n₀ : ℕ) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
simp only [ge_iff_le, Real.norm_eq_abs, Filter.eventually_atTop] at h
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
h : ∃ a, ∀ (b : ℕ), a ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
obtain ⟨N, hN⟩ := h
State after:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∃ c, ∀ (n : ℕ), b ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
specialize hN N le_rfl
State after:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∃ c, ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
case intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
hN : ∃ c, ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
obtain ⟨c, hc⟩ := hN
State after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
let C := Finset.max' (insert c ((Finset.range N).image (fun n ↦ |f n| * |g n|⁻¹))) (by simp)
State after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|

State before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
⊢ ∃ C, ∀ (x : ℕ), |f x| ≤ C * |g x|
Tactic:
refine ⟨C, fun n ↦ ?_⟩
State after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
⊢ |f n| ≤ C * |g n|

State before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
⊢ |f n| ≤ C * |g n|
Tactic:
by_cases hn : N ≤ n
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ |f n| ≤ C * |g n|

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
⊢ |f n| ≤ C * |g n|

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
⊢ (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).Nonempty
Tactic:
simp
State after:
no goals

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ |f n| ≤ C * |g n|
Tactic:
calc |f n| ≤ c * |g n| := hc n hn
  _ ≤ C * |g n| := by
    gcongr
    apply Finset.le_max'
    simp
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c * |g n| ≤ C * |g n|
Tactic:
gcongr
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ≤ C

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ≤ C
Tactic:
apply Finset.le_max'
State after:
case h.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))

State before:
case h.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : N ≤ n
⊢ c ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))
Tactic:
simp
State after:
no goals

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
⊢ |f n| ≤ C * |g n|
Tactic:
by_cases hg : g n = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : g n = 0
⊢ |f n| ≤ C * |g n|

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| ≤ C * |g n|

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| ≤ C * |g n|
Tactic:
rw [← mul_inv_le_iff']
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ≤ C

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ≤ C

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
apply Finset.le_max'
State after:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|

State before:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ ∈ insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
simp only [Finset.mem_insert, Finset.mem_image, Finset.mem_range]
State after:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ = c ∨ ∃ a < N, |f a| * |g a|⁻¹ = |f n| * |g n|⁻¹

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|

State before:
case neg.H2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ |f n| * |g n|⁻¹ = c ∨ ∃ a < N, |f a| * |g a|⁻¹ = |f n| * |g n|⁻¹

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
exact .inr ⟨n, by omega, rfl⟩
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : g n = 0
⊢ |f n| ≤ C * |g n|
Tactic:
simp [hg, h0]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ n < N
Tactic:
omega
State after:
no goals

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
f g : ℕ → ℝ
h0 : ∀ (n : ℕ), g n = 0 → f n = 0
N : ℕ
c : ℝ
hc : ∀ (n : ℕ), N ≤ n → |f n| ≤ c * |g n|
C : ℝ := (insert c (Finset.image (fun n => |f n| * |g n|⁻¹) (Finset.range N))).max' ⋯
n : ℕ
hn : ¬N ≤ n
hg : ¬g n = 0
⊢ 0 < |g n|
Tactic:
simp [hg]
State after:
no goals