awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
h : 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)
⊢ (∀ 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:
_
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
_ : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * 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:
_
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num1
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
⊢ max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2

Tactic:
simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]

Premises used: one_le_pow₀
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
⊢ max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2

Tactic:
have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2
⊢ f (1 / 2 * z) = f (max n₀ 2)

Tactic:
grind [mul_assoc]

Premises used: mul_assoc
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2
⊢ f (1 / 2 * z) = f (max n₀ 2)

Tactic:
have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
-- 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 : ℕ
h : n ≥ 1
h_1 : ∀ z ∈ Set.Ico (max n₀ 2) (HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
z : ℝ
h_2 : z ∈ Set.Ico (HPow.hPow (α := ℝ) 2 n * max n₀ 2) (HPow.hPow (α := ℝ) 2 (n + 1) * max n₀ 2)
le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2
half_z_to_base : f (1 / 2 * z) = f (max n₀ 2)
⊢ f z = 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
case case₁ case₂ case₃ case₄ :
  ∀ 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)
case₅ :
  ∀ 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),
        ∀ (le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2), f z = f (max n₀ 2)
case₆ :
  ∀ 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),
        ∀ (le_2n : max n₀ 2 ≤ HPow.hPow (α := ℝ) 2 n * max n₀ 2) (half_z_to_base : f (1 / 2 * z) = f (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:
case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
-- 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₂
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c

Tactic:
have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
      simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
      rw [eventually_atTop] at h
      obtain ⟨n₀, hn₀⟩ := h
      refine ⟨f (max n₀ 2), ?_⟩
      rw [eventually_atTop]
      refine ⟨max n₀ 2, ?_⟩
      refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
      case base => grind
      case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
-- 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₂
hmain : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, f x = c
obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : ℝ) in atTop, f x = c), (∀ᶠ (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, hc⟩ := hmain
-- 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₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
h₁ : ∀ (a : ℝ) (hc : f a = c), 0 ≤ f a
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x

Tactic:
filter_upwards [hc] with _ hc
-- 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₂
c : ℝ
hc_1 : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
a : ℝ
hc : f a = c
⊢ 0 ≤ f a

Tactic:
simpa only [hc]
-- 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₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hpos : 0 ≤ c
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]

Premises used: Or.inl
-- 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₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
inr : ∀ᶠ (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)
heq : c₁ = c₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
h₁ : ∀ (x : ℝ) (hc : f x = c), f x ≤ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
filter_upwards [hc] with x hc
-- 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₂
c : ℝ
hc_1 : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x < 0

Tactic:
simpa only [hc]
-- 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₂
c : ℝ
hc_1 : ∀ᶠ (x : ℝ) in atTop, f x = c
hneg : c < 0
x : ℝ
hc : f x = c
⊢ f x ≤ 0

Tactic:
exact le_of_lt <| by simpa only [hc]

Premises used: le_of_lt
-- 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₂
c : ℝ
hc : ∀ᶠ (x : ℝ) in atTop, f x = c
⊢ 0 ≤ c ∨ c < 0

Tactic:
cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]

Premises used: le_of_lt, le_or_gt, Or.inl, 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)
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
match lt_trichotomy c₁ c₂ with
  | .inl hlt => -- c₁ < c₂
    left
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : 0 ≤ (c₂ - c₁) * f x := by linarith
    exact nonneg_of_mul_nonneg_right hu' (by linarith)
  | .inr (.inr hgt) => -- c₂ < c₁
    right
    filter_upwards [h, eventually_ge_atTop 0] with x hx hx_nonneg
    have h' : 3 / 4 * x ∈ Set.Icc (1 / 2 * x) x := by
      rw [Set.mem_Icc]
      exact ⟨by gcongr ?_ * x; norm_num, by linarith⟩
    have hu := hx (3 / 4 * x) h'
    have hu := Set.nonempty_of_mem hu
    rw [Set.nonempty_Icc] at hu
    have hu' : (c₁ - c₂) * f x ≤ 0 := by linarith
    exact nonpos_of_mul_nonpos_right hu' (by linarith)
  | .inr (.inl heq) => -- c₁ = c₂
    have hmain : ∃ c, ∀ᶠ x in atTop, f x = c := by
      simp only [heq, Set.Icc_self, Set.mem_singleton_iff] at h
      rw [eventually_atTop] at h
      obtain ⟨n₀, hn₀⟩ := h
      refine ⟨f (max n₀ 2), ?_⟩
      rw [eventually_atTop]
      refine ⟨max n₀ 2, ?_⟩
      refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
      case base => grind
      case step =>
        intro n _ _ z _
        have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
        have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
          grind [mul_assoc]
        grind
    obtain ⟨c, hc⟩ := hmain
    cases le_or_gt 0 c with
    | inl hpos =>
      exact Or.inl <| by filter_upwards [hc] with _ hc; simpa only [hc]
    | inr hneg =>
      right
      filter_upwards [hc] with x hc
      exact le_of_lt <| by simpa only [hc]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
