{motive : BoundingSieve → Sort u} →
  (t : BoundingSieve) →
    ((support : Finset ℕ) →
        (prodPrimes : ℕ) →
          (prodPrimes_squarefree : Squarefree prodPrimes) →
            (weights : ℕ → ℝ) →
              (weights_nonneg : ∀ (n : ℕ), 0 ≤ weights n) →
                (totalMass : ℝ) →
                  (nu : ArithmeticFunction ℝ) →
                    (nu_mult : nu.IsMultiplicative) →
                      (nu_pos_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → 0 < nu p) →
                        (nu_lt_one_of_prime : ∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → nu p < 1) →
                          motive
                            { support := support, prodPrimes := prodPrimes,
                              prodPrimes_squarefree := prodPrimes_squarefree, weights := weights,
                              weights_nonneg := weights_nonneg, totalMass := totalMass, nu := nu, nu_mult := nu_mult,
                              nu_pos_of_prime := nu_pos_of_prime, nu_lt_one_of_prime := nu_lt_one_of_prime }) →
      motive t