awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
e_f :
  cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I)
⊢ cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
rw [← Complex.exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
e_f : (↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I = (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I
⊢ cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
e_f :
  ((↑((L : (a : E) → ℝ) a) : ℂ) + (↑((L : (a : E) → ℝ) r) : ℂ)) * I =
    (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I
⊢ (↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I = (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I

Tactic:
simp only [map_add, ofReal_add]

Premises used: Complex.ofReal_add, map_add
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ ((↑((L : (a : E) → ℝ) a) : ℂ) + (↑((L : (a : E) → ℝ) r) : ℂ)) * I =
    (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
simp_rw :
  charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ x + r) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
⊢ charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ r + x) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
simp_rw [add_comm r]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ x + r) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
charFunDual_map_add_const _ _

Premises used: MeasureTheory.charFunDual_map_add_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ x + r) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
exact charFunDual_map_add_const _ _

Premises used: MeasureTheory.charFunDual_map_add_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst_4 : SFinite μ
inst_5 : SFinite ν
L : StrongDual ℝ (E × F)
simp_rw :
  ∫ (v : E × F), cexp ((↑((L : (a : E × F) → ℝ) v) : ℂ) * I) ∂μ.prod ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : F), cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v) : ℂ) * I) ∂ν)
simp_rw₁ :
  ∫ (v : E × F),
      cexp
        ((↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v.1 : ℝ)
                ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v.2 : ℝ)) :
            ℂ) *
          I) ∂μ.prod ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : F), cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v) : ℂ) * I) ∂ν)
simp_rw₂ :
  ∫ (v : E × F),
      cexp
        (((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v.1) : ℂ) +
            (↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v.2) : ℂ)) *
          I) ∂μ.prod ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : F), cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v) : ℂ) * I) ∂ν)
simp_rw₃ :
  ∫ (v : E × F),
      cexp
        ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v.1) : ℂ) * I +
          (↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v.2) : ℂ) * I) ∂μ.prod ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : F), cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v) : ℂ) * I) ∂ν)
simp_rw₄ :
  ∫ (v : E × F),
      cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v.1) : ℂ) * I) *
        cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v.2) : ℂ) * I) ∂μ.prod ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : F), cexp ((↑((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) v) : ℂ) * I) ∂ν)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]

Premises used: add_mul, MeasureTheory.charFunDual_apply, ContinuousLinearMap.comp_inl_add_comp_inr, Complex.exp_add, Complex.ofReal_add, MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
inst_5 : SFinite μ
inst_6 : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ (WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) fun (v : WithLp p (E × F)) ↦
      cexp ((↑((L : (a : WithLp p (E × F)) → ℝ) v) : ℂ) * I))
    (∫ (z : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) :
                      (a : E × F) → WithLp p (E × F))
                    z :
                  WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)
⊢ charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L =
    charFunDual μ
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν
        (L ∘SL
          (↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) ∘SL
            ContinuousLinearMap.inr ℝ E F)

Tactic:
simp_rw [charFunDual_apply, ← integral_prod_mul, ← Complex.exp_add, ← add_mul, ← ofReal_add,
    L.comp_apply, ← map_add, ContinuousLinearMap.comp_inl_add_comp_inr]

Premises used: add_mul, MeasureTheory.charFunDual_apply, ContinuousLinearMap.comp_inl_add_comp_inr, Complex.exp_add, Complex.ofReal_add, map_add, MeasureTheory.integral_prod_mul, ContinuousLinearMap.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
inst_5 : SFinite μ
inst_6 : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
rw :
  Eq (α := ℂ)
    (∫ (x : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                ((MeasurableEquiv.toLp p (E × F) : (a : E × F) → WithLp p (E × F)) x : WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)
    (∫ (z : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) :
                      (a : E × F) → WithLp p (E × F))
                    z :
                  WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ (WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) fun (v : WithLp p (E × F)) ↦
      cexp ((↑((L : (a : WithLp p (E × F)) → ℝ) v) : ℂ) * I))
    (∫ (z : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) :
                      (a : E × F) → WithLp p (E × F))
                    z :
                  WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)

Tactic:
rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]

Premises used: MeasurableEquiv.coe_toLp, MeasureTheory.integral_map_equiv
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst_4 : Fact (1 ≤ p)
inst_5 : SFinite μ
inst_6 : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ Eq (α := ℂ)
    (∫ (x : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                ((MeasurableEquiv.toLp p (E × F) : (a : E × F) → WithLp p (E × F)) x : WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)
    (∫ (z : E × F),
      cexp
        ((↑((L : (a : WithLp p (E × F)) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (prodContinuousLinearEquiv p ℝ E F)) : E × F →L[ℝ] WithLp p (E × F)) :
                      (a : E × F) → WithLp p (E × F))
                    z :
                  WithLp p (E × F))) :
            ℂ) *
          I) ∂μ.prod ν)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_5
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_4 : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
simp_rw :
  Eq (α := ℂ) (∫ (v : (i : ι) → E i), cexp ((↑((L : (a : (i : ι) → E i) → ℝ) v) : ℂ) * I) ∂Measure.pi (α := E) μ)
    (∏ x : ι,
      ∫ (v : E x),
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ) v) :
              ℂ) *
            I) ∂μ x)
simp_rw₁ :
  Eq (α := ℂ)
    (∫ (v : (i : ι) → E i),
      cexp
        ((↑(∑ i : ι,
                (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i) : (a : E i) → ℝ)
                  (v i)) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
    (∏ x : ι,
      ∫ (v : E x),
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ) v) :
              ℂ) *
            I) ∂μ x)
simp_rw₂ :
  Eq (α := ℂ)
    (∫ (v : (i : ι) → E i),
      cexp
        ((∑ i : ι,
            (↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i) : (a : E i) → ℝ)
                  (v i)) :
              ℂ)) *
          I) ∂Measure.pi (α := E) μ)
    (∏ x : ι,
      ∫ (v : E x),
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ) v) :
              ℂ) *
            I) ∂μ x)
simp_rw₃ :
  Eq (α := ℂ)
    (∫ (v : (i : ι) → E i),
      cexp
        (∑ i : ι,
          (↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i) : (a : E i) → ℝ)
                  (v i)) :
              ℂ) *
            I) ∂Measure.pi (α := E) μ)
    (∏ x : ι,
      ∫ (v : E x),
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ) v) :
              ℂ) *
            I) ∂μ x)
simp_rw₄ :
  Eq (α := ℂ)
    (∫ (v : (i : ι) → E i),
      ∏ x : ι,
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ)
                  (v x)) :
              ℂ) *
            I) ∂Measure.pi (α := E) μ)
    (∏ x : ι,
      ∫ (v : E x),
        cexp
          ((↑((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E x) : (a : E x) → ℝ) v) :
              ℂ) *
            I) ∂μ x)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))

Tactic:
simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]

Premises used: ContinuousLinearMap.sum_comp_single, MeasureTheory.charFunDual_apply, MeasureTheory.integral_fintype_prod_eq_prod, Complex.ofReal_sum, Complex.exp_sum, Finset.sum_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_5 : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ (WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ))
      fun (v : WithLp p ((i : ι) → E i)) ↦ cexp ((↑((L : (a : WithLp p ((i : ι) → E i)) → ℝ) v) : ℂ) * I))
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : PiLp p E) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E) :
                      (a : (i : ι) → E i) → PiLp p E)
                    x :
                  PiLp p E)) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
⊢ charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L =
    ∏ i : ι,
      charFunDual (μ i)
        (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:
simp_rw [charFunDual_apply, ← integral_fintype_prod_eq_prod, ← Complex.exp_sum, ← Finset.sum_mul,
    ← ofReal_sum, L.comp_apply, ← map_sum, ContinuousLinearMap.sum_comp_single]

Premises used: ContinuousLinearMap.sum_comp_single, MeasureTheory.charFunDual_apply, MeasureTheory.integral_fintype_prod_eq_prod, map_sum, Complex.ofReal_sum, Complex.exp_sum, Finset.sum_mul, ContinuousLinearMap.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_5 : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
rw :
  Eq (α := ℂ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : WithLp p ((i : ι) → E i)) → ℝ)
                ((MeasurableEquiv.toLp p ((i : ι) → E i) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) x :
                  WithLp p ((i : ι) → E i))) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : PiLp p E) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E) :
                      (a : (i : ι) → E i) → PiLp p E)
                    x :
                  PiLp p E)) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ (WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ))
      fun (v : WithLp p ((i : ι) → E i)) ↦ cexp ((↑((L : (a : WithLp p ((i : ι) → E i)) → ℝ) v) : ℂ) * I))
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : PiLp p E) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E) :
                      (a : (i : ι) → E i) → PiLp p E)
                    x :
                  PiLp p E)) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)

Tactic:
rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]

Premises used: MeasurableEquiv.coe_toLp, MeasureTheory.integral_map_equiv
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_5 : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ Eq (α := ℂ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : WithLp p ((i : ι) → E i)) → ℝ)
                ((MeasurableEquiv.toLp p ((i : ι) → E i) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) x :
                  WithLp p ((i : ι) → E i))) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑((L : (a : PiLp p E) → ℝ)
                (((↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E) :
                      (a : (i : ι) → E i) → PiLp p E)
                    x :
                  PiLp p E)) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ μ = ν

Tactic:
ext_of_integral_char_eq continuous_probChar probChar_ne_one
    ?_ ?_ (fun L ↦ funext_iff.mp h L)

Premises used: funext_iff, Real.continuous_probChar, MeasureTheory.ext_of_integral_char_eq, Iff.mp, Real.probChar_ne_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
refine_1 :
  ∀ (v : E),
    v ≠ 0 →
      Ne (α := StrongDual ℝ E →ₗ[ℝ] ℝ)
        ((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            v :
          StrongDual ℝ E →ₗ[ℝ] ℝ)
        (0 : StrongDual ℝ E →ₗ[ℝ] ℝ)
refine_2 :
  Continuous (Y := ℝ) fun (p : E × StrongDual ℝ E) ↦
    (((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            p.1 :
          StrongDual ℝ E →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      p.2
⊢ μ = ν

Tactic:
refine ext_of_integral_char_eq continuous_probChar probChar_ne_one
    ?_ ?_ (fun L ↦ funext_iff.mp h L)

Premises used: funext_iff, Real.continuous_probChar, MeasureTheory.ext_of_integral_char_eq, Iff.mp, Real.probChar_ne_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ ∀ (v : E),
    v ≠ 0 →
      Ne (α := StrongDual ℝ E →ₗ[ℝ] ℝ)
        ((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            v :
          StrongDual ℝ E →ₗ[ℝ] ℝ)
        (0 : StrongDual ℝ E →ₗ[ℝ] ℝ)

Tactic:
fun v hv ↦ DFunLike.ne_iff.mpr <| SeparatingDual.exists_ne_zero hv

Premises used: Iff.mpr, SeparatingDual.exists_ne_zero, DFunLike.ne_iff
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ ∀ (v : E),
    v ≠ 0 →
      Ne (α := StrongDual ℝ E →ₗ[ℝ] ℝ)
        ((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            v :
          StrongDual ℝ E →ₗ[ℝ] ℝ)
        (0 : StrongDual ℝ E →ₗ[ℝ] ℝ)

Tactic:
exact fun v hv ↦ DFunLike.ne_iff.mpr <| SeparatingDual.exists_ne_zero hv

Premises used: Iff.mpr, DFunLike.ne_iff
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ Continuous (Y := ℝ) fun (p : E × StrongDual ℝ E) ↦
    (((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            p.1 :
          StrongDual ℝ E →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      p.2

Tactic:
isBoundedBilinearMap_apply.symm.continuous

Premises used: IsBoundedBilinearMap.continuous, IsBoundedBilinearMap.symm, isBoundedBilinearMap_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
inst_4 : CompleteSpace E
μ ν : Measure E
inst_5 : IsFiniteMeasure μ
inst_6 : IsFiniteMeasure ν
h : Eq (α := (L : StrongDual ℝ E) → ℂ) (charFunDual μ) (charFunDual ν)
⊢ Continuous (Y := ℝ) fun (p : E × StrongDual ℝ E) ↦
    (((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap ⋯) :
              (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
            p.1 :
          StrongDual ℝ E →ₗ[ℝ] ℝ) :
        (a : StrongDual ℝ E) → ℝ)
      p.2

Tactic:
exact isBoundedBilinearMap_apply.symm.continuous

Premises used: IsBoundedBilinearMap.continuous, IsBoundedBilinearMap.symm, isBoundedBilinearMap_apply