awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
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
have neg : ∀ᶠ (x : ℝ) in atTop, f x < 0
Tactic: refine Or.inr (Or.inr ?_)
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x < 0
have neg : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0
Tactic: simp only [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
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
have neg : (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
Tactic: rw [eventually_and]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
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
have x : (∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)
have obtain : ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
  (hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
  ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)
Tactic: obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)
have refine : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
Tactic: refine ⟨c₂, hc₂_mem, c₁, hc₁_mem, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
have h : ∀ (x : ℝ) (hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
  ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
Tactic: filter_upwards [hf] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ (-f) u ∈ Set.Icc (c₂ * (-f) x) (c₁ * (-f) x)
have h : f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: simp only [Pi.neg_apply, Set.neg_mem_Icc_iff, neg_mul_eq_mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially f
have rw : GrowsPolynomially (- -f)
Tactic: rw [← neg_neg f]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
have h : ∀ (x : ℝ) (hx : 0 ≤ f x), f x = |f x|
Tactic: filter_upwards [hf'] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : 0 ≤ f x
⊢ f x = |f x|
have h : f x = f x
Tactic: rw [abs_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|
have hmain : 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]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
have h : ∀ (x : ℝ) (hx : f x ≤ 0), (-f) x = |f x|
Tactic: filter_upwards [hf'] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|
have hmain : -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]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hmain : -f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|
have inr : GrowsPolynomially (-f)
Tactic: rw [← iff_eventuallyEq hmain]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|
have x : (∀ᶠ (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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
c : ℝ
⊢ GrowsPolynomially fun (x : ℝ) ↦ c
have 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))
Tactic: refine fun _ _ => ⟨1, by norm_num, 1, by norm_num, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
c x : ℝ
h : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) x
⊢ ∀ᶠ (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))
have h : ∀ (x_1 u : ℝ), u ∈ Set.Icc (x * x_1) x_1 → c ∈ Set.Icc (1 * c) (1 * c)
Tactic: filter_upwards [] with x
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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)
have 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)
Tactic: refine ⟨b, hb.1, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∃ 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)
have 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))
Tactic: refine ⟨1, by norm_num, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∀ᶠ (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))
have h : ∀ (x u : ℝ) (hu : u ∈ Set.Icc (b * x) x), u ∈ Set.Icc (b * x) (1 * x)
Tactic: filter_upwards with x u hu
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ∈ Set.Icc (b * x) (1 * x)
have h : b * x ≤ u ∧ u ≤ x
Tactic: simp only [one_mul, Set.mem_Icc]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
have h : ∀ (x : ℝ) (hx₁ : 0 ≤ f x) (hx₂ : 0 ≤ g x), f x * g x = |f x| * |g x|
Tactic: filter_upwards [hf', hg'] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ f x * g x = |f x| * |g x|
have h : f x * g x = f x * |g x|
Tactic: rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
⊢ f x * g x = |f x| * |g x|
have h₁ : f x * g x = f x * g x
Tactic: rw [abs_of_nonneg hx₁, abs_of_nonneg hx₂]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have hmain : 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₂]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
have h : ∀ (x : ℝ) (hx₁ : 0 ≤ f x) (hx₂ : g x ≤ 0), f x * g x = -|f x| * |g x|
Tactic: filter_upwards [hf', hg'] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have hmain : 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₂]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
have inl : GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)
Tactic: simp only [iff_eventuallyEq hmain, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have 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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
have h : ∀ (x : ℝ) (hx₁ : f x ≤ 0) (hx₂ : 0 ≤ g x), f x * g x = -|f x| * |g x|
Tactic: filter_upwards [hf', hg'] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ f x * g x = -|f x| * |g x|
have h : f x * g x = - -f x * |g x|
Tactic: rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
⊢ f x * g x = -|f x| * |g x|
have h₁ : f x * g x = - -f x * g x
Tactic: rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ f x * g x = -|f x| * |g x|
have h₂ : f x * g x = f x * g x
Tactic: rw [abs_of_nonpos hx₁, abs_of_nonneg hx₂, neg_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have hmain : 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]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
have inr : GrowsPolynomially fun (x : ℝ) ↦ -(|f x| * |g x|)
Tactic: simp only [iff_eventuallyEq hmain, neg_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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|
have h : ∀ (x : ℝ) (hx₁ : f x ≤ 0) (hx₂ : g x ≤ 0), f x * g x = |f x| * |g x|
Tactic: filter_upwards [hf', hg'] with x hx₁ hx₂
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have hmain : 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₂]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have 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_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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : GrowsPolynomially fun (x : ℝ) ↦ |f x| * |g x|
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have 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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * g x
have suffices : 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
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
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 : ℝ) ↦ |f x| * |g x|) u ∈
            Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
have hf₁ : ∃ c₁ > 0,
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
Tactic: have hf := hf.abs b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf :
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x| * |g x|) u ∈
            Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x| * |g x|) x) (c₂ * (fun (x : ℝ) ↦ |f x| * |g x|) x)
have hg₁ : ∃ c₁ > 0,
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |g x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |g x|) x) (c₂ * (fun (x : ℝ) ↦ |g x|) x)
Tactic: have hg := hg.abs b hb