-- Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
lemma isRatCondKernelCDFAux_density_Iic (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsRatCondKernelCDFAux (fun (p : α × γ) q ↦ density κ (fst κ) p.1 p.2 (Iic q)) κ (fst κ) where
  measurable := measurable_pi_iff.mpr fun _ ↦ measurable_density κ (fst κ) measurableSet_Iic
  mono' a q r hqr :=
    ae_of_all _ fun c ↦ density_mono_set le_rfl a c (Iic_subset_Iic.mpr (by exact_mod_cast hqr))
  nonneg' _ _ := ae_of_all _ fun _ ↦ density_nonneg le_rfl _ _ _
  le_one' _ _ := ae_of_all _ fun _ ↦ density_le_one le_rfl _ _ _
  tendsto_integral_of_antitone a s hs_anti hs_tendsto

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
i j : ℕ
hij : i ≤ j
⊢ ↑(s i) ≤ ↑(s j)

Tactic:
exact mod_cast hs_mono hij

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop
    (𝓝 ((κ a) {p | p.1 ∈ univ}).toReal)

Tactic:
let s' : ℕ → Set ℝ := fun n ↦ Iic (s n)

Result:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
⊢ Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop
    (𝓝 ((κ a) {p | p.1 ∈ univ}).toReal)

Proof state:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
⊢ x ∈ ⋃ i, s' i ↔ x ∈ univ

Tactic:
simp only [mem_iUnion, mem_Iic, mem_univ, iff_true]

Result:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i

Proof state:
case refine_1
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
i j : ℕ
hij : i ≤ j
⊢ ↑(s j) ≤ ↑(s i)

Tactic:
exact mod_cast hs_anti hij

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 0)

Tactic:
let s' : ℕ → Set ℝ := fun n ↦ Iic (s n)

Result:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
⊢ Tendsto (fun m => ∫ (c : γ), κ.density κ.fst (a, c).1 (a, c).2 (Iic ↑(s m)) ∂κ.fst a) atTop (𝓝 0)

Proof state:
case refine_1
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
⊢ Antitone s'

Tactic:
refine fun i j hij ↦ Iic_subset_Iic.mpr ?_

Result:
case refine_1
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
i j : ℕ
hij : i ≤ j
⊢ ↑(s j) ≤ ↑(s i)

Proof state:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
have ⟨q, hq⟩ := exists_rat_lt x

Result:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
⊢ ∃ x_1, ↑(s x_1) < x

Proof state:
case refine_1
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
⊢ Monotone s'

Tactic:
exact fun i j hij ↦ Iic_subset_Iic.mpr (by exact mod_cast hs_mono hij)

Result:
no goals

Proof state:
case refine_2.h.intro
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ∃ x_1, ↑(s x_1) < x

Tactic:
refine ⟨i, lt_of_le_of_lt ?_ hq⟩

Result:
case refine_2.h.intro
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ↑(s i) ≤ ↑q

Proof state:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
⊢ ∃ i, x ∈ s' i

Tactic:
have ⟨q, hq⟩ := exists_rat_gt x

Result:
case refine_2.h
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ s a
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : x < ↑q
⊢ ∃ i, x ∈ s' i

Proof state:
case refine_2.h.intro
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ i, ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun n => Iic ↑(s n)
x : ℝ
q : ℚ
hq : ↑q < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ↑(s i) ≤ ↑q

Tactic:
exact mod_cast hi i le_rfl

Result:
no goals