{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {f : α × β → ℚ → ℝ} →
          {κ : ProbabilityTheory.Kernel α (β × ℝ)} →
            {ν : ProbabilityTheory.Kernel α β} →
              {motive : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → Sort u} →
                ((measurable : Measurable f) →
                    (mono' : ∀ (a : α) {q r : ℚ}, q ≤ r → ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ f (a, c) r) →
                      (nonneg' : ∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, 0 ≤ f (a, c) q) →
                        (le_one' : ∀ (a : α) (q : ℚ), ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ 1) →
                          (tendsto_integral_of_antitone :
                              ∀ (a : α) (seq : ℕ → ℚ),
                                Antitone seq →
                                  Filter.Tendsto seq Filter.atTop Filter.atBot →
                                    Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop (nhds 0)) →
                            (tendsto_integral_of_monotone :
                                ∀ (a : α) (seq : ℕ → ℚ),
                                  Monotone seq →
                                    Filter.Tendsto seq Filter.atTop Filter.atTop →
                                      Filter.Tendsto (fun m => ∫ (c : β), f (a, c) (seq m) ∂ν a) Filter.atTop
                                        (nhds ((ν a).real Set.univ))) →
                              (integrable : ∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun c => f (a, c) q) (ν a)) →
                                (setIntegral :
                                    ∀ (a : α) {A : Set β},
                                      MeasurableSet A →
                                        ∀ (q : ℚ), ∫ (c : β) in A, f (a, c) q ∂ν a = (κ a).real (A ×ˢ Set.Iic ↑q)) →
                                  motive ⋯) →
                  (t : ProbabilityTheory.IsRatCondKernelCDFAux f κ ν) → motive t