awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) atBot
    (𝓝 0)

Tactic:
rw [← h_empty, ← Real.iInter_Iic_rat, prod_iInter]

Premises used: Real.iInter_Iic_rat, Set.prod_iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
h :
  ∀ (x : α × ℝ),
    Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) x ↔
      Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) x
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))

Tactic:
ext1 x
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
⊢ Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) x ↔
    Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) x

Tactic:
push _ ∈ _
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
⊢ (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)

Tactic:
⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩

Premises used: And.left, And.intro, Iff.intro
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) (i : ℚ), x.2 ≤ (↑i : ℝ)
h₁ : ∀ (h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)) (i : ℚ), x.2 ≤ (↑(-i) : ℝ)
⊢ (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)

Tactic:
refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
⊢ x.1 ∈ s ∧ x.2 ≤ (↑(- -i) : ℝ)

Tactic:
have h' := h (-i)
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
i : ℚ
⊢ x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)

Tactic:
have h' := h (-i)
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑(- -i) : ℝ)
⊢ x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)

Tactic:
rw [neg_neg] at h'

Premises used: neg_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
⊢ x.2 ≤ (↑i : ℝ)

Tactic:
h'.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
⊢ x.2 ≤ (↑i : ℝ)

Tactic:
exact h'.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
⊢ x.2 ≤ (↑(-i) : ℝ)

Tactic:
h'.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
⊢ x.2 ≤ (↑(-i) : ℝ)

Tactic:
exact h'.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))

Tactic:
have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) := by
      ext1 x
      push _ ∈ _
      refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
      · rw [neg_neg] at h'; exact h'.2
      · exact h'.2
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) : Filter ℝ≥0∞)

Tactic:
rw [h_inter_eq] at h_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
h_neg₁ :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) : Filter ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))

Tactic:
rw [h_inter_eq] at h_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) : Filter ℝ≥0∞)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)

Tactic:
tendsto_comp_neg_atTop_iff.mp h_neg

Premises used: Iff.mp, Filter.tendsto_comp_neg_atTop_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) : Filter ℝ≥0∞)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)

Tactic:
exact tendsto_comp_neg_atTop_iff.mp h_neg

Premises used: Iff.mp, Filter.tendsto_comp_neg_atTop_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
suffices :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)

Tactic:
suffices h_neg :
      Tendsto (fun r : ℚ ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r : ℚ, s ×ˢ Iic ↑(-r)))) by
    have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) := by
      ext1 x
      push _ ∈ _
      refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
      · rw [neg_neg] at h'; exact h'.2
      · exact h'.2
    rw [h_inter_eq] at h_neg
    exact tendsto_comp_neg_atTop_iff.mp h_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_iInter_atTop (fun q ↦ (hs.prod measurableSet_Iic).nullMeasurableSet)
    ?_ ⟨0, measure_ne_top ρ _⟩

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_ne_top, MeasurableSet.prod, measurableSet_Iic, MeasureTheory.tendsto_measure_iInter_atTop, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
refine : Antitone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)

Tactic:
refine tendsto_measure_iInter_atTop (fun q ↦ (hs.prod measurableSet_Iic).nullMeasurableSet)
    ?_ ⟨0, measure_ne_top ρ _⟩

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measure_ne_top, MeasurableSet.prod, measurableSet_Iic, MeasureTheory.tendsto_measure_iInter_atTop, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Antitone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))

Tactic:
fun q r hqr ↦ Set.prod_mono subset_rfl fun x hx ↦ ?_

Premises used: Antitone, Set.prod_mono, subset_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  ∀ (q r : ℚ) (hqr : q ≤ r) (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic (↑(-r) : ℝ)) x),
    Membership.mem (γ := Set ℝ) (Iic (↑(-q) : ℝ)) x
⊢ Antitone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))

Tactic:
refine fun q r hqr ↦ Set.prod_mono subset_rfl fun x hx ↦ ?_

Premises used: Set.prod_mono, subset_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic (↑(-r) : ℝ)) x
simp : ∀ (hx : x ≤ -(↑r : ℝ)), x ≤ -(↑q : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Iic (↑(-q) : ℝ)) x

Tactic:
simp only [Rat.cast_neg, mem_Iic] at hx ⊢

Premises used: Set.mem_Iic, Rat.cast_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -(↑r : ℝ)
⊢ x ≤ -(↑q : ℝ)

Tactic:
hx.trans (neg_le_neg ?_)

Premises used: neg_le_neg, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -(↑r : ℝ)
refine : LE.le (α := ℝ) (↑q : ℝ) (↑r : ℝ)
⊢ x ≤ -(↑q : ℝ)

Tactic:
refine hx.trans (neg_le_neg ?_)

Premises used: neg_le_neg, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -(↑r : ℝ)
⊢ LE.le (α := ℝ) (↑q : ℝ) (↑r : ℝ)

Tactic:
mod_cast hqr

Premises used: cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -(↑r : ℝ)
⊢ LE.le (α := ℝ) (↑q : ℝ) (↑r : ℝ)

Tactic:
exact mod_cast hqr
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
⊢ Measurable (preCDF ρ r)

Tactic:
Measure.measurable_rnDeriv _ _

Premises used: ProbabilityTheory.preCDF, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
rw : ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α) ↦ (preCDF ρ a x).toReal
⊢ Measurable (β := (r : ℚ) → ℝ) fun (a : α) (r : ℚ) ↦ (preCDF ρ r a).toReal

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α) ↦ (preCDF ρ a x).toReal

Tactic:
fun _ ↦ measurable_preCDF.ennreal_toReal

Premises used: ProbabilityTheory.measurable_preCDF, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α) ↦ (preCDF ρ a x).toReal

Tactic:
exact fun _ ↦ measurable_preCDF.ennreal_toReal

Premises used: ProbabilityTheory.measurable_preCDF, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst : IsFiniteMeasure ρ
⊢ ρ.fst.withDensity (preCDF ρ r) = ρ.IicSnd (↑r : ℝ)

Tactic:
Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq.mp (Measure.IicSnd_ac_fst ρ r)

Premises used: ProbabilityTheory.preCDF, Rat.cast, Iff.mp, MeasureTheory.Measure.IicSnd_ac_fst, MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst

Tactic:
simp only [mul_one, forall_const]

Premises used: forall_const, mul_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst

Tactic:
have : ∀ r, ∫⁻ x in s, preCDF ρ r x ∂ρ.fst = ∫⁻ x in s, (preCDF ρ r * 1) x ∂ρ.fst := by
    simp only [mul_one, forall_const]
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
rw : ∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
rw₁ : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 1
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [this, ← setLIntegral_withDensity_eq_setLIntegral_mul _ measurable_preCDF _ hs]

Premises used: MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul, ProbabilityTheory.measurable_preCDF