awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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 ℝ
⊢ ((μ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∞)
have 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∞)
Tactic: suffices μH[1] (IsometryEquiv.vaddConst x '' (· • (y -ᵥ x)) '' s) = nndist x y • μH[1] s by
    simpa only [Set.image_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
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 ℝ
⊢ ((μ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∞)
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ((μ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∞)
have 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∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image,
    nndist_eq_nnnorm_vsub' E]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image,
    nndist_eq_nnnorm_vsub' E]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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∞)
⊢ ((μ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∞)
have 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∞)
Tactic: rw [IsometryEquiv.hausdorffMeasure_image, hausdorffMeasure_smul_right_image,
    nndist_eq_nnnorm_vsub' E]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ((μH[1] : Measure P) : (a : Set P) → ℝ≥0∞) (affineSegment ℝ x y) = edist x y
have rw : (algebraMap ℝ≥0 ℝ≥0∞ : (a : ℝ≥0) → ℝ≥0∞) (nndist 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
x y : E
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) (segment ℝ x y) = edist x y
have rw : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) (affineSegment ℝ x y) = edist x y
Tactic: rw [← affineSegment_eq_segment, hausdorffMeasure_affineSegment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
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
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) (segment ℝ x y) = edist x y
have rw₁ : edist x y = edist x y
Tactic: rw [← affineSegment_eq_segment, hausdorffMeasure_affineSegment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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)) μ)
have simp : @Integrable ℂ _ _ _ Prod.instMeasurableSpace (Function.uncurry fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I))
  (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
Tactic: simp only [neg_le_self_iff, hr.le, Set.uIoc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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.Ioc (-r) r)) μ)
have 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)) μ)
Tactic: rw [← integrable_norm_iff (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
⊢ @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)) μ)
have rw : @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : ℝ × ℝ) ↦ 1)
  (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (x : ℝ × ℝ) ↦ 1)
    (Measure.prod (Measure.restrict volume (Set.Ioc (-r) r)) μ)
have funProp : enorm (E := ℝ) 1 ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < 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)) μ)
have suffices : Eq (α := (a : ℝ × ℝ) → ℝ)
  (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
  fun (x : ℝ × ℝ) ↦ 1
Tactic: suffices (fun a => ‖Function.uncurry (fun (x y : ℝ) ↦ cexp (x * y * I)) a‖) = fun _ ↦ 1 by
      rw [this]
      fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
⊢ Eq (α := (a : ℝ × ℝ) → ℝ)
    (fun (a : ℝ × ℝ) ↦ Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) a))
    fun (x : ℝ × ℝ) ↦ 1
have h : ∀ (p : ℝ × ℝ), Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑x : ℂ) * (↑y : ℂ) * I)) p) = 1
Tactic: ext p
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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
have h : Norm.norm (E := ℂ) (Function.uncurry (fun (x y : ℝ) ↦ cexp ((↑(x * y) : ℂ) * I)) (p.1, p.2)) = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (hypothesis)
Goal:
μ : Measure ℝ
r : ℝ
inst : IsFiniteMeasure μ
hr : 0 < r
⊢ ∫ (t : ℝ) in -r..r, charFun μ t = 2 * (↑r : ℂ) * (↑(∫ (x : ℝ), sinc (r * x) ∂μ) : ℂ)
have h_int : @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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 (α := ℂ) (∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
    (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
have rw : Eq (α := ℂ) (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
  (∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp ((↑x : ℂ) * (↑y : ℂ) * I) ∂μ)
Tactic: rw [intervalIntegral_integral_swap h_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 (α := ℂ) (∫ (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) ∂μ)
have 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)
Tactic: congr with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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 : ℝ
⊢ ∫ (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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.IntegralCharFun (goal)
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)
⊢ ∫ (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)
have 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)
Tactic: by_cases hy : y = 0