awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ] μ[s.indicator fun (ω : Ω) ↦ 1 | m]
have rw : (ae μ).EventuallyEq (β := ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m] μ[s.indicator fun (ω : Ω) ↦ 1 | m]
Tactic: rw [inf_of_le_left hm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (ae (μ.trim hm)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m]
have rw : (ae μ).EventuallyEq (β := ℝ)
  (fun (x : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
  μ[s.indicator fun (ω : Ω) ↦ 1 | m]
Tactic: rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm
    stronglyMeasurable_condExp]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (a : Ω) ↦
    ((((Kernel.map (condExpKernel μ (MeasurableSpace.comap Y mγ)) X : Kernel Ω β) : (a : Ω) → Measure β) a :
          Measure β) :
        (a : Set β) → ℝ≥0∞)
      s
have simp_rw : (ae μ).EventuallyEq (β := ℝ≥0∞)
  (fun (a : Ω) ↦ ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
  fun (a : Ω) ↦
  (((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (X ⁻¹' s)
Tactic: simp_rw [Kernel.map_apply' _ hX _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (a : Ω) ↦
    (((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (X ⁻¹' s)
have h : ∀ (a : Ω)
  (ha₁ :
    Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
      μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
  (ha₂ :
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
      μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a),
  Eq (α := ℝ≥0∞)
    (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (X ⁻¹' s) :
      ℝ≥0∞)
Tactic: filter_upwards [condDistrib_ae_eq_condExp hY hX (μ := μ) hs,
    condExpKernel_ae_eq_condExp hY.comap_le (μ := μ) (hX hs)] with a ha₁ ha₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
a : Ω
ha₁ :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
ha₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
⊢ Eq (α := ℝ≥0∞)
    (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (X ⁻¹' s) :
      ℝ≥0∞)
have h : Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
Tactic: rw [← measureReal_eq_measureReal_iff, ha₁, ha₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
a : Ω
ha₁ :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
ha₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
h :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (X ⁻¹' s) :
      ℝ≥0∞)
have h₁ : μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a =
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
Tactic: rw [← measureReal_eq_measureReal_iff, ha₁, ha₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
a : Ω
ha₁ :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
ha₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
h :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
h₁ :
  μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a =
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (X ⁻¹' s) :
      ℝ≥0∞)
have h₂ : Eq (α := ℝ) (μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
  (μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
Tactic: rw [← measureReal_eq_measureReal_iff, ha₁, ha₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have inl : ∀ (h : IsEmpty Ω),
  μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
inl :
  ∀ (h : IsEmpty Ω),
    μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have inr : ∀ (h : Nonempty Ω),
  μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
h : IsEmpty Ω
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have this : μ = 0
Tactic: have : μ = 0 := Measure.eq_zero_of_isEmpty μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
h : Nonempty Ω
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have hX : Measurable.{u_1, u_1} (α := Ω) id
Tactic: have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
h : Nonempty Ω
hX : Measurable.{u_1, u_1} (α := Ω) id
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have inr : μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
  @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y
Tactic: simp_rw [condExpKernel_apply_eq_condDistrib]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hf_int : Integrable f μ
h : Nonempty Ω
hX : Measurable.{u_1, u_1} (α := Ω) id
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y
have h₁ : μ[f | MeasurableSpace.comap id (m ⊓ mΩ)] =ᶠ[ae μ] fun (a : Ω) ↦
  @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f y
Tactic: have h := condExp_ae_eq_integral_condDistrib_id hX hf_int
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] μ[f | m]
have rw : μ[f | m] =ᶠ[ae μ] μ[f | m]
Tactic: rw [inf_of_le_left hm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf : StronglyMeasurable f
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine_1 : StronglyMeasurable μ[f | m]
Tactic: refine StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf : StronglyMeasurable f
hf_int : Integrable f μ
refine_1 : StronglyMeasurable μ[f | m]
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine_2 : StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
  @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: refine StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf : StronglyMeasurable f
hf_int : Integrable f μ
refine_1 : StronglyMeasurable μ[f | m]
refine_2 :
  StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine_3 : μ[f | m] =ᶠ[ae μ] fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: refine StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine : μ[AEStronglyMeasurable.mk f sorry | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
  @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: refine (condExp_congr_ae_trim hm hf_int.1.ae_eq_mk).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine_1 : Integrable (AEStronglyMeasurable.mk f sorry) μ
Tactic: refine (condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm
    hf_int.1.stronglyMeasurable_mk ?_).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
refine_1 : Integrable (AEStronglyMeasurable.mk f ⋯) μ
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have refine_2 : EventuallyEq.{u_1, u_2} (β := F) (ae (μ.trim hm))
  (fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f sorry y)
  fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
Tactic: refine (condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm
    hf_int.1.stronglyMeasurable_mk ?_).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ EventuallyEq.{u_1, u_2} (β := F) (ae (μ.trim hm))
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have h : ∀ (ω : Ω)
  (hω :
    f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f sorry),
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f sorry y)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y)
Tactic: filter_upwards [aestronglyMeasurable_trim_condExpKernel hm hf_int.1] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
ω : Ω
hω : f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y)
have h : Eq.{u_2 + 1} (α := F)
  (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f sorry y)
  (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (a : Ω) ↦ AEStronglyMeasurable.mk f sorry a)
Tactic: rw [integral_congr_ae hω]
-- 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 μ
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have pos : ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
Tactic: by_cases hμs : μ s = 0
-- 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 μ
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have neg : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
Tactic: by_cases hμs : μ s = 0
-- 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∞)
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have pos : μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
Tactic: rw [Measure.restrict_eq_zero.2 hμs]
-- 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∞)
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have neg : (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
Tactic: refine ae_eq_trans (condExp_restrict_ae_eq_restrict
    (generateFrom_singleton_le hs)
    (measurableSet_generateFrom rfl) hf).symm ?_
-- 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∞)
⊢ (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have neg : ∀ (s_1 : Set Ω),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn.{u_1, u_2} (ε := F) (fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm
-- 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∞)
neg :
  ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := F) (fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)
⊢ (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
have neg₁ : ∀ (s_1 : Set Ω),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in s_1, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s)
        (∫ (x : Ω) in s_1, f x ∂μ.restrict s)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm