awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
⊢ 0 ≤ -logb 2 (x / x₀)

Tactic:
have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left 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₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
this : 0 ≤ -logb 2 (x / x₀)
⊢ (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)

Tactic:
exact_mod_cast Nat.floor_le this

Premises used: Nat.floor_le
-- 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₀
hmain :
  ∀ (m : ℕ) (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) * x₀) →
        f z = 0
case case₁ case₂ : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
case₃ : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
case₄ : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
case₅ : (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
case₆ : ∀ (this : 0 ≤ -logb 2 (x / x₀)), (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀

Tactic:
case ub =>
    rw [← div_le_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_neg, Int.cast_natCast, neg_neg]
    have : 0 ≤ -logb 2 (x / x₀) := by
      rw [neg_nonneg]
      refine logb_nonpos (by norm_num) (by positivity) ?_
      rw [div_le_one x₀_pos]
      exact le_of_max_le_left hx₀_ge
    exact_mod_cast Nat.floor_le this

Premises used: Int.cast_neg, div_le_iff₀, Int.cast_natCast, neg_neg, zpow_pos, Real.logb_le_logb, Iff.mp, Real.rpow_intCast, Real.logb_rpow, neg_le_neg_iff
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (1 / 2)

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

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

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
h₁ : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
h₁ : ∀ (x : ℝ) (hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) (hx_nonneg : 0 ≤ x), 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x

Tactic:
filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
hbc : 1 / 2 ≤ 3 / 4
⊢ 1 / 2 * x ≤ 3 / 4 * x

Tactic:
gcongr ?_ * x
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 ≤ 3 / 4

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : x < 3 / 4 * x → GT.gt (α := ℝ) 4 0
linarith₄ : x < 3 / 4 * x → 0 - x + (4 * x - HMul.hMul (α := ℝ) 1 3 * (1 * x)) = 0
⊢ 3 / 4 * x ≤ x

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 * x ≤ 3 / 4 * x ∧ 3 / 4 * x ≤ x

Tactic:
exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x

Tactic:
have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
have hu := hx (3 / 4 * x) h'
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty

Tactic:
have hu := Set.nonempty_of_mem hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ c₁ * f x ≤ c₂ * f x

Tactic:
rw [Set.nonempty_Icc] at hu

Premises used: Set.nonempty_Icc
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
linarith : (c₂ - c₁) * f x < 0 → c₁ * f x - c₂ * f x + ((c₂ - c₁) * f x - 0) = 0
⊢ 0 ≤ (c₂ - c₁) * f x

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ 0 ≤ (c₂ - c₁) * f x

Tactic:
have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : 0 ≤ (c₂ - c₁) * f x
linarith : c₂ - c₁ ≤ 0 → c₁ - c₂ + (c₂ - c₁ - 0) = 0
⊢ 0 < c₂ - c₁

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hlt : c₁ < c₂
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : 0 ≤ (c₂ - c₁) * f x
⊢ 0 ≤ f x

Tactic:
exact nonneg_of_mul_nonneg_right hu' (by linarith)

Premises used: nonneg_of_mul_nonneg_right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
h₁ : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
h₁ : ∀ (x : ℝ) (hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) (hx_nonneg : 0 ≤ x), f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
hbc : 1 / 2 ≤ 3 / 4
⊢ 1 / 2 * x ≤ 3 / 4 * x

Tactic:
gcongr ?_ * x
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 ≤ 3 / 4

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
linarith : x < 3 / 4 * x → 4 / 4 = 1
linarith₁ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : x < 3 / 4 * x → HMul.hMul (α := ℝ) 4 1 = 4
linarith₃ : x < 3 / 4 * x → GT.gt (α := ℝ) 4 0
linarith₄ : x < 3 / 4 * x → 0 - x + (4 * x - HMul.hMul (α := ℝ) 1 3 * (1 * x)) = 0
⊢ 3 / 4 * x ≤ x

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 1 / 2 * x ≤ 3 / 4 * x ∧ 3 / 4 * x ≤ x

Tactic:
exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
⊢ 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x

Tactic:
have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
⊢ f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
have hu := hx (3 / 4 * x) h'
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty

Tactic:
have hu := Set.nonempty_of_mem hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : (Set.Icc (c₁ * f x) (c₂ * f x)).Nonempty
⊢ c₁ * f x ≤ c₂ * f x

Tactic:
rw [Set.nonempty_Icc] at hu

Premises used: Set.nonempty_Icc
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
linarith : 0 < (c₁ - c₂) * f x → c₁ * f x - c₂ * f x + (0 - (c₁ - c₂) * f x) = 0
⊢ (c₁ - c₂) * f x ≤ 0

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
⊢ (c₁ - c₂) * f x ≤ 0

Tactic:
have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
linarith : c₁ - c₂ ≤ 0 → c₂ - c₁ + (c₁ - c₂ - 0) = 0
⊢ 0 < c₁ - c₂

Tactic:
linarith
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hgt : c₂ < c₁
x : ℝ
hx : ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hx_nonneg : 0 ≤ x
h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x
hu_1 : f (3 / 4 * x) ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hu : c₁ * f x ≤ c₂ * f x
hu' : (c₁ - c₂) * f x ≤ 0
⊢ f x ≤ 0

Tactic:
exact nonpos_of_mul_nonpos_right hu' (by linarith)

Premises used: nonpos_of_mul_nonpos_right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
heq : c₁ = c₂
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x

Tactic:
simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h

Premises used: Set.Icc_self, Set.mem_singleton_iff
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (1 / 2 * x) x, f u = c₂ * f x
⊢ ∃ (a : ℝ), ∀ b ≥ a, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b

Tactic:
rw [eventually_atTop] at h

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
h : ∃ (a : ℝ), ∀ b ≥ a, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
obtain :
  ∀ (n₀ : ℝ) (hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b), ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
obtain ⟨n₀, hn₀⟩ := h
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
⟨f (max n₀ 2), ?_⟩

Premises used: Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
refine : ∀ᶠ (x : ℝ) in atTop, f x = f (max n₀ 2)
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
refine ⟨f (max n₀ 2), ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
rw : ∃ (a : ℝ), ∀ b ≥ a, f b = f (max n₀ 2)
⊢ ∀ᶠ (x : ℝ) in atTop, f x = f (max n₀ 2)

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∃ (a : ℝ), ∀ b ≥ a, f b = f (max n₀ 2)

Tactic:
⟨max n₀ 2, ?_⟩

Premises used: Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
refine : ∀ b ≥ max n₀ 2, f b = f (max n₀ 2)
⊢ ∃ (a : ℝ), ∀ b ≥ a, f b = f (max n₀ 2)

Tactic:
refine ⟨max n₀ 2, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ LT.lt (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ 0 < max n₀ 2

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
refine : ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)
refine₁ :
  ∀ n ≥ 1,
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
⊢ ∀ b ≥ max n₀ 2, f b = f (max n₀ 2)

Tactic:
refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step

Premises used: Real.induction_Ico_mul, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)

Tactic:
grind
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
⊢ ∀ x ∈ Set.Ico (max n₀ 2) (2 * max n₀ 2), f x = f (max n₀ 2)

Tactic:
case base => grind
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
c₁ : ℝ
left : c₁ > 0
c₂ : ℝ
left_1 : c₂ > 0
heq : c₁ = c₂
n₀ : ℝ
hn₀ : ∀ b ≥ n₀, ∀ u ∈ Set.Icc (1 / 2 * b) b, f u = c₂ * f b
n : ℕ
_ :
  n ≥ 1 →
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)
⊢ n ≥ 1 →
    (∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)) →
      ∀ z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2), f z = f (max n₀ 2)

Tactic:
_