awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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))
⊢ 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)
have 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 ν)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 (α := ℂ)
    (@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 ν)
have 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 ν)
Tactic: rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have 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)
Tactic: simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have 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)
Tactic: simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have 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)
Tactic: simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have 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)
Tactic: simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have 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)
Tactic: simp_rw [charFunDual_apply, ← L.sum_comp_single, ofReal_sum, Finset.sum_mul, Complex.exp_sum,
    ← integral_fintype_prod_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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)
⊢ 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)))
have 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) μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 (α := ℂ)
    (@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) μ)
have 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) μ)
Tactic: rw [← MeasurableEquiv.coe_toLp, integral_map_equiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 ν)
⊢ μ = ν
have refine_1 : ∀ (v : E),
  v ≠ 0 →
    Ne (α := StrongDual ℝ E →ₗ[ℝ] ℝ)
      ((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap sorry) :
            (a : E) → StrongDual ℝ E →ₗ[ℝ] ℝ)
          v :
        StrongDual ℝ E →ₗ[ℝ] ℝ)
      (0 : StrongDual ℝ E →ₗ[ℝ] ℝ)
Tactic: refine ext_of_integral_char_eq continuous_probChar probChar_ne_one
    ?_ ?_ (fun L ↦ funext_iff.mp h L)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 →ₗ[ℝ] ℝ)
⊢ μ = ν
have refine_2 : Continuous (Y := ℝ) fun (p : E × StrongDual ℝ E) ↦
  (((ContinuousLinearMap.toLinearMap₁₂ (IsBoundedBilinearMap.toContinuousLinearMap sorry) :
            (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
⊢ ξ = μ.prod ν
have refine : ∀ (t : StrongDual ℝ (E × F)), charFunDual ξ t = charFunDual (μ.prod ν) t
Tactic: refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
t : StrongDual ℝ (E × F)
⊢ charFunDual ξ t = charFunDual (μ.prod ν) t
have rw : charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
    charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F)) =
  charFunDual (μ.prod ν) t
Tactic: rw [h, charFunDual_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
t : StrongDual ℝ (E × F)
rw :
  charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
      charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F)) =
    charFunDual (μ.prod ν) t
⊢ charFunDual ξ t = charFunDual (μ.prod ν) t
have rw₁ : charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
    charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F)) =
  charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inl ℝ E F)) *
    charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.inr ℝ E F))
Tactic: rw [h, charFunDual_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
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 : BorelSpace E
inst_5 : SecondCountableTopology E
inst_6 : BorelSpace F
inst_7 : SecondCountableTopology F
inst_8 : CompleteSpace E
inst_9 : CompleteSpace F
ξ : Measure (E × F)
inst_10 : IsFiniteMeasure μ
inst_11 : IsFiniteMeasure ν
inst_12 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
        charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
have rw : ∀ (L : StrongDual ℝ (E × F)),
  charFunDual (μ.prod ν) L =
    charFunDual μ (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inl ℝ E F)) *
      charFunDual ν (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.inr ℝ E F))
Tactic: rw [h]