awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : 0 ≤ f x
h h₁ : f x = f x
⊢ f x = |f x|

Tactic:
rw [abs_of_nonneg hx]

Premises used: abs_of_nonneg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ f =ᶠ[atTop] 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]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
inl : GrowsPolynomially f
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|

Tactic:
rw [← iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
⊢ GrowsPolynomially f

Tactic:
hf
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hmain : f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
⊢ GrowsPolynomially f

Tactic:
exact hf
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
h : ∀ (x : ℝ) (hx : f x ≤ 0), (-f) x = |f x|
⊢ -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|

Tactic:
filter_upwards [hf'] with x hx
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
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]

Premises used: abs_of_nonpos, Pi.neg_apply
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ -f =ᶠ[atTop] 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]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
inr : GrowsPolynomially (-f)
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|

Tactic:
rw [← iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
⊢ GrowsPolynomially (-f)

Tactic:
hf.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
⊢ GrowsPolynomially (-f)

Tactic:
exact hf.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

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

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|

Tactic:
hf.abs

Premises used: AkraBazziRecurrence.GrowsPolynomially.abs
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|

Tactic:
exact hf.abs

Premises used: AkraBazziRecurrence.GrowsPolynomially.abs
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
c x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x
⊢ GT.gt (α := ℝ) 1 0

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
c : ℝ
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x →
      ∀ᶠ (x_2 : ℝ) in atTop,
        ∀ u ∈ Set.Icc (x * x_2) x_2,
          (fun (x : ℝ) ↦ c) u ∈
            Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ c) x_2)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ c) x_2))
⊢ GrowsPolynomially fun (x : ℝ) ↦ c

Tactic:
refine fun _ _ => ⟨1, by norm_num, 1, by norm_num, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
c x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x
h : ∀ (x_1 u : ℝ), u ∈ Set.Icc (x * x_1) x_1 → c ∈ Set.Icc (1 * c) (1 * c)
⊢ ∀ᶠ (x_1 : ℝ) in atTop,
    ∀ u ∈ Set.Icc (x * x_1) x_1,
      (fun (x : ℝ) ↦ c) u ∈
        Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ c) x_1)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ c) x_1))

Tactic:
filter_upwards [] with x
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
c x_1 : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x_1
x : ℝ
⊢ ∀ u ∈ Set.Icc (x_1 * x) x, c ∈ Set.Icc (1 * c) (1 * c)

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun (x : ℝ) ↦ x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ x) x) (c₂ * (fun (x : ℝ) ↦ x) x)

Tactic:
⟨b, hb.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
refine :
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun (x : ℝ) ↦ x) u ∈ Set.Icc (b * (fun (x : ℝ) ↦ x) x) (c₂ * (fun (x : ℝ) ↦ x) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x, (fun (x : ℝ) ↦ x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ x) x) (c₂ * (fun (x : ℝ) ↦ x) x)

Tactic:
refine ⟨b, hb.1, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ GT.gt (α := ℝ) 1 0

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
refine :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ x) u ∈ Set.Icc (b * (fun (x : ℝ) ↦ x) x) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ x) x))
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun (x : ℝ) ↦ x) u ∈ Set.Icc (b * (fun (x : ℝ) ↦ x) x) (c₂ * (fun (x : ℝ) ↦ x) x)

Tactic:
refine ⟨1, by norm_num, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
h : ∀ (x u : ℝ) (hu : u ∈ Set.Icc (b * x) x), u ∈ Set.Icc (b * x) (1 * x)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ x) u ∈ Set.Icc (b * (fun (x : ℝ) ↦ x) x) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ x) x))

Tactic:
filter_upwards with x u hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
h : b * x ≤ u ∧ u ≤ x
⊢ u ∈ Set.Icc (b * x) (1 * x)

Tactic:
simp only [one_mul, Set.mem_Icc]

Premises used: Set.mem_Icc, one_mul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u ∧ u ≤ x

Tactic:
⟨hu.1, hu.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u ∧ u ≤ x

Tactic:
exact ⟨hu.1, hu.2⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
h : ∀ (x : ℝ) (hx₁ : 0 ≤ f x) (hx₂ : 0 ≤ g x), f x * g x = |f x| * |g x|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : 0 ≤ g x
h : f x * g x = f x * |g x|
h₁ h₂ : f x * g x = f x * g x
⊢ f x * g x = |f x| * |g x|

Tactic:
rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]

Premises used: abs_of_nonneg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|
inl inl₁ inl₂ inl₃ : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x

Tactic:
rwa [iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
h : ∀ (x : ℝ) (hx₁ : 0 ≤ f x) (hx₂ : g x ≤ 0), f x * g x = -|f x| * |g x|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
x : ℝ
hx₁ : 0 ≤ f x
hx₂ : g x ≤ 0
⊢ f x * g x = -|f x| * |g x|

Tactic:
simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
inl : GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x

Tactic:
simp only [iff_eventuallyEq hmain, neg_mul]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq, neg_mul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)

Tactic:
this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)

Tactic:
exact this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ g x) ∨ ∀ᶠ (x : ℝ) in atTop, g x ≤ 0

Tactic:
cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
        rwa [iff_eventuallyEq hmain]
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg, neg_mul, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
h : ∀ (x : ℝ) (hx₁ : f x ≤ 0) (hx₂ : 0 ≤ g x), f x * g x = -|f x| * |g x|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
x : ℝ
hx₁ : f x ≤ 0
hx₂ : 0 ≤ g x
h : f x * g x = - -f x * |g x|
h₁ : f x * g x = - -f x * g x
h₂ h₃ : f x * g x = f x * g x
⊢ f x * g x = -|f x| * |g x|

Tactic:
rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]

Premises used: neg_neg, abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
inr : GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x

Tactic:
simp only [iff_eventuallyEq hmain, neg_mul]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq, neg_mul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)

Tactic:
this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ g x
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ -|f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)

Tactic:
exact this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
h : ∀ (x : ℝ) (hx₁ : f x ≤ 0) (hx₂ : g x ≤ 0), f x * g x = |f x| * |g x|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
filter_upwards [hf', hg'] with x hx₁ hx₂
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
x : ℝ
hx₁ : f x ≤ 0
hx₂ : g x ≤ 0
⊢ f x * g x = |f x| * |g x|

Tactic:
simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]

Premises used: abs_of_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|
inr : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x

Tactic:
simp only [iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
this
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hg' : ∀ᶠ (x : ℝ) in atTop, g x ≤ 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ f x * g x) fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|

Tactic:
exact this
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ g x) ∨ ∀ᶠ (x : ℝ) in atTop, g x ≤ 0

Tactic:
cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg, neg_mul, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
cases eventually_atTop_nonneg_or_nonpos hf with
    | inl hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
        rwa [iff_eventuallyEq hmain]
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
    | inr hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg, neg_mul, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
suffices : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x

Tactic:
suffices GrowsPolynomially fun x => |f x| * |g x| by
    cases eventually_atTop_nonneg_or_nonpos hf with
    | inl hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
        rwa [iff_eventuallyEq hmain]
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonneg hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
    | inr hf' =>
      cases eventually_atTop_nonneg_or_nonpos hg with
      | inl hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => -|f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
        simp only [iff_eventuallyEq hmain, neg_mul]
        exact this.neg
      | inr hg' =>
        have hmain : (fun x => f x * g x) =ᶠ[atTop] fun x => |f x| * |g x| := by
          filter_upwards [hf', hg'] with x hx₁ hx₂
          simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂]
        simp only [iff_eventuallyEq hmain]
        exact this