awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
change :
  ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      ((⇑((AffineEquiv.homothetyUnitsMulHom x : (a : 𝕜ˣ) → P ≃ᵃ[𝕜] P) (Units.mk0 c hc) : P ≃ᵃ[𝕜] P) : (a : P) → P) ⁻¹'
        s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) ((⇑(AffineMap.homothety x c) : (a : P) → P) ⁻¹' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
change μH[d] (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 c hc) ⁻¹' s) = _

Premises used: MeasureTheory.Measure.hausdorffMeasure, AffineEquiv.homothetyUnitsMulHom, Units.mk0, Set.preimage, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : MeasurableSpace P
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
inst_6 : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
rw :
  ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      ((⇑(AffineEquiv.symm ((AffineEquiv.homothetyUnitsMulHom x : (a : 𝕜ˣ) → P ≃ᵃ[𝕜] P) (Units.mk0 c hc))) :
          (a : P) → P) ''
        s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      ((⇑(AffineMap.homothety x (↑((Units.mk0 c hc)⁻¹ : 𝕜ˣ) : 𝕜)) : (a : P) → P) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (‖(↑((Units.mk0 c hc)⁻¹ : 𝕜ˣ) : 𝕜)‖₊ ^ d)
      (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₃ :
  HSMul.hSMul (β := ℝ≥0∞) (‖(↑(Units.mk0 c hc : 𝕜ˣ) : 𝕜)⁻¹‖₊ ^ d)
      (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₄ :
  HSMul.hSMul (β := ℝ≥0∞) (‖c⁻¹‖₊ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
rw₅ rw₆ :
  HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞)
      ((⇑((AffineEquiv.homothetyUnitsMulHom x : (a : 𝕜ˣ) → P ≃ᵃ[𝕜] P) (Units.mk0 c hc) : P ≃ᵃ[𝕜] P) : (a : P) → P) ⁻¹'
        s) =
    HSMul.hSMul (β := ℝ≥0∞) (‖c‖₊⁻¹ ^ d) (((μH[d] : Measure P) : (a : Set P) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← AffineEquiv.image_symm, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm,
    hausdorffMeasure_homothety_image hd x (_ : 𝕜ˣ).isUnit.ne_zero, Units.val_inv_eq_inv_val,
    Units.val_mk0, nnnorm_inv]

Premises used: nnnorm_inv, Units.val_inv_eq_inv_val, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, MeasureTheory.hausdorffMeasure_homothety_image, AffineEquiv.image_symm, IsUnit.ne_zero, Units.isUnit, Units.val_mk0
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
s : Set ℝ
this :
  ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P) ((fun (x_1 : ℝ) ↦ x_1 • (y -ᵥ x)) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞) ((⇑(AffineMap.lineMap x y) : (a : ℝ) → P) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
s : Set ℝ
suffices :
  ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P) ((fun (x_1 : ℝ) ↦ x_1 • (y -ᵥ x)) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞) ((⇑(AffineMap.lineMap x y) : (a : ℝ) → P) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
suffices μH[1] (IsometryEquiv.vaddConst x '' (· • (y -ᵥ x)) '' s) = nndist x y • μH[1] s by
    simpa only [Set.image_image]
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
s : Set ℝ
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
s : Set ℝ
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rw :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (x_1 : ℝ) ↦ x_1 • (y -ᵥ x)) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := ℝ≥0∞) ‖y -ᵥ x‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  HSMul.hSMul (β := ℝ≥0∞) ‖y -ᵥ x‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) ‖y -ᵥ x‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞)
      (image.{u_5, u_6} (α := E) (⇑(IsometryEquiv.vaddConst x) : (a : E) → P) ((fun (x_1 : ℝ) ↦ x_1 • (y -ᵥ x)) '' s)) =
    HSMul.hSMul (β := ℝ≥0∞) (nndist x y) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image,
    nndist_eq_nnnorm_vsub' E]

Premises used: IsometryEquiv.hausdorffMeasure_image, MeasureTheory.hausdorffMeasure_smul_right_image, nndist_eq_nnnorm_vsub'
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
rw : (algebraMap ℝ≥0 ℝ≥0∞ : (a : ℝ≥0) → ℝ≥0∞) (nndist x y) = edist x y
⊢ ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞) (affineSegment ℝ x y) = edist x y

Tactic:
rw [affineSegment, hausdorffMeasure_lineMap_image, hausdorffMeasure_real, Real.volume_Icc,
    sub_zero, ENNReal.ofReal_one, ← Algebra.algebraMap_eq_smul_one]

Premises used: affineSegment, sub_zero, MeasureTheory.hausdorffMeasure_lineMap_image, Real.volume_Icc, ENNReal.ofReal_one, Algebra.algebraMap_eq_smul_one, MeasureTheory.hausdorffMeasure_real
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
⊢ (algebraMap ℝ≥0 ℝ≥0∞ : (a : ℝ≥0) → ℝ≥0∞) (nndist x y) = edist x y

Tactic:
(edist_nndist _ _).symm

Premises used: ENNReal.ofNNReal, WithTop.some, edist_nndist, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_5
P : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace P
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor E P
inst_5 : BorelSpace P
x y : P
⊢ (algebraMap ℝ≥0 ℝ≥0∞ : (a : ℝ≥0) → ℝ≥0∞) (nndist x y) = edist x y

Tactic:
exact (edist_nndist _ _).symm

Premises used: edist_nndist, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
x y : E
rw : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) (affineSegment ℝ x y) = edist x y
rw₁ rw₂ : edist x y = edist x y
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) (segment ℝ x y) = edist x y

