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
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) 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)
⊢ ξ = μ.prod ν
have refine : ∀ (L : StrongDual ℝ (WithLp p (E × F))),
  charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L
Tactic: refine (MeasurableEquiv.toLp p (E × F)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun 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
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) 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)
L : StrongDual ℝ (WithLp p (E × F))
⊢ charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L
have rw : charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
  charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
Tactic: rw [MeasurableEquiv.coe_toLp, 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
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) 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)
L : StrongDual ℝ (WithLp p (E × F))
rw :
  charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
⊢ charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L
have rw₁ : 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) =
  charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
Tactic: rw [MeasurableEquiv.coe_toLp, 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
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) 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)
L : StrongDual ℝ (WithLp p (E × F))
rw :
  charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
rw₁ :
  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) =
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) (μ.prod ν)) L
⊢ charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) ξ) L =
    charFunDual (mE := WithLp.measurableSpace p (E × F))
      (Measure.map (⇑(MeasurableEquiv.toLp p (E × F)) : (a : E × F) → WithLp p (E × F)) (μ.prod ν)) L
have rw₂ : 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) =
  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: rw [MeasurableEquiv.coe_toLp, 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
p : ℝ≥0∞
inst_6 : Fact (1 ≤ p)
inst_7 : BorelSpace F
inst_8 : SecondCountableTopology F
inst_9 : CompleteSpace E
inst_10 : CompleteSpace F
ξ : Measure (E × F)
inst_11 : IsFiniteMeasure μ
inst_12 : IsFiniteMeasure ν
inst_13 : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (WithLp p (E × F))),
    charFunDual (mE := WithLp.measurableSpace p (E × F)) (Measure.map (toLp p) ξ) 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 rw : ∀ (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)
Tactic: rw [h]
-- 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)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
⊢ ν = Measure.pi (α := E) μ
have refine : ∀ (t : StrongDual ℝ ((i : ι) → E i)), charFunDual ν t = charFunDual (Measure.pi (α := E) μ) t
Tactic: refine Measure.ext_of_charFunDual <| funext fun t ↦ ?_
-- 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)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
t : StrongDual ℝ ((i : ι) → E i)
⊢ charFunDual ν t = charFunDual (Measure.pi (α := E) μ) t
have rw : ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)) =
  charFunDual (Measure.pi (α := E) μ) t
Tactic: rw [h, charFunDual_pi]
-- 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)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
t : StrongDual ℝ ((i : ι) → E i)
rw :
  ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)) =
    charFunDual (Measure.pi (α := E) μ) t
⊢ charFunDual ν t = charFunDual (Measure.pi (α := E) μ) t
have rw₁ : Eq (α := ℂ)
  (∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)))
  (∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) t (ContinuousLinearMap.single ℝ E i)))
Tactic: rw [h, charFunDual_pi]
-- 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)
inst_4 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_6 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_7 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_8 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ ((i : ι) → E i)),
    charFunDual ν L =
      ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
have rw : ∀ (L : StrongDual ℝ ((i : ι) → E i)),
  charFunDual (Measure.pi (α := E) μ) L =
    ∏ i : ι, charFunDual (μ i) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L (ContinuousLinearMap.single ℝ E i))
Tactic: rw [h]
-- 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)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) 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)))
⊢ ν = Measure.pi (α := E) μ
have refine : ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      L
Tactic: refine (MeasurableEquiv.toLp p (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFunDual <| funext fun L ↦ ?_
-- 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)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) 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)))
L : StrongDual ℝ (WithLp p ((i : ι) → E i))
⊢ charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      L
have rw : charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFunDual_pi']
-- 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)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) 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)))
L : StrongDual ℝ (WithLp p ((i : ι) → E i))
rw :
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
⊢ charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      L
have rw₁ : ∏ 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))) =
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
Tactic: rw [MeasurableEquiv.coe_toLp, h, charFunDual_pi']
-- 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)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h :
  ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) 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)))
L : StrongDual ℝ (WithLp p ((i : ι) → E i))
rw :
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
rw₁ :
  ∏ 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))) =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L
⊢ charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i)) ν) L =
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp p ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp p ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      L
have rw₂ : Eq (α := ℂ)
  (∏ 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))))
  (∏ 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: rw [MeasurableEquiv.coe_toLp, h, charFunDual_pi']