{α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : Nonempty α] →
      {T : ℕ → ℝ} →
        {g : ℝ → ℝ} →
          {a b : α → ℝ} →
            {r : α → ℕ → ℕ} →
              {motive : AkraBazziRecurrence T g a b r → Sort u} →
                (t : AkraBazziRecurrence 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) →
                                          motive
                                            { 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 }) →
                    motive t