Tactic:
rw [← affineSegment_eq_segment, hausdorffMeasure_affineSegment]

Premises used: affineSegment_eq_segment, MeasureTheory.hausdorffMeasure_affineSegment
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
d : ℝ
s : Set E
hs : 0 ≤ d
⊢ LE.le (α := ℝ≥0∞)
    (((μH[d] : Measure ↥K) : (a : Set ↥K) → ℝ≥0∞) ((⇑K.orthogonalProjection : (a : E) → ↥K) '' s) : ℝ≥0∞)
    (((μH[d] : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa using K.lipschitzWith_orthogonalProjection.hausdorffMeasure_image_le hs s

Premises used: Submodule.lipschitzWith_orthogonalProjection, LipschitzWith.hausdorffMeasure_image_le
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
simp :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
⊢ @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)

Tactic:
simp only [neg_le_self_iff, hr.le, Set.uIoc_of_le]

Premises used: neg_le_self_iff, LT.lt.le, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Prod.instMeasurableSpace)
    (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
rw :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
⊢ @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)

Tactic:
rw [← integrable_norm_iff (by fun_prop)]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
this :
  Eq (α := (a : ℝ × ℝ) → ℝ)
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    fun (x : ℝ × ℝ) ↦ 1
rw :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : ℝ × ℝ) ↦ 1)
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
this :
  Eq (α := (a : ℝ × ℝ) → ℝ)
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    fun (x : ℝ × ℝ) ↦ 1
funProp : enorm (E := ℝ) 1 ≠ ⊤
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : ℝ × ℝ) ↦ 1)
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
suffices :
  Eq (α := (a : ℝ × ℝ) → ℝ)
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    fun (x : ℝ × ℝ) ↦ 1
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)

Tactic:
suffices (fun a => ‖Function.uncurry (fun (x y : ℝ) ↦ cexp (x * y * I)) a‖) = fun _ ↦ 1 by
      rw [this]
      fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h : ∀ (p : ℝ × ℝ), Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) p) = 1
⊢ Eq (α := (a : ℝ × ℝ) → ℝ)
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    fun (x : ℝ × ℝ) ↦ 1

Tactic:
ext p
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
p : ℝ × ℝ
h : Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) (p.1, p.2)) = 1
⊢ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) p) = 1

Tactic:
rw [← Prod.mk.eta (p := p)]

Premises used: Prod.mk.eta
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
p : ℝ × ℝ
h : Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑(x * y) : ℂ) * I)) (p.1, p.2)) = 1
⊢ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) (p.1, p.2)) = 1

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
p : ℝ × ℝ
⊢ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑(x * y) : ℂ) * I)) (p.1, p.2)) = 1

Tactic:
simp only [Function.uncurry_apply_pair, norm_exp_ofReal_mul_I]

Premises used: Complex.norm_exp_ofReal_mul_I, Function.uncurry_apply_pair
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
⊢ @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)

Tactic:
have h_int : Integrable (Function.uncurry fun (x y : ℝ) ↦ cexp (x * y * I))
      ((volume.restrict (Set.uIoc (-r) r)).prod μ) := by
    simp only [neg_le_self_iff, hr.le, Set.uIoc_of_le]
    -- integrable since the function has norm 1 everywhere and the measure is finite
    rw [← integrable_norm_iff (by fun_prop)]
    suffices (fun a => ‖Function.uncurry (fun (x y : ℝ) ↦ cexp (x * y * I)) a‖) = fun _ ↦ 1 by
      rw [this]
      fun_prop
    ext p
    rw [← Prod.mk.eta (p := p)]
    norm_cast
    simp only [Function.uncurry_apply_pair, norm_exp_ofReal_mul_I]
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
⊢ Eq (α := ℂ) (∫ (t : ℝ) in -r..r, charFun μ t) (∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)

Tactic:
simp_rw [charFun_apply_real]

Premises used: MeasureTheory.charFun_apply_real
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
rw rw₁ :
  Eq (α := ℂ) (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
⊢ Eq (α := ℂ) (∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)

Tactic:
rw [intervalIntegral_integral_swap h_int]

Premises used: MeasureTheory.intervalIntegral_integral_swap
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
e_f :
  ∀ (y : ℝ),
    ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
      if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
⊢ Eq (α := ℂ) (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I) ∂μ)

Tactic:
congr with y
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
pos :
  ∀ (hy : y = 0),
    ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
      if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
neg :
  ∀ (hy : ¬y = 0),
    ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
      if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
    if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : y = 0
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
    if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
simp [hy, two_mul]

Premises used: two_mul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
neg :
  ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) = (↑y : ℂ)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
    if r * y = 0 then 2 * (↑r : ℂ) else (↑y⁻¹ : ℂ) * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
simp only [mul_eq_zero, hr.ne', hy, or_self, ↓reduceIte, ofReal_inv]

Premises used: mul_eq_zero, LT.lt.ne', or_self, reduceIte, Complex.ofReal_inv
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ y) (Set.uIcc (-r) r)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
neg :
  ∀
    (h :
      Eq (α := ℂ)
        (∫ (x : ℝ) in -r..r,
          HSMul.hSMul (α := ℝ) (β := ℂ) ((fun (x : ℝ) ↦ y) x)
            (((fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) ∘ fun (x : ℝ) ↦ y * x) x))
        (∫ (x : ℝ) in (fun (x : ℝ) ↦ y * x) (-r)..(fun (x : ℝ) ↦ y * x) r, (fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) x)),
    ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) = (↑y : ℂ)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
neg₁ : ∀ x ∈ Set.uIcc (-r) r, HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ y * x) ((fun (x : ℝ) ↦ y) x) x
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) = (↑y : ℂ)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
have h := intervalIntegral.integral_deriv_smul_comp (E := ℂ) (a := -r) (b := r)
      (f := fun x ↦ y * x) (f' := fun _ ↦ y) (g := fun x ↦ cexp (x * I)) ?_ (by fun_prop)
      (by fun_prop)
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
x : ℝ
hx : x ∈ Set.uIcc (-r) r
neg : HasDerivAt (fun (x : ℝ) ↦ x * y) y x
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ y * x) ((fun (x : ℝ) ↦ y) x) x

Tactic:
simp_rw [mul_comm y]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
x : ℝ
hx : x ∈ Set.uIcc (-r) r
⊢ HasDerivAt (fun (x : ℝ) ↦ x * y) y x

Tactic:
hasDerivAt_mul_const _

Premises used: hasDerivAt_mul_const
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
x : ℝ
hx : x ∈ Set.uIcc (-r) r
⊢ HasDerivAt (fun (x : ℝ) ↦ x * y) y x

Tactic:
exact hasDerivAt_mul_const _

Premises used: hasDerivAt_mul_const
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
h :
  Eq (α := ℂ)
    (∫ (x : ℝ) in -r..r,
      HSMul.hSMul (α := ℝ) (β := ℂ) ((fun (x : ℝ) ↦ y) x)
        (((fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) ∘ fun (x : ℝ) ↦ y * x) x))
    (∫ (x : ℝ) in (fun (x : ℝ) ↦ y * x) (-r)..(fun (x : ℝ) ↦ y * x) r, (fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)) x)
⊢ (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
simp only [Function.comp_apply, ofReal_mul, real_smul, intervalIntegral.integral_const_mul,
      mul_neg] at h

Premises used: Complex.real_smul, Function.comp_apply, Complex.ofReal_mul, mul_neg, intervalIntegral.integral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
h_int :
  @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
    (Measure.prod (Measure.restrict volume (Set.uIoc (-r) r)) μ)
y : ℝ
hy : ¬y = 0
h : (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)
neg :
  ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) =
    (↑y : ℂ)⁻¹ * (↑y : ℂ) * ∫ (x : ℝ) in -r..r, cexp ((↑y : ℂ) * (↑x : ℂ) * I)
⊢ ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) = (↑y : ℂ)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp ((↑x : ℂ) * I)

Tactic:
rw [← h, ← mul_assoc]

Premises used: mul_assoc