awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)

Tactic:
hf.tendsto_zero_of_antitone _ _ Nat.mono_cast.neg
    (tendsto_neg_atBot_iff.mpr tendsto_natCast_atTop_atTop)

Premises used: Iff.mpr, Nat.mono_cast, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone, Filter.tendsto_neg_atBot_iff, Monotone.neg, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)

Tactic:
exact hf.tendsto_zero_of_antitone _ _ Nat.mono_cast.neg
    (tendsto_neg_atBot_iff.mpr tendsto_natCast_atTop_atTop)

Premises used: Iff.mpr, Nat.mono_cast, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone, Filter.tendsto_neg_atBot_iff, Monotone.neg, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
h :
  ∀ (c : β) (hc : ∀ (q : ℚ), 0 ≤ f (a, c) q) (q : ℚ),
    BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))

Tactic:
filter_upwards [hf.nonneg a] with c hc

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))

Tactic:
fun q ↦ ⟨0, ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
h : ∀ (q : ℚ), Membership.mem (γ := Set ℝ) (lowerBounds (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))) 0
⊢ ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))

Tactic:
refine fun q ↦ ⟨0, ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
q : ℚ
⊢ Membership.mem (γ := Set ℝ) (lowerBounds (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, c) (↑r : ℚ))) 0

Tactic:
simp [mem_lowerBounds, hc]

Premises used: mem_lowerBounds
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
rw :
  MemLp (ε := ℝ) (m0 := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ((ν : (a : α) → Measure β) a)

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ MemLp (ε := ℝ) (m0 := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a)

Tactic:
⟨(Measurable.iInf fun i ↦ hf.measurable_right a _).aestronglyMeasurable, ?_⟩

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.MemLp, ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right, And.intro, Measurable.iInf
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
refine :
  @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) < ∞
⊢ MemLp (ε := ℝ) (m0 := mβ) (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a)

Tactic:
refine ⟨(Measurable.iInf fun i ↦ hf.measurable_right a _).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) < ∞

Tactic:
(?_ : _ ≤ (ν a univ : ℝ≥0∞)).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
refine :
  @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) ≤
    (((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ
⊢ @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) < ∞

Tactic:
refine (?_ : _ ≤ (ν a univ : ℝ≥0∞)).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
⊢ HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
        (ENNReal.toReal 1)⁻¹ *
      ENNReal.ofReal 1 ≤
    (((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
refine :
  ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) ≤ 1
⊢ @eLpNorm _ ℝ _ mβ (fun (t : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1 ((ν : (a : α) → Measure β) a) ≤
    (((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) ?_).trans (by simp)

Premises used: LE.le.trans, MeasureTheory.eLpNorm_le_of_ae_bound
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
h :
  ∀ (t : β) (hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ)))
    (h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q) (h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1),
    norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤ 1
⊢ ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) ≤ 1

Tactic:
filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a]
    with t hbdd_below h_nonneg h_le_one

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg, ProbabilityTheory.IsRatCondKernelCDFAux.le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
h : LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1
h₁ : LE.le (α := ℝ) 0 (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))
⊢ norm (E := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) ≤ 1

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1

Tactic:
ciInf_le_of_le ?_ ?_ ?_

Premises used: ciInf_le_of_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
h : BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h₁ : (↑(Ioi q) : Type)
h₂ : f (a, t) (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi q) (q + 1) ⋯) : ℚ) ≤ 1
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) 1

Tactic:
refine ciInf_le_of_le ?_ ?_ ?_

Premises used: ciInf_le_of_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))

Tactic:
hbdd_below _
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))

Tactic:
exact hbdd_below _
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ q + 1 ∈ Ioi q

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ (↑(Ioi q) : Type)

Tactic:
exact ⟨q + 1, by simp⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi q) (q + 1) ⋯) : ℚ) ≤ 1

Tactic:
h_le_one _
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi q) (q + 1) ⋯) : ℚ) ≤ 1

Tactic:
exact h_le_one _
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ LE.le (α := ℝ) 0 (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))

Tactic:
le_ciInf fun r ↦ h_nonneg _

Premises used: le_ciInf, Subtype.val
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (α := ℝ) (range fun (r : (↑(Ioi q) : Type)) ↦ f (a, t) (↑r : ℚ))
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ LE.le (α := ℝ) 0 (⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ))

