-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_zero_or_pos_or_neg (hf : GrowsPolynomially f) :
    (∀ᶠ x in atTop, f x = 0) ∨ (∀ᶠ x in atTop, 0 < f x) ∨ (∀ᶠ x in atTop, f x < 0)

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
simp only [lt_iff_le_and_ne]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

Tactic:
simp only [lt_iff_le_and_ne]

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
cases eventually_atTop_nonneg_or_nonpos hf with
| inl h' =>
  refine Or.inr (Or.inl ?_)
  simp only [lt_iff_le_and_ne]
  rw [eventually_and]
  exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
| inr h' =>
  refine Or.inr (Or.inr ?_)
  simp only [lt_iff_le_and_ne]
  rw [eventually_and]
  exact ⟨h', h⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
exact Or.inl <| eventually_zero_of_frequently_zero hf h

Result:
no goals

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
refine Or.inr (Or.inr ?_)

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x < 0

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
refine Or.inr (Or.inl ?_)

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ¬∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
rw [not_frequently] at h

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, ¬f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
exact ⟨h', h⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
if h : ∃ᶠ x in atTop, f x = 0 then
  exact Or.inl <| eventually_zero_of_frequently_zero hf h
else
  rw [not_frequently] at h
  push_neg at h
  cases eventually_atTop_nonneg_or_nonpos hf with
  | inl h' =>
    refine Or.inr (Or.inl ?_)
    simp only [lt_iff_le_and_ne]
    rw [eventually_and]
    exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
  | inr h' =>
    refine Or.inr (Or.inr ?_)
    simp only [lt_iff_le_and_ne]
    rw [eventually_and]
    exact ⟨h', h⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
filter_upwards [h] with x hx

Result:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : f x ≠ 0
⊢ 0 ≠ f x

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0

Tactic:
rw [eventually_and]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, ¬f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
push_neg at h

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x

Tactic:
rw [eventually_and]

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Proof state:
case h
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : f x ≠ 0
⊢ 0 ≠ f x

Tactic:
exact hx.symm

Result:
no goals