awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
a : ℝ
hx : 0 < f a
⊢ f a ≠ 0

Tactic:
exact (ne_of_lt hx).symm

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

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

Tactic:
(ne_of_gt hx).symm

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

Tactic:
exact (ne_of_gt hx).symm

Premises used: ne_of_gt, Ne.symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
inl : ∀ (H : ∀ᶠ (x : ℝ) in atTop, 0 < f x), ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
inr : ∀ (H : ∀ᶠ (x : ℝ) in atTop, f x < 0), ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ ∀ᶠ (x : ℝ) in atTop, f x ≠ 0

Tactic:
have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
inr : GrowsPolynomially fun (x : ℝ) ↦ |f x|⁻¹
⊢ GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|

Tactic:
simp only [abs_inv]

Premises used: abs_inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
⊢ GrowsPolynomially fun (x : ℝ) ↦ |f x|

Tactic:
have hf := hf.abs
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ 0 < b

Tactic:
have hb_pos := hb.1
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
inr :
  ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
    (hf :
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)),
    ∃ c₁ > 0,
      ∃ c₂ > 0,
        ∀ᶠ (x : ℝ) in atTop,
          ∀ u ∈ Set.Icc (b * x) x,
            (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₂ * (fun (x : ℝ) ↦ |f x|⁻¹) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₂ * (fun (x : ℝ) ↦ |f x|⁻¹) x)

Tactic:
obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
⊢ 0 < c₂⁻¹

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
inr :
  ∃ c₂_1 > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₂_1 * (fun (x : ℝ) ↦ |f x|⁻¹) x)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₂ * (fun (x : ℝ) ↦ |f x|⁻¹) x)

Tactic:
refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
⊢ 0 < c₁⁻¹

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
inr :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₁⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x)
⊢ ∃ c₂_1 > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₂_1 * (fun (x : ℝ) ↦ |f x|⁻¹) x)

Tactic:
refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
h :
  ∀ (x : ℝ) (hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)) (hx' : f x ≠ 0)
    (hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0),
    ∀ 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,
      (fun (x : ℝ) ↦ |f x|⁻¹) u ∈ Set.Icc (c₂⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x) (c₁⁻¹ * (fun (x : ℝ) ↦ |f x|⁻¹) x)

Tactic:
filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx' hx''

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_id, Filter.Tendsto.eventually_forall_ge_atTop
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
rw : f u ≠ 0
⊢ 0 < |f u|

Tactic:
rw [abs_pos]

Premises used: abs_pos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ≠ 0

Tactic:
hx'' u hu.1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ≠ 0

Tactic:
exact hx'' u hu.1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ 0 < |f u|

Tactic:
have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
⟨?lb, ?ub⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
refine : c₂⁻¹ * |f x|⁻¹ ≤ |f u|⁻¹
refine₁ : |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹
⊢ |f u|⁻¹ ∈ Set.Icc (c₂⁻¹ * |f x|⁻¹) (c₁⁻¹ * |f x|⁻¹)

Tactic:
refine ⟨?lb, ?ub⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
rw : (c₂ * |f x|)⁻¹ ≤ |f u|⁻¹
⊢ c₂⁻¹ * |f x|⁻¹ ≤ |f u|⁻¹

Tactic:
rw [← mul_inv]

Premises used: mul_inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
hba : |f u| ≤ c₂ * |f x|
⊢ (c₂ * |f x|)⁻¹ ≤ |f u|⁻¹

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u| ≤ c₂ * |f x|

Tactic:
(hx u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u| ≤ c₂ * |f x|

Tactic:
exact (hx u hu).2

Premises used: And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ c₂⁻¹ * |f x|⁻¹ ≤ |f u|⁻¹

Tactic:
case lb =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).2

Premises used: mul_inv, And.right
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
rw : |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹

Tactic:
rw [← mul_inv]

Premises used: mul_inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
hba : c₁ * |f x| ≤ |f u|
⊢ |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ c₁ * |f x| ≤ |f u|

Tactic:
(hx u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ c₁ * |f x| ≤ |f u|

Tactic:
exact (hx u hu).1

Premises used: And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf_1 : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf_2 : GrowsPolynomially fun (x : ℝ) ↦ |f x|
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ |f x|) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ |f x|) x) (c₂ * (fun (x : ℝ) ↦ |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
case case₁ case₂ : |f u|⁻¹ ≤ (c₁ * |f x|)⁻¹
hba : c₁ * |f x| ≤ |f u|
⊢ |f u|⁻¹ ≤ c₁⁻¹ * |f x|⁻¹

Tactic:
case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1

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

Tactic:
cases hf.eventually_atTop_zero_or_pos_or_neg with
  | inl hf' =>
    refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
    have hb_pos := hb.1
    filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx'
    intro u hu
    simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]
  | inr hf_pos_or_neg =>
    suffices GrowsPolynomially fun x => |(f x)⁻¹| by
      cases hf_pos_or_neg with
      | inl hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
        rwa [iff_eventuallyEq hmain]
      | inr hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
        rw [iff_eventuallyEq hmain]
        exact this.neg
    have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
    simp only [abs_inv]
    have hf := hf.abs
    intro b hb
    have hb_pos := hb.1
    obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
    refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
    refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
    filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx' hx''
    intro u hu
    have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
    refine ⟨?lb, ?ub⟩
    case lb =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).2
    case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1

Premises used: Set.Icc_self, mul_inv, inv_zero, abs_inv, MulZeroClass.mul_zero, Set.mem_singleton_iff, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_zero_or_pos_or_neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
h : ∀ (x : ℝ), f x / g x = f x * (g x)⁻¹
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹

Tactic:
ext
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
x : ℝ
h h₁ : f x * (g x)⁻¹ = f x * (g x)⁻¹
⊢ f x / g x = f x * (g x)⁻¹

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hg : GrowsPolynomially g
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ f x / g x) fun (x : ℝ) ↦ f x * (g x)⁻¹

Tactic:
have : (fun x => f x / g x) = fun x => f x * (g x)⁻¹ := by ext; rw [div_eq_mul_inv]