awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]) t (μ.restrict s)
have neg : enorm.{u_2} (E := F) (∫ (x : Ω), f x ∂μ[|s]) = 0 ∨
  LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [integrableOn_const_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg : ∀ (h : t = ∅),
  Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
Tactic: obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
neg :
  ∀ (h : t = ∅),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg₁ : ∀ (h : t = s),
  Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
Tactic: obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
neg :
  ∀ (h : t = ∅),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₁ :
  ∀ (h : t = s),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg₂ : ∀ (h : t = sᶜ),
  Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
Tactic: obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
neg :
  ∀ (h : t = ∅),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₁ :
  ∀ (h : t = s),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₂ :
  ∀ (h : t = sᶜ),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg₃ : ∀ (h : t = univ),
  Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
Tactic: obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg : μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ.restrict s
Tactic: simp only [h, cond, integral_smul_measure, ENNReal.toReal_inv, integral_const,
        MeasurableSet.univ, measureReal_restrict_apply, univ_inter, measureReal_restrict_apply_self,
        ← measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ.restrict s
have neg : μ.real s ≠ 0
Tactic: rw [smul_inv_smul₀, Measure.restrict_restrict hs, inter_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
have neg : μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
Tactic: simp only [h, Measure.restrict_univ, cond, integral_smul_measure, ENNReal.toReal_inv, ←
        measureReal_def, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have neg : μ.real s ≠ 0
Tactic: rw [smul_inv_smul₀]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
    fun (x : Ω) ↦ μ[|s].real t
have rw : (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
  fun (x : Ω) ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]
Tactic: rw [← integral_indicator_one ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s,
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
have this : (ae (μ.restrict s)).EventuallyEq (β := ℝ)
  (fun (ω : Ω) ↦
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
  μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
Tactic: have : (fun ω ↦ (condExpKernel μ (generateFrom {s}) ω).real t) =ᵐ[μ.restrict s]
      μ⟦t | generateFrom {s}⟧ :=
    ae_restrict_le <| condExpKernel_ae_eq_condExp
      (generateFrom_singleton_le hs) ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
⊢ ∀ᵐ (ω : Ω) ∂μ.restrict s,
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
have h : ∀ (ω : Ω) (hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t)
  (hω₂ :
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
      μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
Tactic: filter_upwards [condExp_set_generateFrom_singleton hs ht, this] with ω hω₁ hω₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
have h : ∀
  (hω₂ :
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
      μ[|s].real t),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
Tactic: rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂
Cleared hypotheses: hω₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω
h :
  ∀
    (hω₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
have h₁ : ∀
  (hω₂ :
    ENNReal.toReal
        ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          t) =
      μ[|s].real t),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
Tactic: rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂
Cleared hypotheses: hω₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω
h :
  ∀
    (hω₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₁ :
  ∀
    (hω₂ :
      ENNReal.toReal
          ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t) =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
have h₂ : ∀
  (hω₂ :
    ENNReal.toReal
        ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          t) =
      ENNReal.toReal μ[t | s]),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
Tactic: rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂
Cleared hypotheses: hω₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}] ω
h :
  ∀
    (hω₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₁ :
  ∀
    (hω₂ :
      ENNReal.toReal
          ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t) =
        μ[|s].real t),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
h₂ :
  ∀
    (hω₂ :
      ENNReal.toReal
          ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) :
              (a : Set Ω) → ℝ≥0∞)
            t) =
        ENNReal.toReal μ[t | s]),
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
have h₃ : ∀
  (hω₂ :
    Eq (α := ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          t :
        ℝ≥0∞)
      (μ[t | s] : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    (μ[t | s] : ℝ≥0∞)
Tactic: rwa [hω₁, measureReal_def, measureReal_def,
    ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)] at hω₂
Cleared hypotheses: hω₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
f g : Kernel α β
h : f.toFun = g.toFun
⊢ f = g
have mk : ∀ (toFun : α → Measure β) (measurable' : Measurable toFun)
  (h : { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun = g.toFun),
  { toFun := toFun, measurable' := measurable' : Kernel α β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : Kernel α β
toFun : α → Measure β
measurable' : Measurable toFun
h : { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun = g.toFun
⊢ { toFun := toFun, measurable' := measurable' : Kernel α β } = g
have mk : ∀ (toFun_1 : α → Measure β) (measurable'_1 : Measurable toFun_1)
  (h :
    { toFun := toFun, measurable' := measurable' : Kernel α β }.toFun =
      { toFun := toFun_1, measurable' := measurable'_1 : Kernel α β }.toFun),
  { toFun := toFun, measurable' := measurable' : Kernel α β } = { toFun := toFun_1, measurable' := measurable'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
⊢ Eq.{u_2 + 1} (α := Measure β) (((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β)
    (∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β)
have rw : Eq.{u_2 + 1} (α := Measure β) ((∑ i ∈ I, (⇑(κ i) : (a : α) → Measure β)) a) (∑ i ∈ I, (κ i : (a : α) → Measure β) a)
Tactic: rw [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
rw :
  Eq.{u_2 + 1} (α := Measure β) ((∑ i ∈ I, (⇑(κ i) : (a : α) → Measure β)) a) (∑ i ∈ I, (κ i : (a : α) → Measure β) a)
⊢ Eq.{u_2 + 1} (α := Measure β) (((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β)
    (∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β)
have rw₁ : Eq.{u_2 + 1} (α := Measure β) (∑ c ∈ I, (κ c : (a : α) → Measure β) a) (∑ i ∈ I, (κ i : (a : α) → Measure β) a)
Tactic: rw [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
⊢ Eq (α := ℝ≥0∞) (((((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
  (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [finsetSum_apply, Measure.finsetSum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
rw :
  Eq (α := ℝ≥0∞) (((∑ i ∈ I, (κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((((∑ i ∈ I, κ i : Kernel α β) : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
  (∑ i ∈ I, (((κ i : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s)
Tactic: rw [finsetSum_apply, Measure.finsetSum_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
⊢ κ.bound < ∞
have obtain : ∀ (C : ℝ≥0∞) (hC : C < ∞)
  (hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C), κ.bound < ∞
Tactic: obtain ⟨C, hC, hle⟩ := h.exists_univ_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsFiniteKernel κ
C : ℝ≥0∞
hC : C < ∞
hle : ∀ (a : α), (((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ C
⊢ κ.bound < ∞
have refine : κ.bound ≤ C
Tactic: refine lt_of_le_of_lt ?_ hC
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
⊢ IsFiniteKernel (κ + η)
have refine : ∀ (a : α), (((κ + η : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ ≤ κ.bound + η.bound
Tactic: refine ⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst : IsZeroOrMarkovKernel κ
a : α
⊢ IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) ((κ : (a : α) → Measure β) a)
have inl : ∀ [IsZeroOrMarkovKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0],
  IsZeroOrProbabilityMeasure.{u_2} (α := β) (m0 := mβ) (((0 : Kernel α β) : (a : α) → Measure β) a)
Tactic: rcases eq_zero_or_isMarkovKernel κ with rfl | h'
Cleared hypotheses: κ, inst