{α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {f : α × β → ℚ → ℝ} →
          {κ : ProbabilityTheory.Kernel α (β × ℝ)} →
            {ν : ProbabilityTheory.Kernel α β} →
              {motive : ProbabilityTheory.IsRatCondKernelCDF f κ ν → Sort u} →
                (t : ProbabilityTheory.IsRatCondKernelCDF f κ ν) →
                  ((measurable : Measurable f) →
                      (isRatStieltjesPoint_ae :
                          ∀ (a : α), ∀ᵐ (b : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, b)) →
                        (integrable : ∀ (a : α) (q : ℚ), MeasureTheory.Integrable (fun b => f (a, b) q) (ν a)) →
                          (setIntegral :
                              ∀ (a : α) {s : Set β},
                                MeasurableSet s →
                                  ∀ (q : ℚ), ∫ (b : β) in s, f (a, b) q ∂ν a = (κ a).real (s ×ˢ Set.Iic ↑q)) →
                            motive ⋯) →
                    motive t