-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma _root_.MeasureTheory.Measure.iInf_rat_gt_prod_Iic {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ]
    {s : Set α} (hs : MeasurableSet s) (t : ℚ) :
    ⨅ r : { r' : ℚ // t < r' }, ρ (s ×ˢ Iic (r : ℝ)) = ρ (s ×ˢ Iic (t : ℝ))

Proof state:
case hs
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Monotone fun r => s ×ˢ Iic ↑↑r

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

Result:
no goals

Proof state:
case h.e_6.h.e_a.h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ), t < a → x ≤ ↑a
⊢ x ≤ ↑t

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

Result:
case h.e_6.h.e_a.h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ), t < a → x ≤ ↑a
q : ℚ
htq : ↑t < ↑q
⊢ t < q

Proof state:
case h.e_6.h.e_a.h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ), t < a → x ≤ ↑a
q : ℚ
htq : ↑t < ↑q
⊢ t < q

Tactic:
exact mod_cast htq

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ⨅ r, ρ (s ×ˢ Iic ↑↑r) = ρ (s ×ˢ Iic ↑t)

Tactic:
rw [← Monotone.measure_iInter]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ρ (⋂ i, s ×ˢ Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)

case hs
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ Monotone fun r => s ×ˢ Iic ↑↑r

case hsm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∀ (i : { r' // t < r' }), NullMeasurableSet (s ×ˢ Iic ↑↑i) ρ

case hfin
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ i, ρ (s ×ˢ Iic ↑↑i) ≠ ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
r r' : { r' // t < r' }
hrr' : r ≤ r'
⊢ Iic ↑↑r ⊆ Iic ↑↑r'

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ρ (⋂ i, s ×ˢ Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)

Tactic:
rw [← prod_iInter]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ρ (s ×ˢ ⋂ i, Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)

Proof state:
case h.e_6.h.e_a.h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ x ∈ ⋂ i, Iic ↑↑i ↔ x ∈ Iic ↑t

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

Result:
case h.e_6.h.e_a.h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ (∀ (a : ℚ), t < a → x ≤ ↑a) ↔ x ≤ ↑t

Proof state:
case h.e_6.h.e_a.h.refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : x ≤ ↑t
a : ℚ
hta : t < a
⊢ ↑t ≤ ↑a

Tactic:
exact mod_cast hta.le

Result:
no goals

Proof state:
case hsm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∀ (i : { r' // t < r' }), NullMeasurableSet (s ×ˢ Iic ↑↑i) ρ

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ρ (s ×ˢ ⋂ i, Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)

Tactic:
congr with x : 1

Result:
case h.e_6.h.e_a.h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ x ∈ ⋂ i, Iic ↑↑i ↔ x ∈ Iic ↑t

Proof state:
case h.e_6.h.e_a.h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ (∀ (a : ℚ), t < a → x ≤ ↑a) ↔ x ≤ ↑t

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

Result:
case h.e_6.h.e_a.h.refine_1
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : ∀ (a : ℚ), t < a → x ≤ ↑a
⊢ x ≤ ↑t

case h.e_6.h.e_a.h.refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
h : x ≤ ↑t
a : ℚ
hta : t < a
⊢ ↑t ≤ ↑a

Proof state:
case hfin
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ∃ i, ρ (s ×ˢ Iic ↑↑i) ≠ ⊤

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

Result:
no goals