∀ {α : Type u_1} {inst : Fintype α} {inst_1 : Nonempty α} {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} {n₀ : ℕ}
  {n₀_gt_zero : 0 < n₀} {a_pos : ∀ (i : α), 0 < a i} {b_pos : ∀ (i : α), 0 < b i} {b_lt_one : ∀ (i : α), b i < 1}
  {g_nonneg : ∀ x ≥ 0, 0 ≤ g x} {g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g}
  {h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n} {T_gt_zero' : ∀ n < n₀, 0 < T n}
  {r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n}
  {dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2} {n₀_1 : ℕ}
  {n₀_gt_zero_1 : 0 < n₀_1} {a_pos_1 : ∀ (i : α), 0 < a i} {b_pos_1 : ∀ (i : α), 0 < b i}
  {b_lt_one_1 : ∀ (i : α), b i < 1} {g_nonneg_1 : ∀ x ≥ 0, 0 ≤ g x}
  {g_grows_poly_1 : AkraBazziRecurrence.GrowsPolynomially g}
  {h_rec_1 : ∀ (n : ℕ), n₀_1 ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n} {T_gt_zero'_1 : ∀ n < n₀_1, 0 < T n}
  {r_lt_n_1 : ∀ (i : α) (n : ℕ), n₀_1 ≤ n → r i n < n}
  {dist_r_b_1 : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2},
  { n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
        g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n,
        dist_r_b := dist_r_b } =
      { n₀ := n₀_1, n₀_gt_zero := n₀_gt_zero_1, a_pos := a_pos_1, b_pos := b_pos_1, b_lt_one := b_lt_one_1,
        g_nonneg := g_nonneg_1, g_grows_poly := g_grows_poly_1, h_rec := h_rec_1, T_gt_zero' := T_gt_zero'_1,
        r_lt_n := r_lt_n_1, dist_r_b := dist_r_b_1 } →
    n₀ = n₀_1