-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma measurableSet_isRatStieltjesPoint [MeasurableSpace α] (hf : Measurable f) :
    MeasurableSet {a | IsRatStieltjesPoint f a}

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}

Tactic:
ext a

Result:
case h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
a : α
⊢ a ∈ {a | IsRatStieltjesPoint f a} ↔
    a ∈
      {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
        {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} :=
  measurableSet_tendsto _ (fun q ↦ hf.eval)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Proof state:
case h.refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
a : α
h : IsRatStieltjesPoint f a
⊢ ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

Tactic:
exact ⟨⟨⟨h.mono, h.tendsto_atTop_one⟩, h.tendsto_atBot_zero⟩, h.iInf_rat_gt_eq⟩

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
this :
  {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
rw [this]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
this :
  {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet
    ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t})

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
have h1 : MeasurableSet {a | Monotone (f a)} := by
  change MeasurableSet {a | ∀ q r (_ : q ≤ r), f a q ≤ f a r}
  simp_rw [Set.setOf_forall]
  refine MeasurableSet.iInter (fun q ↦ ?_)
  refine MeasurableSet.iInter (fun r ↦ ?_)
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  exact measurableSet_le hf.eval hf.eval

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}

Tactic:
rw [Set.setOf_forall]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet (⋂ i, {x | ⨅ r, f x ↑r = f x i})

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
q r : ℚ
⊢ MeasurableSet (⋂ (_ : q ≤ r), {x | f x q ≤ f x r})

Tactic:
refine MeasurableSet.iInter (fun _ ↦ ?_)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
q r : ℚ
x✝ : q ≤ r
⊢ MeasurableSet {x | f x q ≤ f x r}

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
q : ℚ
⊢ MeasurableSet (⋂ i, ⋂ (_ : q ≤ i), {x | f x q ≤ f x i})

Tactic:
refine MeasurableSet.iInter (fun r ↦ ?_)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
q r : ℚ
⊢ MeasurableSet (⋂ (_ : q ≤ r), {x | f x q ≤ f x r})

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
q r : ℚ
x✝ : q ≤ r
⊢ MeasurableSet {x | f x q ≤ f x r}

Tactic:
exact measurableSet_le hf.eval hf.eval

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
this :
  {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet
    ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t})

Tactic:
exact (((h1.inter h2).inter h3).inter h4)

Result:
no goals