awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * (g x)⁻¹

Tactic:
GrowsPolynomially.mul hf (GrowsPolynomially.inv hg)

Premises used: AkraBazziRecurrence.GrowsPolynomially.mul, AkraBazziRecurrence.GrowsPolynomially.inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹
⊢ GrowsPolynomially fun (x : ℝ) ↦ f x * (g x)⁻¹

Tactic:
exact GrowsPolynomially.mul hf (GrowsPolynomially.inv hg)

Premises used: AkraBazziRecurrence.GrowsPolynomially.mul, AkraBazziRecurrence.GrowsPolynomially.inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
obtain :
  ∀ (c₁ : ℝ) (hc₁_mem : 0 < c₁) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hfnew : ∀ᶠ (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,
            (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
obtain ⟨c₁, (hc₁_mem : 0 < c₁), c₂, hc₂_mem, hfnew⟩ := hf b hb
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 < c₁ ^ p

Tactic:
have hc₁p : 0 < c₁ ^ p := Real.rpow_pos_of_pos hc₁_mem _
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
⊢ 0 < c₂ ^ p

Tactic:
have hc₂p : 0 < c₂ ^ p := Real.rpow_pos_of_pos hc₂_mem _
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
⟨c₁^p, hc₁p, ?_⟩

Premises used: HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
inl :
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
refine ⟨c₁^p, hc₁p, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
⟨c₂^p, hc₂p, ?_⟩

Premises used: HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
inl :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ ^ p * (fun (x : ℝ) ↦ f x ^ p) x)
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
refine ⟨c₂^p, hc₂p, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h_1 : 0 ≤ p
x : ℝ
h :
  0 < x →
    (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
      0 ≤ f x →
        (∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y) →
          ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
⊢ 0 < x →
    (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
      0 ≤ f x →
        (∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y) →
          ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)

Tactic:
_
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h_1 : 0 ≤ p
h :
  ∀ (x : ℝ),
    0 < x →
      ∀ (hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) (hf_nonneg : 0 ≤ f x)
        (hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y),
        ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ ^ p * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ ^ p * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
filter_upwards [eventually_gt_atTop 0, hfnew, hf_nonneg,
        (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf_nonneg]
        with x _ hf₁ hf_nonneg hf_nonneg₂

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, And.left, OfNat.ofNat, Filter.Tendsto.eventually_forall_ge_atTop, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 0 ≤ f u

Tactic:
have fu_nonneg : 0 ≤ f u := hf_nonneg₂ u hu.1
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)

Tactic:
⟨?lb, ?ub⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
refine : c₁ ^ p * f x ^ p ≤ f u ^ p
refine₁ : f u ^ p ≤ c₂ ^ p * f x ^ p
⊢ f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)

Tactic:
refine ⟨?lb, ?ub⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
rw rw₁ : c₁ ^ p * f x ^ p = c₁ ^ p * f x ^ p
⊢ c₁ ^ p * f x ^ p = (c₁ * f x) ^ p

Tactic:
rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]

Premises used: le_of_lt, Real.mul_rpow
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
h₁ : c₁ * f x ≤ f u
⊢ (c₁ * f x) ^ p ≤ f u ^ p

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ * f x ≤ f u

Tactic:
(hf₁ u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ * f x ≤ f u

Tactic:
exact (hf₁ u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
c₃ : c₁ ^ p * f x ^ p = (c₁ * f x) ^ p
c₄ : (c₁ * f x) ^ p ≤ f u ^ p
⊢ c₁ ^ p * f x ^ p ≤ f u ^ p

Tactic:
calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1

Premises used: HMul.hMul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ c₁ ^ p * f x ^ p ≤ f u ^ p

Tactic:
case lb => calc
      c₁ ^ p * (f x) ^ p = (c₁ * f x) ^ p := by rw [mul_rpow (le_of_lt hc₁_mem) hf_nonneg]
        _ ≤ _ := by gcongr; exact (hf₁ u hu).1

Premises used: HMul.hMul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
h₁ : f u ≤ c₂ * f x
⊢ f u ^ p ≤ (c₂ * f x) ^ p

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ≤ c₂ * f x

Tactic:
(hf₁ u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
⊢ f u ≤ c₂ * f x

Tactic:
exact (hf₁ u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
rw rw₁ : (c₂ * f x) ^ p = (c₂ * f x) ^ p
⊢ (c₂ * f x) ^ p = c₂ ^ p * f x ^ p

Tactic:
rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

Premises used: le_of_lt, Real.mul_rpow
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
p₁ : f u ^ p ≤ (c₂ * f x) ^ p
p₂ : (c₂ * f x) ^ p = c₂ ^ p * f x ^ p
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p

Tactic:
calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

Premises used: HMul.hMul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg_1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h : 0 ≤ p
x : ℝ
h_1 : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hf_nonneg : 0 ≤ f x
hf_nonneg₂ : ∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y
u : ℝ
hu : u ∈ Set.Icc (b * x) x
fu_nonneg : 0 ≤ f u
case : f u ^ p ≤ (c₂ * f x) ^ p
case₁ : (c₂ * f x) ^ p = c₂ ^ p * f x ^ p
⊢ f u ^ p ≤ c₂ ^ p * f x ^ p

Tactic:
case ub => calc
      (f u) ^ p ≤ (c₂ * f x) ^ p := by gcongr; exact (hf₁ u hu).2
        _ = _ := by rw [← mul_rpow (le_of_lt hc₂_mem) hf_nonneg]

Premises used: HMul.hMul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ GT.gt (α := ℝ) 1 0

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
refine :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈
        Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x))
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
refine ⟨1, by norm_num, 1, by norm_num, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
h :
  ∀ (x : ℝ) (hx : f x = 0) (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 ^ p ∈ Set.Icc (1 * f x ^ p) (1 * f x ^ p)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x ^ p) u ∈
        Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ f x ^ p) x))

Tactic:
filter_upwards [hzero, hfnew] with x hx hx'
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
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
h : f u ^ p = 0
⊢ f u ^ p ∈ Set.Icc (1 * f x ^ p) (1 * f x ^ p)

Tactic:
simp only [hx, zero_rpow (ne_of_lt hp), mul_zero,
        Set.Icc_self, Set.mem_singleton_iff]

Premises used: Set.Icc_self, Real.zero_rpow, MulZeroClass.mul_zero, Set.mem_singleton_iff, ne_of_lt
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
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
⊢ ∀ u ∈ Set.Icc (b * x) x, f u = 0

Tactic:
simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx'

Premises used: Set.Icc_self, MulZeroClass.mul_zero, Set.mem_singleton_iff
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hx' : ∀ u ∈ Set.Icc (b * x) x, f u = 0
h : HPow.hPow (α := ℝ) 0 p = 0
h₁ h₂ : Eq (α := ℝ) 0 0
⊢ f u ^ p = 0

Tactic:
rw [hx' u hu, zero_rpow (ne_of_lt hp)]

Premises used: Real.zero_rpow, ne_of_lt
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x ^ p) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x ^ p) x) (c₂ * (fun (x : ℝ) ↦ f x ^ p) x)

Tactic:
⟨c₂^p, hc₂p, ?_⟩

Premises used: HPow.hPow, And.intro, Exists.intro