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

Tactic:
simp only [Nat.cast_add, Nat.cast_one] at *

Premises used: Nat.cast_add, Nat.cast_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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ x ≤ z

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

Tactic:
simp only [neg_add, ← sub_eq_add_neg] at hz

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

Tactic:
hz.2

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

Tactic:
exact hz.2

Premises used: And.right
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
calc : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
calc x ≤ z := hxz
          _ ≤ _ := by simp only [neg_add, ← sub_eq_add_neg] at hz; exact hz.2
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
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
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))

Tactic:
specialize hx ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' z

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HPow.hPow, 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
specialize :
  HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)
succ : ∀ (ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0), f z = 0
⊢ f z = 0

Tactic:
specialize ih ((2 : ℝ) ^ (-(k : ℤ) - 1) * x₀) hx' ?ineq

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HPow.hPow, 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)

Tactic:
rw [Set.left_mem_Icc]

Premises used: Set.left_mem_Icc
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
hbc : LE.le (α := ℝ) 1 2
hbc₁ : HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 ≤ -(↑k : ℤ)
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀

Tactic:
gcongr
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
⊢ LE.le (α := ℝ) 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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
⊢ HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 ≤ -(↑k : ℤ)

Tactic:
lia
-- 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₀
k : ℕ
ih :
  ∀ (z : ℝ),
    x ≤ z →
      z ∈
          Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
            (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀) →
        f z = 0
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀)
      (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑k : ℤ)) * x₀)

Tactic:
case ineq =>
        rw [Set.left_mem_Icc]
        gcongr
        · norm_num
        · lia

Premises used: Set.left_mem_Icc
-- 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z ∈
      Set.Icc (c₁ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (c₂ * f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
⊢ z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0

Tactic:
simp only [ih, 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ f z = 0

Tactic:
hx ⟨?lb₁, ?ub₁⟩

Premises used: And.intro
-- 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
refine : 1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z
refine₁ : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ f z = 0

Tactic:
refine hx ⟨?lb₁, ?ub₁⟩

Premises used: And.intro
-- 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ Ne (α := ℝ) 2 0

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_pos : 0 < x
x₀ : ℝ
hx₀_ge : x₀ ≥ max x 1
hx₀ : f x₀ = 0
x₀_pos : 0 < x₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
rw : HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z
⊢ 1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z

Tactic:
rw [one_div, ← zpow_neg_one, ← mul_assoc, ← zpow_add₀ (by norm_num)]

Premises used: zpow_neg_one, mul_assoc, zpow_add₀, one_div
-- 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2

Tactic:
ring
-- 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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx' : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
ih : f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0
hx :
  z ∈
      Set.Icc (1 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀))
        (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) →
    f z = 0
⊢ -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2

Tactic:
have h₁ : (-1 : ℤ) + (-k - 1) = -k - 2 := by ring