awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
calc : f u + g u ≥ f u - ‖g u‖
calc₁ : f u - ‖g u‖ ≥ f u + 1 / 2 * f u
calc₂ : f u + 1 / 2 * f u = 3 / 2 * f u
calc₃ : 3 / 2 * f u ≥ 3 / 2 * (c₁ * f x)
calc₄ : 3 / 2 * (c₁ * f x) = 3 * c₁ * (1 / 2 * f x)
calc₅ : 3 * c₁ * (1 / 2 * f x) ≥ 3 * c₁ * (f x + g x)
⊢ 3 * c₁ * (f x + g x) ≤ f u + g u

Tactic:
calc f u + g u ≥ f u - ‖g u‖ := by
                  rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le _
           _ ≥ f u + 1 / 2 * f u := by
                  rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?_
                  rwa [neg_neg, ← neg_mul, ← neg_div]
           _ = 3 / 2 * f u := by ring
           _ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
           _ = 3 * c₁ * (1 / 2 * f x) := by ring
           _ ≥ 3 * c₁ * (f x + g x) := by gcongr

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ 3 * c₁ * (f x + g x) ≤ f u + g u

Tactic:
case lb =>
      calc f u + g u ≥ f u - ‖g u‖ := by
                  rw [sub_eq_add_neg, norm_eq_abs]; gcongr; exact neg_abs_le _
           _ ≥ f u + 1 / 2 * f u := by
                  rw [sub_eq_add_neg]
                  gcongr
                  refine le_of_neg_le_neg ?_
                  rwa [neg_neg, ← neg_mul, ← neg_div]
           _ = 3 / 2 * f u := by ring
           _ ≥ 3 / 2 * (c₁ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).1
           _ = 3 * c₁ * (1 / 2 * f x) := by ring
           _ ≥ 3 * c₁ * (f x + g x) := by gcongr

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
bc : g u ≤ ‖g u‖
⊢ f u + g u ≤ f u + ‖g u‖

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ g u ≤ ‖g u‖

Tactic:
le_norm_self (g u)

Premises used: Real.le_norm_self
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ g u ≤ ‖g u‖

Tactic:
exact le_norm_self (g u)

Premises used: Real.le_norm_self
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
bc : ‖g u‖ ≤ -(1 / 2 * f u)
⊢ f u + ‖g u‖ ≤ f u + -(1 / 2 * f u)

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
bc : ‖g u‖ ≤ -(1 / 2) * f u
bc₁ bc₂ bc₃ bc₄ : ‖g u‖ ≤ -1 / 2 * f u
⊢ ‖g u‖ ≤ -(1 / 2 * f u)

Tactic:
rwa [← neg_mul, ← neg_div]

Premises used: neg_div, neg_mul
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u - 1 / 2 * f u = 1 / 2 * f u

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
hbc : f u ≤ c₂ * f x
⊢ 1 / 2 * f u ≤ 1 / 2 * (c₂ * f x)

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u ≤ c₂ * f x

Tactic:
(hf₁ u ⟨hu_lb, hu_ub⟩).2

Premises used: And.right, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ f u ≤ c₂ * f x

Tactic:
exact (hf₁ u ⟨hu_lb, hu_ub⟩).2

Premises used: And.right, And.intro
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
⊢ 1 / 2 * (c₂ * f x) = c₂ / 3 * (3 / 2 * f x)

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
ha : 0 ≤ c₂ / 3
⊢ c₂ / 3 * (3 / 2 * f x) ≤ c₂ / 3 * (f x + g x)

Tactic:
gcongr
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
calc : f u + g u ≤ f u + ‖g u‖
calc₁ : f u + ‖g u‖ ≤ f u - 1 / 2 * f u
calc₂ : f u - 1 / 2 * f u = 1 / 2 * f u
calc₃ : 1 / 2 * f u ≤ 1 / 2 * (c₂ * f x)
calc₄ : 1 / 2 * (c₂ * f x) = c₂ / 3 * (3 / 2 * f x)
calc₅ : c₂ / 3 * (3 / 2 * f x) ≤ c₂ / 3 * (f x + g x)
⊢ f u + g u ≤ c₂ / 3 * (f x + g x)

Tactic:
calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u - 1 / 2 * f u := by
                rw [sub_eq_add_neg]
                gcongr
                rwa [← neg_mul, ← neg_div]
           _ = 1 / 2 * f u := by ring
           _ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = c₂ / 3 * (3 / 2 * f x) := by ring
           _ ≤ c₂ / 3 * (f x + g x) := by gcongr

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : 0 < c₂
hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
x : ℝ
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hfg' : ∀ (y : ℝ), b * id x ≤ y → ‖g y‖ ≤ 1 / 2 * ‖f y‖
hf₂ : ∀ (y : ℝ), b * id x ≤ y → f y ≤ 0
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
hx_ub : f x + g x ≤ 1 / 2 * f x
hx_lb : 3 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonpos : f u ≤ 0
hfg₃ : ‖g u‖ ≤ -1 / 2 * f u
case : f u + g u ≤ f u + ‖g u‖
case₁ : f u + ‖g u‖ ≤ f u - 1 / 2 * f u
case₂ : f u - 1 / 2 * f u = 1 / 2 * f u
case₃ : 1 / 2 * f u ≤ 1 / 2 * (c₂ * f x)
case₄ : 1 / 2 * (c₂ * f x) = c₂ / 3 * (3 / 2 * f x)
case₅ : c₂ / 3 * (3 / 2 * f x) ≤ c₂ / 3 * (f x + g x)
⊢ f u + g u ≤ c₂ / 3 * (f x + g x)

