awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h : s.Nonempty
rw :
  ∫⁻ (b : γ) in s, κ.rnDeriv η a b ∂(η : (a : α) → Measure γ) a ≤
    (((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞)
    ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have hf : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [Kernel.withDensity_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)
have rw : Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
Tactic: rw [Kernel.withDensity_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
⊢ Eq.{u_2 + 1} (α := Measure γ) ((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ)
    ((κ : (a : α) → Measure γ) a : Measure γ)
have hf : Measurable (Function.uncurry (κ.rnDeriv η))
Tactic: rw [Kernel.withDensity_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
have h_ae : κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
Tactic: have h_ae := κ.rnDeriv_eq_rnDeriv_measure (η := η) (a := a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h_ae :
  κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
have rw : Eq.{u_2 + 1} (α := Measure γ)
  (Measure.withDensity ((η : (a : α) → Measure γ) a)
    (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)))
  ((κ : (a : α) → Measure γ) a)
Tactic: rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h : Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h_ae :
  κ.rnDeriv η a =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
rw :
  Eq.{u_2 + 1} (α := Measure γ)
    (Measure.withDensity ((η : (a : α) → Measure γ) a)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)))
    ((κ : (a : α) → Measure γ) a)
⊢ Eq (α := Measure γ) (Measure.withDensity ((η : (a : α) → Measure γ) a) (κ.rnDeriv η a)) ((κ : (a : α) → Measure γ) a)
have rw₁ : Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
Tactic: rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)] f a
have h_ae : (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
  Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
Tactic: have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (hypothesis)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)] f a
have hf' : ∀ (a : α), Measurable (f a)
Tactic: have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
hf' : ∀ (a : α), Measurable (f a)
⊢ (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)] f a
have h : ∀ (x : γ)
  (hx1 :
    (κ.withDensity f).rnDeriv κ a x =
      Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x)
  (hx2 :
    Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a)
        x =
      f a x),
  (κ.withDensity f).rnDeriv κ a x = f a x
Tactic: filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 :
  (κ.withDensity f).rnDeriv κ a x =
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x
hx2 :
  Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a) x =
    f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x
have h : Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x = f a x
Tactic: rw [hx1, κ.withDensity_apply hf, hx2]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst_1 : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae :
  (κ.withDensity f).rnDeriv κ a =ᶠ[ae (F := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)]
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a)
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 :
  (κ.withDensity f).rnDeriv κ a x =
    Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x
hx2 :
  Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a) x =
    f a x
h : Measure.rnDeriv (m := mγ) ((κ.withDensity f : (a : α) → Measure γ) a) ((κ : (a : α) → Measure γ) a) x = f a x
h₁ :
  Measure.rnDeriv (m := mγ) (Measure.withDensity ((κ : (a : α) → Measure γ) a) (f a)) ((κ : (a : α) → Measure γ) a) x =
    f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x
have h₂ : f a x = f a x
Tactic: rw [hx1, κ.withDensity_apply hf, hx2]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Eq.{u_2 + 1} (α := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)
have rw : (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a)
      ((η : (a : α) → Measure γ) a) =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
    1
Tactic: rw [← Measure.rnDeriv_eq_one_iff_eq h_ac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a) =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
      1
have refine : ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ),
  κ.rnDeriv η a x = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x = 1 x
Tactic: refine eventually_congr ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ),
    κ.rnDeriv η a x = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x = 1 x
have h : ∀ (c : γ)
  (hc : κ.rnDeriv η a c = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c),
  κ.rnDeriv η a c = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
Tactic: filter_upwards [rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with c hc
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
c : γ
hc : κ.rnDeriv η a c = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c
⊢ κ.rnDeriv η a c = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
have h : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 ↔
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
Tactic: rw [hc, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
c : γ
hc : κ.rnDeriv η a c = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c
h :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
⊢ κ.rnDeriv η a c = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
have h₁ : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 ↔
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1
Tactic: rw [hc, Pi.one_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
⊢ Measurable (uncurry f)
have refine : ∀ (a : (↑I : Type)), MeasurableSet (uncurry f ⁻¹' Ioi a)
Tactic: refine measurable_of_Ioi fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
a : (↑I : Type)
⊢ MeasurableSet (uncurry f ⁻¹' Ioi a)
have simp : MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}
Tactic: simp only [preimage, uncurry, mem_Ioi]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
a : (↑I : Type)
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}
have h_monotone : ∀ (s : X),
  Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
      (Icc 0 x)
Tactic: have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) :=
      fun x y hxy ↦ measureReal_mono (by gcongr)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
⊢ Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
have h : ∀ (e : X × (↑I : Type)),
  Membership.mem (γ := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2} e ↔
    Membership.mem (γ := Set (X × (↑I : Type)))
      (⋃ (q : ℚ),
        ⋃ (hqI : (↑q : ℝ) ∈ I),
          ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
            {e : X × (↑I : Type) |
              Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                  ((κ : (a : X) → Measure (↑I : Type)) e.1)
                  (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
                (↑e.2 : ℝ)})
      e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
⊢ Membership.mem (γ := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2} e ↔
    Membership.mem (γ := Set (X × (↑I : Type)))
      (⋃ (q : ℚ),
        ⋃ (hqI : (↑q : ℝ) ∈ I),
          ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
            {e : X × (↑I : Type) |
              Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                  ((κ : (a : X) → Measure (↑I : Type)) e.1)
                  (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
                (↑e.2 : ℝ)})
      e
have h : (∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry) ↔
  ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) sorry)) <
          (↑e.2 : ℝ)
Tactic: simp_all only [lt_sSup_iff, mem_setOf_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
⊢ (∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯)) <
          (↑e.2 : ℝ) ∧
        a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯) ↔
    ∃ (i : ℚ),
      (↑a : ℝ) < (↑i : ℝ) ∧
        ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
            (↑e.2 : ℝ)
have h : (∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry) →
  ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) sorry)) <
          (↑e.2 : ℝ)
Tactic: constructor