-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem tendsto_IicSnd_atBot [IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) :
    Tendsto (fun r : ℚ ↦ ρ.IicSnd r s) atBot (𝓝 0)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ∈ Iic ↑(-r)
⊢ x ∈ Iic ↑(-q)

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

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -↑r
⊢ x ≤ -↑q

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
⊢ ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r

Tactic:
ext1 x

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
⊢ x ∈ ⋂ r, s ×ˢ Iic ↑(-r) ↔ x ∈ ⋂ r, s ×ˢ Iic ↑r

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ ρ (s ×ˢ ∅) = 0

Tactic:
simp only [prod_empty, measure_empty]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))

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

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
⊢ Antitone fun r => s ×ˢ Iic ↑(-r)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => (ρ.IicSnd ↑r) s) atBot (𝓝 0)

Tactic:
simp_rw [ρ.IicSnd_apply _ hs]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)

Proof state:
case h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑i
⊢ x.2 ≤ ↑i

Tactic:
exact h'.2

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)

Tactic:
have h_empty : ρ (s ×ˢ ∅) = 0 := by simp only [prod_empty, measure_empty]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 0)

Proof state:
case h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(- -i)
⊢ x.2 ≤ ↑i

Tactic:
rw [neg_neg] at h'

Result:
case h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑i
⊢ x.2 ≤ ↑i

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
rw [h_inter_eq] at h_neg

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑r)))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑r)))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
h_fun_eq : (fun r => ρ (s ×ˢ Iic ↑r)) = fun r => ρ (s ×ˢ Iic ↑(- -r))
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑(- -r))) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
exact h_neg.comp tendsto_neg_atBot_atTop

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑r)))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Tactic:
have h_fun_eq : (fun r : ℚ ↦ ρ (s ×ˢ Iic (r : ℝ))) = fun r : ℚ ↦ ρ (s ×ˢ Iic ↑(- -r)) := by
  simp_rw [neg_neg]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑r)))
h_inter_eq : ⋂ r, s ×ˢ Iic ↑(-r) = ⋂ r, s ×ˢ Iic ↑r
h_fun_eq : (fun r => ρ (s ×ˢ Iic ↑r)) = fun r => ρ (s ×ˢ Iic ↑(- -r))
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atBot (𝓝 (ρ (⋂ i, s ×ˢ Iic ↑i)))

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
⊢ (∀ (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, ?_⟩⟩ <;> have h' := h (-i)

Result:
case h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑(-i)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(- -i)
⊢ x.2 ≤ ↑i

case h.refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(-i)
⊢ x.2 ≤ ↑(-i)

Proof state:
case h.refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
h_neg : Tendsto (fun r => ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r, s ×ˢ Iic ↑(-r))))
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ ↑i
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ ↑(-i)
⊢ x.2 ≤ ↑(-i)

Tactic:
exact h'.2

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : ρ (s ×ˢ ∅) = 0
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -↑r
⊢ ↑q ≤ ↑r

Tactic:
exact mod_cast hqr

Result:
no goals