awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1)) fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
IsTheta.const_mul_left hp <| isTheta_refl _ _

Premises used: Asymptotics.IsTheta.const_mul_left, Asymptotics.isTheta_refl
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 - ε z)) fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
calc (fun x => deriv (fun z => z ^ p * (1 - ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
        (isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

Premises used: Asymptotics.IsTheta.const_mul_left, HMul.hMul, deriv, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, HPow.hPow, Asymptotics.isTheta_refl, Asymptotics.IsEquivalent.isTheta, OfNat.ofNat, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ Norm.norm (E := ℝ) (deriv (fun (z : ℝ) ↦ z ^ p * (1 + ε z)) x))
    fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
IsTheta.norm_left ?_

Premises used: Asymptotics.IsTheta.norm_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 + ε z)) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ Norm.norm (E := ℝ) (deriv (fun (z : ℝ) ↦ z ^ p * (1 + ε z)) x))
    fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Premises used: Asymptotics.IsTheta.norm_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (z : ℝ) ↦ z ^ p * (1 + ε z)) x) fun (z : ℝ) ↦
    p * z ^ (p - 1)

Tactic:
(isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn hp).isTheta

Premises used: AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, Asymptotics.IsEquivalent.isTheta
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 + ε z)) fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
calc (fun x => deriv (fun z => z ^ p * (1 + ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
      (isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

Premises used: Asymptotics.IsTheta.const_mul_left, HMul.hMul, deriv, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, HPow.hPow, Asymptotics.isTheta_refl, HAdd.hAdd, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, Asymptotics.IsEquivalent.isTheta, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
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, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)

Tactic:
have hg' := hg b hb
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hg' : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
obtain :
  ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)),
    ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (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, hg'⟩ := hg'
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g 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:
⟨c₁, hc₁_mem, c₂, hc₂_mem, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
refine : ∀ᶠ (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:
refine ⟨c₁, hc₁_mem, c₂, hc₂_mem, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
h :
  ∀ (x : ℝ) (hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x))
    (hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y) (hx₃ : f x = g x),
    ∀ 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)

Tactic:
filter_upwards [hg', (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg, hfg]
    with x hx₁ hx₂ hx₃

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, And.left, Filter.Tendsto.eventually_forall_ge_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h : g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
rw [hx₂ u hu.1, hx₃]

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)

Tactic:
hx₁ u hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
x : ℝ
hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y
hx₃ : f x = g x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)

Tactic:
exact hx₁ u hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
h : f =ᶠ[atTop] g
⊢ GrowsPolynomially f ↔ GrowsPolynomially g

Tactic:
⟨fun hf => congr_of_eventuallyEq h.symm hf, fun hg => congr_of_eventuallyEq h hg⟩

Premises used: Iff.intro, AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
obtain :
  ∀ c₁ > 0,
    ∀ (c₂ : ℝ) (hc₂ : c₂ > 0) (h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
      ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
⊢ ∃ c > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

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

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

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

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

Tactic:
filter_upwards [h]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a

Tactic:
fun _ H u hu => (H u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
hc₂ : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a

Tactic:
exact fun _ H u hu => (H u hu).2
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
obtain :
  ∀ (c : ℝ) (hc_mem : c > 0) (hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x),
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb

Premises used: AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)

Tactic:
⟨c, hc_mem, hc.natCast_atTop⟩

Premises used: Filter.Eventually.natCast_atTop, And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), f u ≤ c * f (↑n : ℝ)

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

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

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

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

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

Tactic:
filter_upwards [h]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u

Tactic:
fun _ H u hu => (H u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c₁ : ℝ
hc₁ : c₁ > 0
c₂ : ℝ
left : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ ∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, c₁ * f a ≤ f u

Tactic:
exact fun _ H u hu => (H u hu).1
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
obtain :
  ∀ (c : ℝ) (hc_mem : c > 0) (hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u),
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_ge hb

Premises used: AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u

Tactic:
⟨c, hc_mem, hc.natCast_atTop⟩

Premises used: Filter.Eventually.natCast_atTop, And.intro, Exists.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * (↑n : ℝ)) (↑n : ℝ), c * f (↑n : ℝ) ≤ f u

Tactic:
exact ⟨c, hc_mem, hc.natCast_atTop⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (1 / 2)

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0
obtain :
  ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
    ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x = 0

Tactic:
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf (1 / 2) (by norm_num)

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∃ᶠ (x : ℝ) in atTop, f x = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
rw :
  ∀ (hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0) (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
    ∀ᶠ (x : ℝ) in atTop, f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x = 0

Tactic:
rw [frequently_atTop] at hf'

Premises used: Filter.frequently_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
h :
  ∀ (x : ℝ) (hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)) (hx_pos : 0 < x),
    f x = 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x = 0

Tactic:
filter_upwards [eventually_forall_ge_atTop.mpr hf, eventually_gt_atTop 0] with x hx hx_pos

Premises used: Iff.mpr, OfNat.ofNat, Filter.eventually_forall_ge_atTop, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
h : ∀ (x₀ : ℝ) (hx₀_ge : x₀ ≥ max x 1) (hx₀ : f x₀ = 0), f x = 0
⊢ f x = 0

Tactic:
obtain ⟨x₀, hx₀_ge, hx₀⟩ := hf' (max x 1)

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
⊢ LT.lt (α := ℝ) 0 1

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
⊢ 0 < x₀

Tactic:
have x₀_pos := calc
    0 < 1 := by norm_num
    _ ≤ x₀ := le_of_max_le_right hx₀_ge
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
zero : ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0
⊢ ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑0 : ℤ)) * x₀) →
        f z = 0

Tactic:
simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *

Premises used: CharP.cast_eq_zero, zpow_zero, neg_zero, one_mul, zero_sub
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ (y : ℝ), x ≤ y → ∀ u ∈ Set.Icc (1 / 2 * y) y, f u ∈ Set.Icc (c₁ * f y) (c₂ * f y)
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
⊢ ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u ∈ Set.Icc (c₁ * f x₀) (c₂ * f x₀)

Tactic:
specialize hx x₀ (le_of_max_le_left hx₀_ge)

Premises used: le_of_max_le_left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u ∈ Set.Icc (c₁ * f x₀) (c₂ * f x₀)
⊢ ∀ u ∈ Set.Icc (1 / 2 * 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 : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0

Tactic:
fun z _ hz => hx _ ?_
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
zero : ∀ (z : ℝ), x ≤ z → ∀ (hz : z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀), z ∈ Set.Icc (1 / 2 * x₀) x₀
⊢ ∀ (z : ℝ), x ≤ z → z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀ → f z = 0

Tactic:
refine fun z _ hz => hx _ ?_
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
z : ℝ
h : x ≤ z
hz : z ∈ Set.Icc (HPow.hPow (α := ℝ) (β := ℤ) 2 (-1) * x₀) x₀
⊢ z ∈ Set.Icc (2⁻¹ * x₀) x₀

Tactic:
simp only [zpow_neg, zpow_one] at hz

Premises used: zpow_one, zpow_neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf' : ∀ (a : ℝ), ∃ b ≥ a, f b = 0
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
hx : ∀ u ∈ Set.Icc (1 / 2 * x₀) x₀, f u = 0
z : ℝ
h : x ≤ z
hz : z ∈ Set.Icc (2⁻¹ * x₀) x₀
⊢ z ∈ Set.Icc (1 / 2 * x₀) x₀

Tactic:
simp only [one_div, hz]

Premises used: one_div