Tactic:
case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u - 1 / 2 * f u := by
                rw [sub_eq_add_neg]
                gcongr
                rwa [← neg_mul, ← neg_div]
           _ = 1 / 2 * f u := by ring
           _ ≤ 1 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = c₂ / 3 * (3 / 2 * f x) := by ring
           _ ≤ c₂ / 3 * (f x + g x) := by gcongr

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ GT.gt (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
inl :
  ∀ (b : ℝ) (hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b),
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x,
        (fun (x : ℝ) ↦ (f x)⁻¹) u ∈
          Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ (f x)⁻¹) x)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ (f x)⁻¹) x))
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹

Tactic:
refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
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 : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
h :
  ∀ (x : ℝ) (hx : f x = 0) (hx' : ∀ (y : ℝ), b * id x ≤ y → f y = 0),
    ∀ u ∈ Set.Icc (b * x) x, (f u)⁻¹ ∈ Set.Icc (1 * (f x)⁻¹) (1 * (f x)⁻¹)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ (f x)⁻¹) u ∈
        Set.Icc (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ (f x)⁻¹) x)) (HMul.hMul (α := ℝ) 1 ((fun (x : ℝ) ↦ (f x)⁻¹) x))

Tactic:
filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x 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 : GrowsPolynomially f
hf' : ∀ᶠ (x : ℝ) in atTop, f x = 0
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_pos : 0 < b
x : ℝ
hx : f x = 0
hx' : ∀ (y : ℝ), b * id x ≤ y → f y = 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ (f u)⁻¹ ∈ Set.Icc (1 * (f x)⁻¹) (1 * (f x)⁻¹)

Tactic:
simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]

Premises used: Set.Icc_self, inv_zero, MulZeroClass.mul_zero, Set.mem_singleton_iff, And.left
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
h : ∀ (x : ℝ) (hx₁ : 0 < f x), (f x)⁻¹ = |(f x)⁻¹|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ |(f x)⁻¹|

Tactic:
filter_upwards [hf'] with x hx₁
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
hx₁ : 0 < f x
h h₁ : (f x)⁻¹ = (f x)⁻¹
⊢ (f x)⁻¹ = |(f x)⁻¹|

Tactic:
rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]

Premises used: le_of_lt, inv_nonneg_of_nonneg, abs_of_nonneg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ |(f x)⁻¹|

Tactic:
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₁))]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ |(f x)⁻¹|
inl inl₁ inl₂ inl₃ : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹

Tactic:
rwa [iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
h : ∀ (x : ℝ) (hx₁ : f x < 0), (f x)⁻¹ = -|(f x)⁻¹|
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ -|(f x)⁻¹|

Tactic:
filter_upwards [hf'] with x hx₁
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
x : ℝ
hx₁ : f x < 0
⊢ (f x)⁻¹ = -|(f x)⁻¹|

Tactic:
simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]

Premises used: Iff.mpr, le_of_lt, abs_of_nonpos, inv_nonpos
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ -|(f x)⁻¹|

Tactic:
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₁))]
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ -|(f x)⁻¹|
inr : GrowsPolynomially fun (x : ℝ) ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹

Tactic:
rw [iff_eventuallyEq hmain]

Premises used: AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -|(f x)⁻¹|

Tactic:
this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0
hmain : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (f x)⁻¹) fun (x : ℝ) ↦ -|(f x)⁻¹|
⊢ GrowsPolynomially fun (x : ℝ) ↦ -|(f x)⁻¹|

Tactic:
exact this.neg

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- 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
this : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
inl : ∀ (hf' : ∀ᶠ (x : ℝ) in atTop, 0 < f x), GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹
inr : ∀ (hf' : ∀ᶠ (x : ℝ) in atTop, f x < 0), GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹

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

Premises used: AkraBazziRecurrence.GrowsPolynomially.neg
-- 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
inr : GrowsPolynomially fun (x : ℝ) ↦ |(f x)⁻¹|
⊢ GrowsPolynomially fun (x : ℝ) ↦ (f x)⁻¹

Tactic:
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
-- Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially
Goal:
f : ℝ → ℝ
hf : GrowsPolynomially f
H : ∀ᶠ (x : ℝ) in atTop, 0 < f x
h : ∀ (a : ℝ) (hx : 0 < f a), 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, 0 < f x
a : ℝ
hx : 0 < f a
⊢ f a ≠ 0

Tactic:
(ne_of_lt hx).symm

Premises used: Ne.symm, ne_of_lt