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_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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2

Tactic:
have h₂ : -(k + (1 : ℤ)) - 1 = -k - 2 := by 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
rw : HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀ ≤ z
⊢ HPow.hPow (α := ℝ) 2 (-1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀ ≤ z

Tactic:
rw [h₁]
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)

Tactic:
rw [h₂] at hz
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
hz₁ :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
⊢ x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
rw [h₂] at hz
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
hz₁ :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀)
      (HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀)
hx'₁ : x ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ f (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) = 0

Tactic:
rw [h₂] at hz
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
hz₁ :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * 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
⊢ 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:
rw [h₂] at hz
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
hz₁ :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * 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:
rw [h₂] at hz
-- 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
hz₁ :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * 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
h₃ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2

Tactic:
rw [h₂] at hz
-- 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 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀ ≤ z

Tactic:
hz.1

Premises used: And.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₀
k : ℕ
z : ℝ
hxz : x ≤ z
hz :
  z ∈
    Set.Icc (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * 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
h₁ : -1 + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
h₂ : -HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 - 1 = HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2
⊢ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 2) * x₀ ≤ z

Tactic:
exact hz.1

Premises used: And.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₀
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 / 2 * (HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀) ≤ z

Tactic:
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

Premises used: zpow_neg_one, mul_assoc, zpow_add₀, And.left, 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
⊢ z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀

Tactic:
have := 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_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
this : z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

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

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_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
this : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
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_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
this : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
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_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
case case₁ case₂ :
  ∀ (this : z ≤ HPow.hPow (α := ℝ) 2 (-HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) * x₀),
    z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
case₃ :
  ∀ (this : z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀),
    z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀
⊢ z ≤ HPow.hPow (α := ℝ) 2 (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) * x₀

Tactic:
case ub₁ =>
        have := hz.2
        simp only [neg_add, ← sub_eq_add_neg] at this
        exact this

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

Tactic:
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

Premises used: CharP.cast_eq_zero, Set.Icc_self, zpow_neg_one, mul_assoc, zpow_zero, sub_eq_add_neg, neg_add, zpow_one, le_of_max_le_left, MulZeroClass.mul_zero, Nat.cast_add, zpow_add₀, Set.mem_singleton_iff, Set.left_mem_Icc, zpow_neg, one_div, neg_zero, Nat.cast_one, one_mul, zero_sub