awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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)
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have calc₄ : 3 / 2 * (c₂ * f x) = 3 * c₂ * (1 / 2 * f x)
Tactic: calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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)
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have calc₅ : 3 * c₂ * (1 / 2 * f x) ≤ 3 * c₂ * (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 gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case : f u + g u ≤ f u + ‖g u‖
Tactic: case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
hfg₃ : ‖g u‖ ≤ 1 / 2 * f u
case : f u + g u ≤ f u + ‖g u‖
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case₁ : f u + ‖g u‖ ≤ f u + 1 / 2 * f u
Tactic: case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case₂ : f u + 1 / 2 * f u = 3 / 2 * f u
Tactic: case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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 = 3 / 2 * f u
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case₃ : 3 / 2 * f u ≤ 3 / 2 * (c₂ * f x)
Tactic: case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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 = 3 / 2 * f u
case₃ : 3 / 2 * f u ≤ 3 / 2 * (c₂ * f x)
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case₄ : 3 / 2 * (c₂ * f x) = 3 * c₂ * (1 / 2 * f x)
Tactic: case ub =>
      calc _ ≤ f u + ‖g u‖ := by gcongr; exact le_norm_self (g u)
           _ ≤ f u + 1 / 2 * f u := by gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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, 0 ≤ f x
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 → 0 ≤ f y
hx_nonneg : 0 ≤ x
hbx : b * x ≤ x
hfg₂ : ‖g x‖ ≤ 1 / 2 * f x
hx_ub : f x + g x ≤ 3 / 2 * f x
hx_lb : 1 / 2 * f x ≤ f x + g x
u : ℝ
hu_lb : b * x ≤ u
hu_ub : u ≤ x
hfu_nonneg : 0 ≤ f u
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 = 3 / 2 * f u
case₃ : 3 / 2 * f u ≤ 3 / 2 * (c₂ * f x)
case₄ : 3 / 2 * (c₂ * f x) = 3 * c₂ * (1 / 2 * f x)
⊢ f u + g u ≤ 3 * c₂ * (f x + g x)
have case₅ : 3 * c₂ * (1 / 2 * f x) ≤ 3 * c₂ * (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 gcongr
           _ = 3 / 2 * f u := by ring
           _ ≤ 3 / 2 * (c₂ * f x) := by gcongr; exact (hf₁ u ⟨hu_lb, hu_ub⟩).2
           _ = 3 * c₂ * (1 / 2 * f x) := by ring
           _ ≤ 3 * c₂ * (f x + g x) := by gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ * (fun (x : ℝ) ↦ f x + g x) x)
have hf₁ : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: have hf := hf b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hb_ub : b < 1
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≤ 0
hf : ∃ 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,
          (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ * (fun (x : ℝ) ↦ f x + g x) x)
have inr : ∀ (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)),
  ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ * (fun (x : ℝ) ↦ f x + g x) x)
Tactic: obtain ⟨c₁, hc₁_mem : 0 < c₁, c₂, hc₂_mem : 0 < c₂, hf⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hf_1 : GrowsPolynomially f
hfg : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ c * ‖f x‖
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)
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ * (fun (x : ℝ) ↦ f x + g x) x)
have hfg₁ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 1 / 2 * ‖f x‖
Tactic: specialize hfg (c := 1 / 2) (by norm_num)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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‖
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop,
        ∀ u ∈ Set.Icc (b * x) x,
          (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ * (fun (x : ℝ) ↦ f x + g x) x)
have inr : ∀ᶠ (x : ℝ) in atTop,
  ∀ u ∈ Set.Icc (b * x) x,
    (fun (x : ℝ) ↦ f x + g x) u ∈ Set.Icc (3 * c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ / 3 * (fun (x : ℝ) ↦ f x + g x) x)
Tactic: refine ⟨3*c₁, by positivity, c₂/3, by positivity, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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 : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x,
      (fun (x : ℝ) ↦ f x + g x) u ∈
        Set.Icc (3 * c₁ * (fun (x : ℝ) ↦ f x + g x) x) (c₂ / 3 * (fun (x : ℝ) ↦ f x + g x) x)
have h : ∀ (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), ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))
Tactic: filter_upwards [hf,
                    (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg,
                    (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hf',
                    eventually_ge_atTop 0] with x hf₁ hfg' hf₂ hx_nonneg
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ b * x ≤ x
have nth_rewrite : b * x ≤ 1 * x
Tactic: nth_rewrite 2 [← one_mul x]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))
have hbx : b * x ≤ x
Tactic: have hbx : b * x ≤ x := by nth_rewrite 2 [← one_mul x]; gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ 1 / 2 * ‖f x‖ = 1 / 2 * -f x
have e_a : ‖f x‖ = -f x
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ ‖g x‖ ≤ -1 / 2 * f x
have calc : 1 / 2 * ‖f x‖ = 1 / 2 * -f x
Tactic: calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
           _ = 1 / 2 * (-f x) := by congr; exact norm_of_nonpos (hf₂ x hbx)
           _ = _ := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
calc : 1 / 2 * ‖f x‖ = 1 / 2 * -f x
⊢ ‖g x‖ ≤ -1 / 2 * f x
have calc₁ : 1 / 2 * -f x = -1 / 2 * f x
Tactic: calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
           _ = 1 / 2 * (-f x) := by congr; exact norm_of_nonpos (hf₂ x hbx)
           _ = _ := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))
have hfg₂ : ‖g x‖ ≤ -1 / 2 * f x
Tactic: have hfg₂ : ‖g x‖ ≤ -1 / 2 * f x := by
      calc ‖g x‖ ≤ 1 / 2 * ‖f x‖ := hfg' x hbx
           _ = 1 / 2 * (-f x) := by congr; exact norm_of_nonpos (hf₂ x hbx)
           _ = _ := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ f x + g x ≤ f x + ‖g x‖
have bc : g x ≤ ‖g x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
⊢ f x + g x ≤ 1 / 2 * f x
have calc : f x + g x ≤ f x + ‖g x‖
Tactic: calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + (-1 / 2 * f x) := by gcongr
           _ = 1 / 2 * f x := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
calc : f x + g x ≤ f x + ‖g x‖
⊢ f x + g x ≤ 1 / 2 * f x
have calc₁ : f x + ‖g x‖ ≤ f x + -1 / 2 * f x
Tactic: calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + (-1 / 2 * f x) := by gcongr
           _ = 1 / 2 * f x := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
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
calc : f x + g x ≤ f x + ‖g x‖
calc₁ : f x + ‖g x‖ ≤ f x + -1 / 2 * f x
⊢ f x + g x ≤ 1 / 2 * f x
have calc₂ : f x + -1 / 2 * f x = 1 / 2 * f x
Tactic: calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + (-1 / 2 * f x) := by gcongr
           _ = 1 / 2 * f x := by ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
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
⊢ ∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (3 * c₁ * (f x + g x)) (c₂ / 3 * (f x + g x))
have hx_ub : f x + g x ≤ 1 / 2 * f x
Tactic: have hx_ub : f x + g x ≤ 1 / 2 * f x := by
      calc _ ≤ f x + ‖g x‖ := by gcongr; exact le_norm_self (g x)
           _ ≤ f x + (-1 / 2 * f x) := by gcongr
           _ = 1 / 2 * f x := by ring