Tactic:
exact le_ciInf fun r ↦ h_nonneg _

Premises used: le_ciInf
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
rw :
  Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
hs₁ :
  Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : { r' : ℚ // t < r' }) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))
hsm : ∀ (i : { r' : ℚ // t < r' }), NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ρ
hfin :
  ∃ (i : { r' : ℚ // t < r' }),
    Ne (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)

Tactic:
rw [← Monotone.measure_iInter]

Premises used: Monotone.measure_iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
rw :
  Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : { r' : ℚ // t < r' }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)

Tactic:
rw [← prod_iInter]

Premises used: Set.prod_iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ)) x ↔
      Membership.mem (γ := Set ℝ) (Iic (↑t : ℝ)) x
⊢ Eq (α := ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)

Tactic:
congr with x : 1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // t < r' }), Iic (↑(↑i : ℚ) : ℝ)) x ↔
    Membership.mem (γ := Set ℝ) (Iic (↑t : ℝ)) x

Tactic:
simp only [mem_iInter, mem_Iic, Subtype.forall]

Premises used: Subtype.forall, Set.mem_iInter, Set.mem_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)

Tactic:
⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩

Premises used: Iff.intro, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)), x ≤ (↑t : ℝ)
h₁ : ∀ (h : x ≤ (↑t : ℝ)) (a : ℚ) (hta : t < a), LE.le (α := ℝ) (↑t : ℝ) (↑a : ℝ)
⊢ (∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)) ↔ x ≤ (↑t : ℝ)

Tactic:
refine ⟨fun h ↦ ?_, fun h a hta ↦ h.trans ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)
⊢ x ≤ (↑t : ℝ)

Tactic:
le_of_forall_lt_rat_imp_le fun q htq ↦ h q ?_

Premises used: le_of_forall_lt_rat_imp_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)
h₁ : ∀ (q : ℚ) (htq : LT.lt (α := ℝ) (↑t : ℝ) (↑q : ℝ)), t < q
⊢ x ≤ (↑t : ℝ)

Tactic:
refine le_of_forall_lt_rat_imp_le fun q htq ↦ h q ?_

Premises used: le_of_forall_lt_rat_imp_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)
q : ℚ
htq : LT.lt (α := ℝ) (↑t : ℝ) (↑q : ℝ)
⊢ t < q

Tactic:
mod_cast htq

Premises used: cast, Rat.cast_lt._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ) (b : t < a), x ≤ (↑a : ℝ)
q : ℚ
htq : LT.lt (α := ℝ) (↑t : ℝ) (↑q : ℝ)
⊢ t < q

Tactic:
exact mod_cast htq
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : x ≤ (↑t : ℝ)
a : ℚ
hta : t < a
⊢ LE.le (α := ℝ) (↑t : ℝ) (↑a : ℝ)

Tactic:
mod_cast hta.le

Premises used: cast, LT.lt.le, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : x ≤ (↑t : ℝ)
a : ℚ
hta : t < a
⊢ LE.le (α := ℝ) (↑t : ℝ) (↑a : ℝ)

Tactic:
exact mod_cast hta.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
r r' : { r' : ℚ // t < r' }
hrr' : r ≤ r'
⊢ Subset (α := Set ℝ) (Iic (↑(↑r : ℚ) : ℝ)) (Iic (↑(↑r' : ℚ) : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : { r' : ℚ // t < r' }) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))

Tactic:
exact fun r r' hrr' ↦ prod_mono_right <| by gcongr

Premises used: Set.prod_mono_right
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∀ (i : { r' : ℚ // t < r' }), NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ρ

Tactic:
fun _ => (hs.prod measurableSet_Iic).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasurableSet.prod, measurableSet_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∀ (i : { r' : ℚ // t < r' }), NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ρ

Tactic:
exact fun _ => (hs.prod measurableSet_Iic).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasurableSet.prod, measurableSet_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ (i : { r' : ℚ // t < r' }),
    Ne (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨⟨t + 1, lt_add_one _⟩, measure_ne_top ρ _⟩

Premises used: lt_add_one, MeasureTheory.measure_ne_top, Subtype.mk, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ (i : { r' : ℚ // t < r' }),
    Ne (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨⟨t + 1, lt_add_one _⟩, measure_ne_top ρ _⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) A) fun (t : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) A (Iic (↑q : ℝ)))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm