awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
have rw : ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ =
  charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
Tactic: rw [charFunDual_apply]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
have hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
Tactic: rw [integral_map]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
have hfm : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
  (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
have this : Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
Tactic: have : ∫ x, cexp (L x * I) ∂μ = ∫ x, cexp (x * I) ∂(μ.map L) := by
    rw [integral_map]
    · fun_prop
    · exact Measurable.aestronglyMeasurable <| by fun_prop
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, 1⟫ : ℂ) * I))
Tactic: rw [this, charFun_apply]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u = charFunDual μ (u • L)
have rw : charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
  ∫ (v : E), cexp ((↑((u • L : (a : E) → ℝ) v) : ℂ) * I) ∂μ
Tactic: rw [charFunDual_apply]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
have rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
  (∫ (x : E), cexp ((↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
Tactic: rw [integral_map]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
rw :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (∫ (x : E), cexp ((↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
have hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
Tactic: rw [integral_map]
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
rw :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (∫ (x : E), cexp ((↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
have hfm : AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑u : ℂ) * (↑x : ℂ) * I))
  (Measure.map (⇑L : (a : E) → ℝ) μ)
Tactic: rw [integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    ∫ (v : E), cexp ((↑((u • L : (a : E) → ℝ) v) : ℂ) * I) ∂μ
have this : Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
    cexp ((↑u : ℂ) * (↑x : ℂ) * I))
Tactic: have : ∫ x, cexp ((u • L) x * I) ∂μ = ∫ x, cexp (u * x * I) ∂(μ.map L) := by
    rw [integral_map]
    · simp
    · fun_prop
    · exact Measurable.aestronglyMeasurable <| by fun_prop
-- 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
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    ∫ (v : E), cexp ((↑((u • L : (a : E) → ℝ) v) : ℂ) * I) ∂μ
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, u⟫ : ℂ) * I))
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
    cexp ((↑u : ℂ) * (↑x : ℂ) * I))
Tactic: rw [this, charFun_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
L : StrongDual ℝ E
⊢ charFun μ ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L) = charFunDual μ L
have rw : charFunDual μ
    ((InnerProductSpace.toDual ℝ E : (a : E) → StrongDual ℝ E)
      ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L)) =
  charFunDual μ L
Tactic: rw [charFun_eq_charFunDual_toDualMap, ← InnerProductSpace.toDual_apply_eq_toDualMap_apply]
-- 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
inst_4 : OpensMeasurableSpace E
inst_5 : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ charFunDual (mE := mF) (Measure.map (⇑L : (a : E) → F) μ) L' = charFunDual μ (L' ∘SL L)
have rw : charFun (E := ℝ) (mE := Real.measurableSpace)
    (Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ) 1 =
  charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑(L' ∘SL L) : (a : E) → ℝ) μ) 1
Tactic: rw [charFunDual_eq_charFun_map_one, charFunDual_eq_charFun_map_one,
    Measure.map_map (by fun_prop) (by fun_prop)]
-- 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 : OpensMeasurableSpace E
x : E
L : StrongDual ℝ E
⊢ charFunDual (mE := mE) (Measure.dirac x) L = cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
have rw : (@integral _ _ _ _ mE (Measure.dirac x) fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) =
  cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
Tactic: rw [charFunDual_apply, integral_dirac]
-- 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 : OpensMeasurableSpace E
x : E
L : StrongDual ℝ E
rw :
  (@integral _ _ _ _ mE (Measure.dirac x) fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) =
    cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
⊢ charFunDual (mE := mE) (Measure.dirac x) L = cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
have rw₁ : cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) = cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
Tactic: rw [charFunDual_apply, integral_dirac]
-- 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
μ : 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)
have rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) (x + r)) : ℂ) * I) ∂μ)
  (∫ (a : E), cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I) ∂μ)
Tactic: rw [charFunDual_apply, charFunDual_apply, integral_map (by fun_prop) (by fun_prop),
    ← integral_mul_const]
-- 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
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) (x + r)) : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I) ∂μ)
have e_f : ∀ (a : E),
  cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
Tactic: congr with a
-- 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
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
have e_f : cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
  cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I)
Tactic: rw [← Complex.exp_add]
-- 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
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
    cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I)
have e_f : (↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I = (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I
Tactic: congr
-- 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
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
a : E
⊢ (↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I = (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I
have e_f : ((↑((L : (a : E) → ℝ) a) : ℂ) + (↑((L : (a : E) → ℝ) r) : ℂ)) * I =
  (↑((L : (a : E) → ℝ) a) : ℂ) * I + (↑((L : (a : E) → ℝ) r) : ℂ) * I
Tactic: simp only [map_add, ofReal_add]
-- 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
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ r + x) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
have simp_rw : charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ x + r) μ) L =
  charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
Tactic: simp_rw [add_comm r]
-- 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 : SFinite μ
inst_5 : SFinite ν
L : StrongDual ℝ (E × F)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
have 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) ∂ν)
Tactic: simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]
-- 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 : 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) ∂ν)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
have 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) ∂ν)
Tactic: simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]
-- 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 : 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) ∂ν)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
have 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) ∂ν)
Tactic: simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]
-- 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 : 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) ∂ν)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
have 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) ∂ν)
Tactic: simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]
-- 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 : 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) ∂ν)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
have 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) ∂ν)
Tactic: simp_rw [charFunDual_apply, ← L.comp_inl_add_comp_inr, ofReal_add, add_mul,
    Complex.exp_add, ← integral_prod_mul]