pos :
  ∀ (h : ∃ᶠ (x : ℝ) in atTop, f x = 0),
    (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
neg :
  ∀ (h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0),
    (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
by_cases! h : ∃ᶠ x in atTop, f x = 0

Premises used: Filter.atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
Or.inl <| eventually_zero_of_frequently_zero hf h

Premises used: AkraBazziRecurrence.GrowsPolynomially.eventually_zero_of_frequently_zero, Or.inl
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∃ᶠ (x : ℝ) in atTop, f x = 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
exact Or.inl <| eventually_zero_of_frequently_zero hf h

Premises used: AkraBazziRecurrence.GrowsPolynomially.eventually_zero_of_frequently_zero, Or.inl
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (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:
Or.inr (Or.inl ?_)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
neg : ∀ᶠ (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:
refine Or.inr (Or.inl ?_)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
neg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

Tactic:
simp only [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
neg : (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x ∧ 0 ≠ f x

Tactic:
rw [eventually_and]

Premises used: Filter.eventually_and
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
h₁ : ∀ (x : ℝ) (hx : f x ≠ 0), 0 ≠ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : f x ≠ 0
⊢ 0 ≠ f x

Tactic:
hx.symm

Premises used: Ne.symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
x : ℝ
hx : f x ≠ 0
⊢ 0 ≠ f x

Tactic:
exact hx.symm

Premises used: Ne.symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∧ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
Or.inr (Or.inr ?_)

Premises used: Or.inr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
neg : ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
refine Or.inr (Or.inr ?_)

Premises used: Or.inr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
neg : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x < 0

Tactic:
simp only [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
neg : (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0 ∧ f x ≠ 0

Tactic:
rw [eventually_and]

Premises used: Filter.eventually_and
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
⟨h', h⟩

Premises used: And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ (∀ᶠ (x : ℝ) in atTop, f x ≤ 0) ∧ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
exact ⟨h', h⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ (∀ᶠ (x : ℝ) in atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x ≤ 0

Tactic:
cases eventually_atTop_nonneg_or_nonpos hf with
    | inl h' =>
      refine Or.inr (Or.inl ?_)
      simp only [lt_iff_le_and_ne]
      rw [eventually_and]
      exact ⟨h', by filter_upwards [h] with x hx; exact hx.symm⟩
    | inr h' =>
      refine Or.inr (Or.inr ?_)
      simp only [lt_iff_le_and_ne]
      rw [eventually_and]
      exact ⟨h', h⟩

Premises used: Filter.eventually_and, lt_iff_le_and_ne, Or.inl, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
obtain :
  ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)),
    ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (-f) u ∈ Set.Icc (c₁ * (-f) x) (c₂ * (-f) x)

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

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

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

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

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

Tactic:
simp only [Pi.neg_apply, Set.neg_mem_Icc_iff, neg_mul_eq_mul_neg, neg_neg]

Premises used: neg_neg, Set.neg_mem_Icc_iff, neg_mul_eq_mul_neg, Pi.neg_apply
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
hx u hu

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

Tactic:
exact hx u hu
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
rw : GrowsPolynomially (- -f)
⊢ GrowsPolynomially f

Tactic:
rw [← neg_neg f]

Premises used: neg_neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially (- -f)

Tactic:
hf.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially (-f)
⊢ GrowsPolynomially (- -f)

Tactic:
exact hf.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
h : ∀ (x : ℝ) (hx : 0 ≤ f x), f x = |f x|
⊢ f =ᶠ[atTop] fun (x : ℝ) ↦ |f x|

Tactic:
filter_upwards [hf'] with x hx