awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ 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))
have 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))
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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))
⊢ 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))
have 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))
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
⊢ iIndepFun (β := E) X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
have 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 ℝ (WithLp p ((x : ι) → E x))),
    charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P) L =
      ∏ i : ι,
        charFunDual (mE := mE i) (Measure.map (X i) P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
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
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 ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
⊢ iIndepFun (β := E) X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P)
          L =
        ∏ i : ι,
          charFunDual (mE := mE i) (Measure.map (X i) P)
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
                (ContinuousLinearMap.single ℝ E i)))
have rw₁ : (∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := measurableSpace p ((i : ι) → E i))
        (Measure.map (toLp p) (Measure.map (fun (ω : Ω) (i : ι) ↦ X i ω) P)) L =
      ∏ i : ι,
        charFunDual (mE := mE i) (Measure.map (X i) P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))) ↔
  ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
    charFunDual (mE := measurableSpace p ((x : ι) → E x)) (Measure.map (fun (ω : Ω) ↦ toLp p fun (x : ι) ↦ X x ω) P) L =
      ∏ i : ι,
        charFunDual (mE := mE i) (Measure.map (X i) P)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
-- 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 μ
⊢ (∀ (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'])
have 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']
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))
-- 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']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ ∀ᵐ (ω : Ω) ∂μ,
    ∀ i ∈ (↑s : Set ι),
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f i)) =
        μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'] ω
have 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
Tactic: rw [ae_ball_iff (Finset.countable_toSet s)]
-- 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']
⊢ (∀ (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'])
have 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'] ω
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
-- 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'] ω
⊢ ∀ (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']
have refine : ∀ (s : Finset ι) (f : ι → Set Ω) (H : ∀ i ∈ s, f i ∈ π i), MeasurableSet.{u_1} (α := Ω) (⋂ i ∈ s, f i)
Tactic: refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_
-- 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 :
  ∀ (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),
      ∀ᵐ (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'])
have 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']
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))