-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
/-- The main proof of the lower bound part of the Akra-Bazzi theorem. The factor
`1 + ε n` does not change the asymptotic order, but is needed for the induction step to go
through. -/
lemma smoothingFn_mul_asympBound_isBigO_T :
    (fun (n : ℕ) => (1 + ε n) * asympBound g a b n) =O[atTop] T

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_b_floor : 0 < ⌊b' * ↑n₀⌋₊
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 + ε ↑y
h_smoothing_pos' : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 + ε ↑(r i y)
bound2 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b i ^ p a b * ↑y ^ p a b * (1 + ε ↑y) ≤ ↑(r i y) ^ p a b * (1 + ε ↑(r i y))
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), sumTransform (p a b) g (r i y) y ≤ c₁ * g ↑y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_exp : ∀ (y : ℕ), n₀ ≤ y → ⌈rexp 1⌉₊ ≤ y
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_min : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
base_min_def : base_min = (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
C : ℝ := (2 * c₁)⁻¹ ⊓ base_min
m : ℕ
hm_mem : m ∈ Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀
hm :
  ((Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)) =
    T m / ((1 + ε ↑m) * asympBound g a b m)
H₁ : 0 < T m
⊢ 0 < T m / ((1 + ε ↑m) * asympBound g a b m)

Tactic:
have H₂ : 0 < 1 + ε m := by rw [Finset.mem_Ico] at hm_mem
                            exact h_smoothing_pos' m hm_mem.1

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_b_floor : 0 < ⌊b' * ↑n₀⌋₊
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 + ε ↑y
h_smoothing_pos' : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 + ε ↑(r i y)
bound2 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b i ^ p a b * ↑y ^ p a b * (1 + ε ↑y) ≤ ↑(r i y) ^ p a b * (1 + ε ↑(r i y))
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), sumTransform (p a b) g (r i y) y ≤ c₁ * g ↑y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_exp : ∀ (y : ℕ), n₀ ≤ y → ⌈rexp 1⌉₊ ≤ y
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_min : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
base_min_def : base_min = (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
C : ℝ := (2 * c₁)⁻¹ ⊓ base_min
m : ℕ
hm_mem : m ∈ Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀
hm :
  ((Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)) =
    T m / ((1 + ε ↑m) * asympBound g a b m)
H₁ : 0 < T m
H₂ : 0 < 1 + ε ↑m
⊢ 0 < T m / ((1 + ε ↑m) * asympBound g a b m)

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_b_floor : 0 < ⌊b' * ↑n₀⌋₊
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 + ε ↑y
h_smoothing_pos' : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 + ε ↑(r i y)
bound2 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b i ^ p a b * ↑y ^ p a b * (1 + ε ↑y) ≤ ↑(r i y) ^ p a b * (1 + ε ↑(r i y))
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), sumTransform (p a b) g (r i y) y ≤ c₁ * g ↑y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_exp : ∀ (y : ℕ), n₀ ≤ y → ⌈rexp 1⌉₊ ≤ y
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_min : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
base_min_def : base_min = (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
C : ℝ := (2 * c₁)⁻¹ ⊓ base_min
hC_pos : 0 < C
n : ℕ
hn : n ≥ n₀
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, C * ((1 + ε ↑n) * asympBound g a b n) ≤ T n
h_asympBound_pos' : 0 < asympBound g a b n
⊢ C * ‖(1 + ε ↑n) * asympBound g a b n‖ ≤ ‖T n‖

Tactic:
have h_one_sub_smoothingFn_pos' : 0 < 1 + ε n := h_smoothing_pos n hn

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c₁ * g ↑n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_b_floor : 0 < ⌊b' * ↑n₀⌋₊
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 + ε ↑y
h_smoothing_pos' : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 + ε ↑(r i y)
bound2 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b i ^ p a b * ↑y ^ p a b * (1 + ε ↑y) ≤ ↑(r i y) ^ p a b * (1 + ε ↑(r i y))
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 + ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), sumTransform (p a b) g (r i y) y ≤ c₁ * g ↑y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_exp : ∀ (y : ℕ), n₀ ≤ y → ⌈rexp 1⌉₊ ≤ y
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_min : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
base_min_def : base_min = (Ico ⌊b' * ↑n₀⌋₊ n₀).inf' h_base_nonempty fun n => T n / ((1 + ε ↑n) * asympBound g a b n)
C : ℝ := (2 * c₁)⁻¹ ⊓ base_min
hC_pos : 0 < C
n : ℕ
hn : n ≥ n₀
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, C * ((1 + ε ↑n) * asympBound g a b n) ≤ T n
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 + ε ↑n
⊢ C * ‖(1 + ε ↑n) * asympBound g a b n‖ ≤ ‖T n‖