awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint f a → IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a)

Tactic:
exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
simp_rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (i_1 : ℚ), ⋂ (_ : i ≤ i_1), {x : α | f x i ≤ f x i_1})
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (q r : ℚ), q ≤ r → f a q ≤ f a r}

Tactic:
simp_rw [Set.setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (i_1 : ℚ), ⋂ (_ : i ≤ i_1), {x : α | f x i ≤ f x i_1})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
refine : ∀ (q : ℚ), MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (_ : q ≤ i), {x : α | f x q ≤ f x i})
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (i_1 : ℚ), ⋂ (_ : i ≤ i_1), {x : α | f x i ≤ f x i_1})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q : ℚ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (_ : q ≤ i), {x : α | f x q ≤ f x i})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q : ℚ
refine : ∀ (r : ℚ), MeasurableSet.{u_1} (α := α) (⋂ (_ : q ≤ r), {x : α | f x q ≤ f x r})
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (_ : q ≤ i), {x : α | f x q ≤ f x i})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q r : ℚ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : q ≤ r), {x : α | f x q ≤ f x r})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q r : ℚ
refine : q ≤ r → MeasurableSet.{u_1} (α := α) {x : α | f x q ≤ f x r}
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : q ≤ r), {x : α | f x q ≤ f x r})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q r : ℚ
h : q ≤ r
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x q ≤ f x r}

Tactic:
measurableSet_le hf.eval hf.eval

Premises used: measurableSet_le, setOf, Measurable.eval
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q r : ℚ
h : q ≤ r
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x q ≤ f x r}

Tactic:
exact measurableSet_le hf.eval hf.eval

Premises used: measurableSet_le, Measurable.eval
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | Monotone (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
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}

Tactic:
have h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}

Tactic:
have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), {x : α | ⨅ (r : (↑(Ioi i) : Type)), f x (↑r : ℚ) = f x i})
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}

Tactic:
rw [Set.setOf_forall]

Premises used: Set.setOf_forall
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), {x : α | ⨅ (r : (↑(Ioi i) : Type)), f x (↑r : ℚ) = f x i})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
refine : ∀ (q : ℚ), MeasurableSet.{u_1} (α := α) {x : α | ⨅ (r : (↑(Ioi q) : Type)), f x (↑r : ℚ) = f x q}
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), {x : α | ⨅ (r : (↑(Ioi i) : Type)), f x (↑r : ℚ) = f x i})

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

Premises used: MeasurableSet.iInter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
q : ℚ
⊢ MeasurableSet.{u_1} (α := α) {x : α | ⨅ (r : (↑(Ioi q) : Type)), f x (↑r : ℚ) = f x q}

Tactic:
measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval

Premises used: measurableSet_eq_fun, Measurable.eval, Measurable.iInf
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
q : ℚ
⊢ MeasurableSet.{u_1} (α := α) {x : α | ⨅ (r : (↑(Ioi q) : Type)), f x (↑r : ℚ) = f x q}

Tactic:
exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval

Premises used: measurableSet_eq_fun, Measurable.eval, Measurable.iInf
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}

Tactic:
have h4 : MeasurableSet {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t} := by
    rw [Set.setOf_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
rw :
  MeasurableSet.{u_1} (α := α)
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})

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

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
⊢ MeasurableSet.{u_1} (α := α)
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})

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

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
suffices :
  Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}

Tactic:
suffices {a | IsRatStieltjesPoint f a}
      = ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)}
        ∩ {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t}) by
    rw [this]
    exact (((h1.inter h2).inter h3).inter h4)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
h :
  ∀ (a : α),
    Membership.mem (γ := Set α) {a : α | IsRatStieltjesPoint f a} a ↔
      Membership.mem (γ := Set α)
        ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
          {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
        a
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})

Tactic:
ext a
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
⊢ IsRatStieltjesPoint f a ↔
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
h :
  ∀ (h : IsRatStieltjesPoint f a),
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
h₁ :
  ∀
    (h :
      ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
        ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t),
    IsRatStieltjesPoint f a
⊢ IsRatStieltjesPoint f a ↔
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), 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 : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

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

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one, And.intro, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), 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 : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

Tactic:
exact ⟨⟨⟨h.mono, h.tendsto_atTop_one⟩, h.tendsto_atBot_zero⟩, h.iInf_rat_gt_eq⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
h :
  ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
    ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
⊢ IsRatStieltjesPoint f a

Tactic:
⟨h.1.1.1, h.1.1.2, h.1.2, h.2⟩

Premises used: And.right, And.left, ProbabilityTheory.IsRatStieltjesPoint.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
h :
  ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
    ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
⊢ IsRatStieltjesPoint f a

Tactic:
exact ⟨h.1.1.1, h.1.1.2, h.1.2, h.2⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Monotone (f a)
neg : ∀ (h : ¬p a), Monotone (g a)
⊢ Monotone (if p a then f a else g a)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

Tactic:
(hf h).mono

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Monotone (g a)

Tactic:
(hg h).mono

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

Tactic:
exacts [(hf h).mono, (hg h).mono]

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Tendsto (f a) atTop (𝓝 1)
neg : ∀ (h : ¬p a), Tendsto (g a) atTop (𝓝 1)
⊢ Tendsto (if p a then f a else g a) atTop (𝓝 1)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

Tactic:
(hf h).tendsto_atTop_one

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)

Tactic:
(hg h).tendsto_atTop_one

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

Tactic:
exacts [(hf h).tendsto_atTop_one, (hg h).tendsto_atTop_one]

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Tendsto (f a) atBot (𝓝 0)
neg : ∀ (h : ¬p a), Tendsto (g a) atBot (𝓝 0)
⊢ Tendsto (if p a then f a else g a) atBot (𝓝 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

Tactic:
(hf h).tendsto_atBot_zero

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)

Tactic:
(hg h).tendsto_atBot_zero

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

Tactic:
exacts [(hf h).tendsto_atBot_zero, (hg h).tendsto_atBot_zero]

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a) (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
neg : ∀ (h : ¬p a) (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), g a (↑r : ℚ) = g a t
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), (if p a then f a else g a) (↑r : ℚ) = (if p a then f a else g a) t

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

Tactic:
(hf h).iInf_rat_gt_eq

Premises used: ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), g a (↑r : ℚ) = g a t

Tactic:
(hg h).iInf_rat_gt_eq

Premises used: ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq