awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hf : AEMeasurable f μ
r t : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (x : X) ↦ r * f x) μ) t =
    charFun (mE := Real.measurableSpace) (Measure.map f μ) (r * t)

Tactic:
charFun_map_smul_comp hf r t

Premises used: MeasureTheory.charFun_map_smul_comp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : OpensMeasurableSpace E
x t : E
rw : (@integral _ _ _ _ inst (Measure.dirac x) fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) = cexp ((↑⟪x, t⟫ : ℂ) * I)
rw₁ rw₂ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp ((↑⟪x, t⟫ : ℂ) * I)
⊢ charFun (mE := inst) (Measure.dirac x) t = cexp ((↑⟪x, t⟫ : ℂ) * I)

Tactic:
rw [charFun_apply, integral_dirac]

Premises used: MeasureTheory.charFun_apply, MeasureTheory.integral_dirac
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ AEMeasurable (β := E) (fun (x : E) ↦ x + r) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := inst) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I))
    (Measure.map (fun (x : E) ↦ x + r) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
rw :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x + r, t⟫ : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I) ∂μ)
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)

Tactic:
rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop),
    ← integral_mul_const]

Premises used: MeasureTheory.charFun_apply, MeasureTheory.integral_map, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
e_f : ∀ (a : E), cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x + r, t⟫ : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I) ∂μ)

Tactic:
congr with a
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
e_f : cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I)
⊢ cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I) * cexp ((↑⟪r, t⟫ : ℂ) * I)

Tactic:
rw [← Complex.exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
e_f : (↑⟪a + r, t⟫ : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
⊢ cexp ((↑⟪a + r, t⟫ : ℂ) * I) = cexp ((↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
e_f : (↑(⟪a, t⟫ + ⟪r, t⟫) : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
⊢ (↑⟪a + r, t⟫ : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I

Tactic:
rw [inner_add_left]

Premises used: inner_add_left
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
e_f : ((↑⟪a, t⟫ : ℂ) + (↑⟪r, t⟫ : ℂ)) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I
⊢ (↑(⟪a, t⟫ + ⟪r, t⟫) : ℂ) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I

Tactic:
simp only [ofReal_add]

Premises used: Complex.ofReal_add
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t a : E
⊢ ((↑⟪a, t⟫ : ℂ) + (↑⟪r, t⟫ : ℂ)) * I = (↑⟪a, t⟫ : ℂ) * I + (↑⟪r, t⟫ : ℂ) * I

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
simp_rw : charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ r + x) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)

Tactic:
simp_rw [add_comm r]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)

Tactic:
charFun_map_add_const _ _

Premises used: MeasureTheory.charFun_map_add_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
r t : E
⊢ charFun (mE := inst) (Measure.map (fun (x : E) ↦ x + r) μ) t = charFun μ t * cexp ((↑⟪r, t⟫ : ℂ) * I)

Tactic:
exact charFun_map_add_const _ _

Premises used: MeasureTheory.charFun_map_add_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h : charFun μ = charFun ν
⊢ ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)

Tactic:
simp_rw [funext_iff, charFun_eq_integral_innerProbChar] at h

Premises used: funext_iff, MeasureTheory.charFun_eq_integral_innerProbChar
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ μ = ν

Tactic:
ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
    ?_ ?_ h

Premises used: Real.continuous_probChar, MeasureTheory.ext_of_integral_char_eq, Real.probChar_ne_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
refine_1 :
  ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)
refine_2 :
  Continuous (Y := ℝ) fun (p : E × E) ↦
    ((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) p.1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) p.2
⊢ μ = ν

Tactic:
refine ext_of_integral_char_eq continuous_probChar probChar_ne_one (L := innerₗ E)
    ?_ ?_ h

Premises used: Real.continuous_probChar, MeasureTheory.ext_of_integral_char_eq, Real.probChar_ne_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)

Tactic:
fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩

Premises used: Iff.mpr, inner_self_ne_zero, DFunLike.ne_iff, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)

Tactic:
exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩

Premises used: Iff.mpr, DFunLike.ne_iff, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ Continuous (Y := ℝ) fun (p : E × E) ↦
    ((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) p.1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) p.2

Tactic:
continuous_inner

Premises used: continuous_inner
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : CompleteSpace E
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (x : E),
    Eq (α := ℂ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂μ) (∫ (v : E), (innerProbChar x : (a : E) → ℂ) v ∂ν)
⊢ Continuous (Y := ℝ) fun (p : E × E) ↦
    ((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) p.1 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) p.2

Tactic:
exact continuous_inner

Premises used: continuous_inner
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
rw :
  ∫ (x : E), ∫ (y : E), cexp ((↑⟪x + y, t⟫ : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)
rw₁ : Integrable (ε := ℂ) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) (μ ∗ ν)
⊢ ∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)

Tactic:
rw [integral_conv]

Premises used: MeasureTheory.integral_conv
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
⊢ ∫ (x : E), ∫ (y : E), cexp ((↑⟪x + y, t⟫ : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂ν)

Tactic:
simp [inner_add_left, add_mul, Complex.exp_add, integral_const_mul, integral_mul_const]

Premises used: add_mul, MeasureTheory.integral_const_mul, Complex.exp_add, inner_add_left, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
⊢ AEStronglyMeasurable (β := ℂ) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) (μ ∗ ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
⊢ ∀ᵐ (a : E) ∂μ ∗ ν, ‖cexp ((↑⟪a, t⟫ : ℂ) * I)‖ ≤ Norm.norm (E := ℝ) 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_3
inst : MeasurableSpace E
μ ν : Measure E
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
t : E
⊢ Integrable (ε := ℂ) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I)) (μ ∗ ν)

Tactic:
exact (integrable_const (1 : ℝ)).mono (by fun_prop) (by simp)

Premises used: MeasureTheory.Integrable.mono, OfNat.ofNat, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : SFinite μ
inst_5 : SFinite ν
t : WithLp 2 (E × F)
simp_rw :
  Eq (α := ℂ)
    (∫ (x : E × F),
      cexp
        ((↑(⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).1, t.ofLp.1⟫ +
                ⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).2, t.ofLp.2⟫) :
            ℂ) *
          I) ∂μ.prod ν)
    (∫ (z : E × F), cexp ((↑⟪z.1, t.ofLp.1⟫ : ℂ) * I) * cexp ((↑⟪z.2, t.ofLp.2⟫ : ℂ) * I) ∂μ.prod ν)
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
    charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
simp_rw [charFun, prod_inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_prod_mul,
    integral_map_equiv]

Premises used: WithLp.prod_inner_apply, MeasurableEquiv.coe_toLp, MeasureTheory.charFun, MeasureTheory.integral_map_equiv, MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : SFinite μ
inst_5 : SFinite ν
t : WithLp 2 (E × F)
⊢ Eq (α := ℂ)
    (∫ (x : E × F),
      cexp
        ((↑(⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).1, t.ofLp.1⟫ +
                ⟪(ofLp (p := 2) ((MeasurableEquiv.toLp 2 (E × F) : (a : E × F) → WithLp 2 (E × F)) x)).2, t.ofLp.2⟫) :
            ℂ) *
          I) ∂μ.prod ν)
    (∫ (z : E × F), cexp ((↑⟪z.1, t.ofLp.1⟫ : ℂ) * I) * cexp ((↑⟪z.2, t.ofLp.2⟫ : ℂ) * I) ∂μ.prod ν)

Tactic:
simp [ofReal_add, add_mul, Complex.exp_add]

Premises used: add_mul, Complex.exp_add, Complex.ofReal_add
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
⊢ ξ = μ.prod ν

Tactic:
(MeasurableEquiv.toLp 2 (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFun, MeasurableEquiv.map_measurableEquiv_injective, Prod, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
refine :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F))
        (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
      charFun (mE := WithLp.measurableSpace 2 (E × F))
        (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t
⊢ ξ = μ.prod ν

Tactic:
refine (MeasurableEquiv.toLp 2 (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFun, MeasurableEquiv.map_measurableEquiv_injective, Prod, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
t : WithLp 2 (E × F)
rw :
  charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
rw₁ :
  charFun μ t.ofLp.1 * charFun ν t.ofLp.2 =
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t
rw₂ rw₃ : charFun μ t.ofLp.1 * charFun ν t.ofLp.2 = charFun μ t.ofLp.1 * charFun ν t.ofLp.2
⊢ charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) ξ) t =
    charFun (mE := WithLp.measurableSpace 2 (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 (E × F)) : (a : E × F) → WithLp 2 (E × F)) (μ.prod ν)) t

Tactic:
rw [MeasurableEquiv.coe_toLp, h, charFun_prod]

Premises used: MeasurableEquiv.coe_toLp, MeasureTheory.charFun_prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
rw :
  ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2
⊢ ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) ξ) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
charFun_prod

Premises used: MeasureTheory.charFun_prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
F : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
mE : MeasurableSpace E
mF : MeasurableSpace F
inst_4 : CompleteSpace E
inst_5 : CompleteSpace F
inst_6 : SecondCountableTopology E
inst_7 : SecondCountableTopology F
inst_8 : BorelSpace E
inst_9 : BorelSpace F
μ : Measure E
ν : Measure F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (t : WithLp 2 (E × F)),
    charFun (mE := WithLp.measurableSpace 2 (E × F)) (Measure.map (toLp 2) (μ.prod ν)) t =
      charFun μ t.ofLp.1 * charFun ν t.ofLp.2

Tactic:
exact charFun_prod

Premises used: MeasureTheory.charFun_prod
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
simp_rw :
  Eq (α := ℂ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑(∑ i : ι,
                ⟪ofLp (p := 2)
                    ((MeasurableEquiv.toLp 2 ((i : ι) → E i) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) x) i,
                  t.ofLp i⟫) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
    (∫ (x : (i : ι) → E i), ∏ i : ι, cexp ((↑⟪x i, t.ofLp i⟫ : ℂ) * I) ∂Measure.pi (α := E) μ)
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
    ∏ i : ι, charFun (μ i) (t.ofLp i)

Tactic:
simp_rw [charFun, PiLp.inner_apply, ← MeasurableEquiv.coe_toLp, ← integral_fintype_prod_eq_prod,
    integral_map_equiv]

Premises used: MeasureTheory.integral_fintype_prod_eq_prod, MeasurableEquiv.coe_toLp, MeasureTheory.charFun, MeasureTheory.integral_map_equiv, PiLp.inner_apply