awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ ∫ (x : Ω),
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            x +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          x ∂P =
    HMul.hMul (α := ℝ)
      (∫ (x : Ω),
        HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) x)
          (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) x) ∂P)
      (∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P)
have rw : HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∫ (a : Ω), ∏ x : S, (g x : (a : E x) → ℝ) (X x a) ∂P : ℝ) -
    HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
  (HSMul.hSMul (β := ℝ) ((P.restrict A).real Set.univ) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
      HSMul.hSMul (β := ℝ) ((P.restrict Aᶜ).real Set.univ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
    ∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P
Tactic: rw [integral_sub, integral_add, integral_indicator₀ mA, integral_indicator₀ mA,
    integral_const_mul, integral_const_mul, integral_const_mul, integral_add,
    integral_indicator₀ mA, integral_indicator₀ mA.compl, integral_const, integral_const, h]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : Fintype S
inst_5 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ),
    ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
      P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) (A.indicator 1 ω) : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) =
      A.indicator
            (fun (ω : Ω) ↦
              HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
            ω +
          HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ) -
        A.indicator
          (fun (ω : Ω) ↦
            HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∏ s : S, (g s : (a : E s) → ℝ) (X s ω) : ℝ))
          ω
h2 :
  ∀ (ω : Ω),
    (f : (a : ℝ) → ℝ) (A.indicator 1 ω) =
      HAdd.hAdd (α := ℝ) (A.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 1) ω)
        (Aᶜ.indicator (fun (x : Ω) ↦ (f : (a : ℝ) → ℝ) 0) ω)
hg : ∀ {c : ℝ}, Integrable (ε := ℝ) (fun (ω : Ω) ↦ c * ∏ s : S, (g s : (a : E s) → ℝ) (X s ω)) P
⊢ HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)
          (∫ (a : Ω), ∏ x : S, (g x : (a : E x) → ℝ) (X x a) ∂P : ℝ) -
      HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
    (HSMul.hSMul (β := ℝ) ((P.restrict A).real Set.univ) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
        HSMul.hSMul (β := ℝ) ((P.restrict Aᶜ).real Set.univ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
      ∫ (x : Ω), ∏ x_1 : S, (g x_1 : (a : E x_1) → ℝ) (X x_1 x) ∂P
have simp : HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 1 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) +
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P : ℝ) -
    HMul.hMul (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (P.real A * ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P) =
  (HMul.hMul (β := ℝ) (P.real A) ((f : (a : ℝ) → ℝ) 1 : ℝ) +
      HMul.hMul (β := ℝ) (1 - P.real A) ((f : (a : ℝ) → ℝ) 0 : ℝ)) *
    ∫ (ω : Ω), ∏ s : S, (g s : (a : E s) → ℝ) (X s ω) ∂P
Tactic: simp [measureReal_compl₀ mA]
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω
have have : ∀ (this : Fintype S), A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω
Tactic: have := Fintype.ofFinite S
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (s : S) ↦ X s ω
have refine : ∀ (f : (s : S) → E s →ᵇ ℝ),
  ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
    P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
Tactic: refine indicator_indepFun_pi_of_prod_bcf mA mX fun f ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst : (s : S) → TopologicalSpace (E s)
inst_1 : (s : S) → MeasurableSpace (E s)
inst_2 : ∀ (s : S), BorelSpace.{u_4} (E s)
inst_3 : ∀ (s : S), HasOuterApproxClosed.{u_4} (E s)
X : (s : S) → Ω → E s
inst_4 : IsProbabilityMeasure P
inst_5 : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ),
    ∫ (ω : Ω) in A, (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P =
      P.real A * ∫ (ω : Ω), (f : (a : (s : S) → E s) → ℝ) fun (x : S) ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P =
    P.real A * ∫ (ω : Ω), ∏ s : S, (f s : (a : E s) → ℝ) (X s ω) ∂P
have h₁ : ∀ (x : Ω),
  Eq (α := ℝ) (∏ s : S, (f s : (a : E s) → ℝ) (X s x) : ℝ)
    ((∏ s : S, (f s).compContinuous { toFun := Function.eval (β := E) s, continuous_toFun := sorry } :
          (a : (s : S) → E s) → ℝ)
        fun (x_1 : S) ↦ X x_1 x :
      ℝ)
Tactic: convert! h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] Z
have suffices : A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (x : Unit) ↦ Z ω
Tactic: suffices (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω (_ : Unit) ↦ Z ω) from
    this.comp (measurable_id) (measurable_pi_apply ())
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
⊢ A.indicator 1 ⟂ᵢ[P] fun (ω : Ω) (x : Unit) ↦ Z ω
have refine : ∀ (f : (s : Unit) → G →ᵇ ℝ),
  ∫ (ω : Ω) in A, ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P =
    P.real A * ∫ (ω : Ω), ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P
