ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
ι : Type ?u.1963
inst✝ : Fintype ι
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
haveI : IsAddLeftInvariant StieltjesFunction.id.measure :=
  ⟨fun a =>
    Eq.symm <|
      Real.measure_ext_Ioo_rat fun p q => by
        simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo,
          sub_sub_sub_cancel_right, StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim,
          StieltjesFunction.id_apply, id.def, preimage_const_add_Ioo]⟩
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
have A : StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1 := by
  change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1
  rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
    simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id.def, tsub_zero,
      StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = 1 • addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ)))
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = StieltjesFunction.measure StieltjesFunction.id
conv_rhs =>
  rw [addHaarMeasure_unique StieltjesFunction.id.measure
      (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
no goals
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
A :
  ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
⊢ volume = 1 • addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ)))
simp only [volume, Basis.addHaar, one_smul]
no goals
ι : Type ?u.1963
inst✝ : Fintype ι
a : ℝ
p q : ℚ
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (Ioo ↑p ↑q) =
    ↑↑(Measure.map (fun x => a + x) (StieltjesFunction.measure StieltjesFunction.id)) (Ioo ↑p ↑q)
simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo,
  sub_sub_sub_cancel_right, StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim,
  StieltjesFunction.id_apply, id.def, preimage_const_add_Ioo]
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (parallelepiped ↑(stdOrthonormalBasis ℝ ℝ)) = 1
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id)
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) =
    1
change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1
no goals
ι : Type ?u.1963
inst✝ : Fintype ι
this : IsAddLeftInvariant (StieltjesFunction.measure StieltjesFunction.id)
⊢ ↑↑(StieltjesFunction.measure StieltjesFunction.id) (parallelepiped ↑(stdOrthonormalBasis ℝ ℝ)) = 1
rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
  simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id.def, tsub_zero,
    StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]