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

Tactic:
have hmain : ∀ (m : ℕ) (z : ℝ), x ≤ z →
      z ∈ Set.Icc ((2 : ℝ) ^ (-(m : ℤ) - 1) * x₀) ((2 : ℝ) ^ (-(m : ℤ)) * x₀) → f z = 0 := by
    intro m
    induction m with
    | zero =>
      simp only [CharP.cast_eq_zero, neg_zero, zero_sub, zpow_zero, one_mul] at *
      specialize hx x₀ (le_of_max_le_left hx₀_ge)
      simp only [hx₀, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine fun z _ hz => hx _ ?_
      simp only [zpow_neg, zpow_one] at hz
      simp only [one_div, hz]
    | succ k ih =>
      intro z hxz hz
      simp only [Nat.cast_add, Nat.cast_one] at *
      have hx' : x ≤ (2 : ℝ) ^ (-(k : ℤ) - 1) * x₀ := by
        calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
      specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z
      specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq
      case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia
      simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
      refine hx ⟨?lb₁, ?ub₁⟩
      case lb₁ =>
        rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]
        have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring
        have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by ring
        rw [h₁]
        rw [h₂] at hz
        exact hz.1
      case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this
-- 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
⊢ f x = 0

Tactic:
hmain ⌊-logb 2 (x / x₀)⌋₊ x le_rfl ⟨?lb, ?ub⟩

Premises used: le_rfl, HDiv.hDiv, Real.logb, And.intro, Nat.floor, OfNat.ofNat, Neg.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 : ∀ (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
refine : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x
refine₁ : x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀
⊢ f x = 0

Tactic:
refine hmain ⌊-logb 2 (x / x₀)⌋₊ x le_rfl ⟨?lb, ?ub⟩

Premises used: le_rfl, HDiv.hDiv, Real.logb, And.intro, Nat.floor, OfNat.ofNat, Neg.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 : ∀ (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
rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) ≤ x / x₀
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x

Tactic:
rw [← le_div_iff₀ x₀_pos]

Premises used: le_div_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 : ∀ (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
⊢ LT.lt (α := ℝ) 1 2

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
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
⊢ LT.lt (α := ℝ) 0 2

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
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 < x / x₀

Tactic:
positivity
-- 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
refine : logb 2 (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1)) ≤ logb 2 (x / x₀)
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) ≤ x / x₀

Tactic:
refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
      (by positivity)).mp ?_

Premises used: zpow_pos, Real.logb_le_logb, Iff.mp
-- 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
⊢ Ne (α := ℝ) 2 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
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
rw : -logb 2 (x / x₀) ≤ -(↑(HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) : ℝ)
⊢ logb 2 (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1)) ≤ logb 2 (x / x₀)

Tactic:
rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]

Premises used: Real.rpow_intCast, Real.logb_rpow, neg_le_neg_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 : ∀ (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
simp : -logb 2 (x / x₀) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
⊢ -logb 2 (x / x₀) ≤ -(↑(HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) : ℝ)

Tactic:
simp only [Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub, sub_neg_eq_add]

Premises used: Int.cast_neg, Int.cast_natCast, neg_sub, Int.cast_sub, Int.cast_one, sub_neg_eq_add
-- 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
⊢ -logb 2 (x / x₀) ≤ (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ)

Tactic:
Nat.le_ceil (-logb 2 (x / x₀))

Premises used: HDiv.hDiv, Real.logb, Nat.le_ceil, OfNat.ofNat, Neg.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 : ∀ (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
rw : (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) 1
⊢ (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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
⊢ (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) 1

Tactic:
exact_mod_cast Nat.ceil_le_floor_add_one _

Premises used: Nat.ceil_le_floor_add_one
-- 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
calc : (↑⌈-logb 2 (x / x₀)⌉₊ : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)
⊢ -logb 2 (x / x₀) ≤ HAdd.hAdd (α := ℝ) 1 (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ)

Tactic:
calc -logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

Premises used: HDiv.hDiv, Real.logb, Nat.le_ceil, OfNat.ofNat, Neg.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 : ∀ (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
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) 1) * x₀ ≤ x

Tactic:
case lb =>
    rw [← le_div_iff₀ x₀_pos]
    refine (logb_le_logb (b := 2) (by norm_num) (zpow_pos (by norm_num) _)
      (by positivity)).mp ?_
    rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]
    simp only [Int.cast_sub, Int.cast_neg, Int.cast_natCast, Int.cast_one, neg_sub, sub_neg_eq_add]
    calc -logb 2 (x / x₀) ≤ ⌈-logb 2 (x / x₀)⌉₊ := Nat.le_ceil (-logb 2 (x / x₀))
         _ ≤ _ := by rw [add_comm]; exact_mod_cast Nat.ceil_le_floor_add_one _

Premises used: Int.cast_neg, Int.cast_natCast, neg_sub, Int.cast_sub, HDiv.hDiv, zpow_pos, Real.logb, Real.logb_le_logb, Iff.mp, Nat.le_ceil, le_div_iff₀, OfNat.ofNat, Real.rpow_intCast, Real.logb_rpow, Neg.neg, Int.cast_one, sub_neg_eq_add, neg_le_neg_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 : ∀ (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
rw : x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))
⊢ x ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) * x₀

Tactic:
rw [← div_le_iff₀ x₀_pos]

Premises used: div_le_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 : ∀ (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
refine : logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))
⊢ x / x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ))

Tactic:
refine (logb_le_logb (b := 2) (by norm_num) (by positivity)
      (zpow_pos (by norm_num) _)).mp ?_

Premises used: zpow_pos, Real.logb_le_logb, Iff.mp
-- 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
rw : -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)
⊢ logb 2 (x / x₀) ≤ logb 2 (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)))

Tactic:
rw [← rpow_intCast, logb_rpow (by norm_num) (by norm_num), ← neg_le_neg_iff]

Premises used: Real.rpow_intCast, Real.logb_rpow, neg_le_neg_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 : ∀ (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
simp : (↑⌊-logb 2 (x / x₀)⌋₊ : ℝ) ≤ -logb 2 (x / x₀)
⊢ -(↑(-(↑⌊-logb 2 (x / x₀)⌋₊ : ℤ)) : ℝ) ≤ -logb 2 (x / x₀)

Tactic:
simp only [Int.cast_neg, Int.cast_natCast, neg_neg]

Premises used: Int.cast_neg, Int.cast_natCast, neg_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 : ∀ (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
rw : logb 2 (x / x₀) ≤ 0
⊢ 0 ≤ -logb 2 (x / x₀)

Tactic:
rw [neg_nonneg]

Premises used: neg_nonneg
-- 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 ≤ x / x₀

Tactic:
positivity
-- 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
refine : x / x₀ ≤ 1
⊢ logb 2 (x / x₀) ≤ 0

Tactic:
refine logb_nonpos (by norm_num) (by positivity) ?_

Premises used: Real.logb_nonpos
-- 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
rw : x ≤ x₀
⊢ x / x₀ ≤ 1

Tactic:
rw [div_le_one x₀_pos]

Premises used: div_le_one
-- 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
⊢ x ≤ x₀

Tactic:
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 : ∀ (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
⊢ x ≤ x₀

Tactic:
exact le_of_max_le_left hx₀_ge

Premises used: le_of_max_le_left