awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : ι → Ω → E
inst_4 : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (β := fun (x : ↥s) ↦ E) (s.restrict (π := fun (i : ι) ↦ Ω → E) X) P
x : Ω
⊢ Eq.{u_3 + 1} (α := E) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : InnerProductSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
h :
  ∀ (x : E),
    charFun (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)) x =
      (∏ i : ι, charFun (μ i)) x
⊢ Eq.{u_3 + 1} (α := (t : E) → ℂ)
    (charFun (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)))
    (∏ i : ι, charFun (μ i))

Tactic:
ext
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
ι : Type u_2
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : Fintype ι
inst_5 : InnerProductSpace ℝ E
μ : ι → Measure E
inst_6 : ∀ (i : ι), IsProbabilityMeasure (μ i)
x : E
⊢ charFun (mE := inst) (Measure.map (fun (p : (i : ι) → E) ↦ ∑ i : ι, p i) (Measure.pi (α := fun (i : ι) ↦ E) μ)) x =
    (∏ i : ι, charFun (μ i)) x

Tactic:
simp [charFun_eq_charFunDual_toDualMap, charFunDual_map_sum_pi_eq_prod]

Premises used: ProbabilityTheory.charFunDual_map_sum_pi_eq_prod, MeasureTheory.charFun_eq_charFunDual_toDualMap
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_6 : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (α := (i : ι) → E i) (β := WithLp 2 ((i : ι) → E i)) (_m := MeasurableSpace.pi (X := E)) (toLp 2)
    (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_6 : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (β := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_6 : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
rw :
  Eq (α := Measure ((i : ι) → E i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
      (Measure.pi (α := E) fun (i : ι) ↦ Measure.map (X i) P) ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
rw₁ :
  (∀ (t : WithLp 2 ((i : ι) → E i)),
      charFun (mE := measurableSpace 2 ((i : ι) → E i))
          (Measure.map (toLp 2) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)) ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
rw₂ :
  (∀ (t : WithLp 2 ((i : ι) → E i)),
      charFun (mE := measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2 ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)) ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
rw₃ rw₄ :
  (∀ (t : WithLp 2 ((i : ι) → E i)),
      charFun (mE := measurableSpace 2 ((i : ι) → E i)) (Measure.map (fun (x : Ω) ↦ toLp 2 fun (i : ι) ↦ X i x) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)) ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)
⊢ iIndepFun (β := E) X P ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (mE := measurableSpace 2 ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp 2 fun (x : ι) ↦ X x ω) P) t =
        ∏ i : ι, charFun (mE := mE i) (Measure.map (X i) P) (t.ofLp i)

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFun_eq_pi_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]

Premises used: Function.comp_def, AEMeasurable.map_map_of_aemeasurable, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map, MeasureTheory.charFun_eq_pi_iff
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst : Fintype ι
inst_1 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_6 : (i : ι) → NormedSpace ℝ (E i)
inst_7 : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
rw :
  Eq (α := Measure ((i : ι) → E i)) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
      (Measure.pi (α := E) fun (i : ι) ↦ Measure.map (X i) P) ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
rw₁ rw₂ :
  (∀ (L : StrongDual ℝ ((i : ι) → E i)),
      charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))) ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
⊢ iIndepFun (β := E) X P ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (mE := MeasurableSpace.pi (X := E)) (Measure.map (fun (ω : Ω) (x : ι) ↦ X x ω) P) L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]

Premises used: MeasureTheory.charFunDual_eq_pi_iff, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_2
inst_1 : Fintype ι
inst_2 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_7 : (i : ι) → NormedSpace ℝ (E i)
inst_8 : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (α := (i : ι) → E i) (_m := MeasurableSpace.pi (X := E)) (toLp p)
    (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.CharacteristicFunction
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_2
inst_1 : Fintype ι
inst_2 : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : ∀ (i : ι), CompleteSpace.{u_3} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_3} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_3} (E i)
X : (i : ι) → Ω → E i
inst_7 : (i : ι) → NormedSpace ℝ (E i)
inst_8 : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (β := (i : ι) → E i) (fun (ω : Ω) (i : ι) ↦ X i ω) P

Tactic:
fun_prop
-- 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 μ
⊢ ∀ (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']

Tactic:
have h_eq' : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i) i (_hi : i ∈ s),
      (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (f i))) =ᵐ[μ] μ⟦f i | m'⟧ :=
    fun s f H i hi ↦ condExpKernel_ae_eq_condExp hm' (hπ i (f i) (H 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']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
rw :
  ∀ (i : ι) (hi : i ∈ (↑s : Set ι)),
    ∀ᵐ (x : Ω) ∂μ,
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] x
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ i ∈ (↑s : Set ι),
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω

Tactic:
rw [ae_ball_iff (Finset.countable_toSet s)]

Premises used: MeasureTheory.ae_ball_iff, 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']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ ∀ (i : ι) (hi : i ∈ (↑s : Set ι)),
    ∀ᵐ (x : Ω) ∂μ,
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] x

Tactic:
h_eq' s f H

Premises used: Filter.EventuallyEq
-- 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']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ ∀ (i : ι) (hi : i ∈ (↑s : Set ι)),
    ∀ᵐ (x : Ω) ∂μ,
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] x

Tactic:
exact h_eq' s f 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']
⊢ ∀ (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'] ω

Tactic:
have h_eq : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i), ∀ᵐ ω ∂μ,
      ∀ i ∈ s, ENNReal.toReal (condExpKernel μ m' ω (f i)) = (μ⟦f i | m'⟧) ω := by
    intro s f H
    simp_rw [← Finset.mem_coe]
    rw [ae_ball_iff (Finset.countable_toSet s)]
    exact h_eq' s f 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 :
  ∀ (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'] ω
⊢ ∀ (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']

Tactic:
fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_

Premises used: MeasureTheory.Measure.real, ProbabilityTheory.condExpKernel_ae_eq_condExp
-- 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'] ω
refine : ∀ (s : Finset ι) (f : ι → Set Ω) (H : ∀ i ∈ s, f i ∈ π i), MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)
⊢ ∀ (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']

Tactic:
refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_

Premises used: ProbabilityTheory.condExpKernel_ae_eq_condExp
-- 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'] ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)

Tactic:
MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H 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'] ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)

Tactic:
exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H 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'] ω
⊢ ∀ (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']

Tactic:
have h_inter_eq : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i),
      (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (⋂ i ∈ s, f i)))
        =ᵐ[μ] μ⟦⋂ i ∈ s, f i | m'⟧ := by
    refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_
    exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H 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 Ω} (_H : ∀ i ∈ s, f i ∈ π i),
      ∀ᵐ (a : Ω) ∂μ.trim hm',
        Eq (α := ℝ≥0∞)
          ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ s, f i) : ℝ≥0∞)
          (∏ i ∈ s, (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i) : ℝ≥0∞)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, f i ∈ π i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
⟨fun h s f hf ↦ ?_, fun h s f hf ↦ ?_⟩

Premises used: Iff.intro