-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isBigO_apply_r_sub_b (q : ℝ → ℝ) (hq_diff : DifferentiableOn ℝ q (Set.Ioi 1))
    (hq_poly : GrowsPolynomially fun x => ‖deriv q x‖) (i : α) :
    (fun n => q (r i n) - q (b i * n)) =O[atTop] fun n => (deriv q n) * (r i n - b i * n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
⊢ (fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
have hb' : ∀ i, b' ≤ b i := fun i => calc
  b (min_bi b) / 2 ≤ b i / 2 := by gcongr; aesop
             _ ≤ b i := by exact le_of_lt <| div_two_lt_of_pos (R.b_pos i)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
⊢ (fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
⊢ (fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
have hb_lt_one : b' < 1 := calc
  b (min_bi b) / 2 < b (min_bi b) := by exact div_two_lt_of_pos (R.b_pos (min_bi b))
                 _ < 1 := R.b_lt_one (min_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
⊢ (fun n => q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n => deriv q ↑n * (↑(r i n) - b i * ↑n)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c * ‖deriv q ↑x * (↑(r i x) - b i * ↑x)‖

Tactic:
refine ⟨c₂, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly✝ : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
hb' : ∀ (i : α), b' ≤ b i
c₁ : ℝ
left✝¹ : c₁ > 0
c₂ : ℝ
left✝ : c₂ > 0
hq_poly :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b' * x) x,
      (fun x => ‖deriv q x‖) u ∈ Set.Icc (c₁ * (fun x => ‖deriv q x‖) x) (c₂ * (fun x => ‖deriv q x‖) x)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖q ↑(r i x) - q (b i * ↑x)‖ ≤ c₂ * ‖deriv q ↑x * (↑(r i x) - b i * ↑x)‖

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i✝ : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
i : α
⊢ b (min_bi b) / 2 ≤ b i / 2

Tactic:
gcongr

Result:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i✝ : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
hb : b' ∈ Set.Ioo 0 1
i : α
⊢ b (min_bi b) ≤ b i

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
⊢ 0 < b'

Tactic:
have := R.b_pos (min_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x => ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
this : 0 < b (min_bi b)
⊢ 0 < b'