-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma abs (hf : GrowsPolynomially f) : GrowsPolynomially (fun x => |f x|)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ -f =ᶠ[atTop] fun x => |f x|

Tactic:
filter_upwards [hf'] with x hx

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

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially (-f)

Tactic:
exact hf.neg

Result:
no goals

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially fun x => |f x|

Tactic:
rw [← iff_eventuallyEq hmain]

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially f

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ f =ᶠ[atTop] fun x => |f x|

Tactic:
filter_upwards [hf'] with x hx

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

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun x => |f x|

Tactic:
have hmain : -f =ᶠ[atTop] fun x => |f x| := by
  filter_upwards [hf'] with x hx
  simp only [Pi.neg_apply, abs_of_nonpos hx]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially fun x => |f x|

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially f

Tactic:
exact hf

Result:
no goals

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x => |f x|

Tactic:
cases eventually_atTop_nonneg_or_nonpos hf with
| inl hf' =>
  have hmain : f =ᶠ[atTop] fun x => |f x| := by
    filter_upwards [hf'] with x hx
    rw [abs_of_nonneg hx]
  rw [← iff_eventuallyEq hmain]
  exact hf
| inr hf' =>
  have hmain : -f =ᶠ[atTop] fun x => |f x| := by
    filter_upwards [hf'] with x hx
    simp only [Pi.neg_apply, abs_of_nonpos hx]
  rw [← iff_eventuallyEq hmain]
  exact hf.neg

Result:
no goals

Proof state:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => |f x|

Tactic:
have hmain : f =ᶠ[atTop] fun x => |f x| := by
  filter_upwards [hf'] with x hx
  rw [abs_of_nonneg hx]

Result:
case inl
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially fun x => |f x|

Proof state:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially fun x => |f x|

Tactic:
rw [← iff_eventuallyEq hmain]

Result:
case inr
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun x => |f x|
⊢ GrowsPolynomially (-f)

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

Tactic:
rw [abs_of_nonneg hx]

Result:
no goals

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

Tactic:
simp only [Pi.neg_apply, abs_of_nonpos hx]

Result:
no goals