Tactic: refine indicator_indepFun_pi_of_prod_bcf mA (fun _ ↦ mZ) fun f ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.BoundedContinuousFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst : TopologicalSpace G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : HasOuterApproxClosed G
Z : Ω → G
inst_4 : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, (f : (a : G) → ℝ) (Z ω) ∂P = P.real A * ∫ (ω : Ω), (f : (a : G) → ℝ) (Z ω) ∂P
f : (s : Unit) → G →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P =
    P.real A * ∫ (ω : Ω), ∏ s : Unit, (f s : (a : G) → ℝ) (Z ω) ∂P
have h₁ : ∀ (x : Ω), Eq (α := ℝ) (∏ s : Unit, (f s : (a : G) → ℝ) (Z x) : ℝ) ((f () : (a : G) → ℝ) (Z x) : ℝ)
Tactic: convert! h (f ())
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFun (mE := mE) (Measure.map (X + Y) P) =
    charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)
have h : ∀ (t : E),
  charFun (mE := mE) (Measure.map (X + Y) P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
⊢ charFun (mE := mE) (Measure.map (X + Y) P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
have h : charFun (mE := mE) (Measure.map X P ∗ Measure.map Y P) t =
  (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFun_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
h :
  charFun (mE := mE) (Measure.map X P ∗ Measure.map Y P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
⊢ charFun (mE := mE) (Measure.map (X + Y) P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
have h₁ : charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t =
  (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFun_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
X : Ω → E
inst_4 : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
t : E
h :
  charFun (mE := mE) (Measure.map X P ∗ Measure.map Y P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
h₁ :
  charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
⊢ charFun (mE := mE) (Measure.map (X + Y) P) t =
    (charFun (mE := mE) (Measure.map X P) * charFun (mE := mE) (Measure.map Y P)) t
have h₂ : charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t =
  charFun (mE := mE) (Measure.map X P) t * charFun (mE := mE) (Measure.map Y P) t
Tactic: rw [hXY.map_add_eq_map_conv_map₀ mX mY, charFun_conv, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ charFun (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) = charFun μ * charFun ν
have mX : AEMeasurable Prod.fst (μ.prod ν)
Tactic: rw [IndepFun.charFun_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
⊢ charFun (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) = charFun μ * charFun ν
have mY : AEMeasurable Prod.snd (μ.prod ν)
Tactic: rw [IndepFun.charFun_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : NormedAddCommGroup E
inst_1 : BorelSpace E
inst_2 : SecondCountableTopology E
inst_3 : InnerProductSpace ℝ E
μ ν : Measure E
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
mX : AEMeasurable Prod.fst (μ.prod ν)
mY : AEMeasurable Prod.snd (μ.prod ν)
⊢ charFun (mE := mE) (Measure.map (fun (p : E × E) ↦ p.1 + p.2) (μ.prod ν)) = charFun μ * charFun ν
have hXY : Prod.fst ⟂ᵢ[μ.prod ν] Prod.snd
Tactic: rw [IndepFun.charFun_map_fun_add_eq_mul, measurePreserving_fst.map_eq,
    measurePreserving_snd.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.CharacteristicFunction (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
have rw : Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
    (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
      charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_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 Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
rw :
  Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
      (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
have rw₁ : (∀ (t : WithLp 2 (E × F)),
    charFun (mE := measurableSpace 2 (E × F)) (Measure.map (toLp 2) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)) t =
      charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
      charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_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 Ω
inst : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
mF : MeasurableSpace F
inst_4 : NormedAddCommGroup F
inst_5 : CompleteSpace F
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst_8 : InnerProductSpace ℝ E
inst_9 : InnerProductSpace ℝ F
inst_10 : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
rw :
  Eq (α := Measure (E × F)) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)
      (Measure.prod (Measure.map X P) (Measure.map Y P)) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
rw₁ :
  (∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (toLp 2) (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) P)) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
have rw₂ : (∀ (t : WithLp 2 (E × F)),
    charFun (mE := measurableSpace 2 (E × F)) (Measure.map (toLp 2 ∘ fun (ω : Ω) ↦ (X ω, Y ω)) P) t =
      charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2) ↔
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := measurableSpace 2 (E × F)) (Measure.map (fun (ω : Ω) ↦ toLp 2 (X ω, Y ω)) P) t =
      charFun (mE := mE) (Measure.map X P) t.ofLp.1 * charFun (mE := mF) (Measure.map Y P) t.ofLp.2
Tactic: rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_iff,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]