awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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'])
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)

Tactic:
.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))

Premises used: MeasurableSet.biInter, Finset.countable_toSet
-- Module: Mathlib.Probability.Independence.Conditional
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'])
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)

Tactic:
exact .biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))
-- Module: Mathlib.Probability.Independence.Conditional
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)

Tactic:
Measurable.stronglyMeasurable ?_

Premises used: Measurable.stronglyMeasurable
-- Module: Mathlib.Probability.Independence.Conditional
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'])
refine_2 :
  Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
    ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (a : Ω) ↦
    ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)

Tactic:
refine Measurable.stronglyMeasurable ?_

Premises used: Measurable.stronglyMeasurable
-- Module: Mathlib.Probability.Independence.Conditional
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'])
⊢ Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
    ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)

Tactic:
Finset.measurable_fun_prod s (fun i hi ↦ measurable_condExpKernel (hπ i _ (hf i hi)))

Premises used: ProbabilityTheory.measurable_condExpKernel, Finset.measurable_fun_prod
-- Module: Mathlib.Probability.Independence.Conditional
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'])
⊢ Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
    ∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)

Tactic:
exact Finset.measurable_fun_prod s (fun i hi ↦ measurable_condExpKernel (hπ i _ (hf i hi)))

Premises used: ProbabilityTheory.measurable_condExpKernel, Finset.measurable_fun_prod
-- Module: Mathlib.Probability.Independence.Conditional
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'])
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∞)
⊢ (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)

Tactic:
filter_upwards [h_eq s f hf, h_inter_eq s f hf, h] with ω h_eq h_inter_eq h
-- Module: Mathlib.Probability.Independence.Conditional
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']) ω)
⊢ 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' ω) _)
-- Module: Mathlib.Probability.Independence.Conditional
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∞)
⊢ 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' ω) _
-- Module: Mathlib.Probability.Independence.Conditional
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)) ∞
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)))
⊢ 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:
rw [← ENNReal.ofReal_toReal h_ne_top, h_inter_eq, h, Finset.prod_apply,
      ← ENNReal.ofReal_toReal this, ENNReal.toReal_prod]

Premises used: Finset.prod_apply, ENNReal.ofReal_toReal, ENNReal.toReal_prod
-- Module: Mathlib.Probability.Independence.Conditional
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)) ∞
h₁ :
  Eq (α := ℝ) (∏ c ∈ s, μ[(f c).indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (∏ i ∈ s, ENNReal.toReal ((((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)))

Tactic:
congr 1