awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (a : Ω) ↦
    ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)
have refine_2 : Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
  ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)
Tactic: refine Measurable.stronglyMeasurable ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (ω : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i))
    fun (a : Ω) ↦ ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)
have h₁ : ∀ (ω : Ω)
  (h_eq :
    ∀ i ∈ s,
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω)
  (h_inter_eq :
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
  (h :
    Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
      ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)),
  Eq (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
    (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: filter_upwards [h_eq s f hf, h_inter_eq s f hf, h] with ω h_eq h_inter_eq h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
    (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h_ne_top : Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: have h_ne_top : condExpKernel μ m' ω (⋂ i ∈ s, f i) ≠ ∞ :=
      (measure_ne_top (condExpKernel μ m' ω) _)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
h_ne_top :
  Ne (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
    (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have this : Ne (α := ℝ≥0∞) (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) ∞
Tactic: have : (∏ i ∈ s, condExpKernel μ m' ω (f i)) ≠ ∞ :=
      ENNReal.prod_ne_top fun _ _ ↦ measure_ne_top (condExpKernel μ m' ω) _
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
h_ne_top :
  Ne (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Ne (α := ℝ≥0∞) (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) ∞
⊢ Eq (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
    (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)
have h₁ : ENNReal.ofReal (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω) =
  ENNReal.ofReal
    (∏ i ∈ s, ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
Tactic: rw [← ENNReal.ofReal_toReal h_ne_top, h_inter_eq, h, Finset.prod_apply,
      ← ENNReal.ofReal_toReal this, ENNReal.toReal_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι) (s : Set Ω) (_hs : s ∈ π i), MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i) (i : ι) (_hi : i ∈ s),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']
h_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    ∀ᵐ (ω : Ω) ∂μ,
      ∀ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
          μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq_1 :
  ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i ∈ s, f i ∈ π i),
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)))
      μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h_1 :
  (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
ω : Ω
h_eq :
  ∀ i ∈ s,
    ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
      μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
h_inter_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i)) =
    μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω
h :
  Eq (α := ℝ) (μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m'] ω)
    ((∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m']) ω)
h_ne_top :
  Ne (α := ℝ≥0∞)
    ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Ne (α := ℝ≥0∞) (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) ∞
⊢ ENNReal.ofReal (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω) =
    ENNReal.ofReal
      (∏ i ∈ s,
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
have h₁ : Eq (α := ℝ) (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω)
  (∏ i ∈ s, ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have hs1_eq : ∀ s ∈ s1,
  (ae μ).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: have hs1_eq : ∀ s ∈ s1, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs1 s hs)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have hs2_eq : ∀ s ∈ s2,
  (ae μ).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: have hs2_eq : ∀ s ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs2 s hs)
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have hs12_eq : ∀ s ∈ s1,
  ∀ t ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
      μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
Tactic: have hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (s ∩ t)))
      =ᵐ[μ] μ⟦s ∩ t | m'⟧ :=
    fun s hs t ht ↦ condExpKernel_ae_eq_condExp hm' ((hs1 s hs).inter ((hs2 t ht)))
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have refine_1 : ∀
  (h :
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞))
  (s t : Set Ω) (hs : s ∈ s1) (ht : t ∈ s2),
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