-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_eq_stieltjes_id : (volume : Measure ℝ) = StieltjesFunction.id.measure

Proof state:
⊢ volume = StieltjesFunction.id.measure

Tactic:
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, preimage_const_add_Ioo]⟩

Result:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ volume = StieltjesFunction.id.measure

Proof state:
a : ℝ
p q : ℚ
⊢ StieltjesFunction.id.measure (Ioo ↑p ↑q) = (Measure.map (fun x => a + x) StieltjesFunction.id.measure) (Ioo ↑p ↑q)

Tactic:
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, preimage_const_add_Ioo]

Result:
no goals

Proof state:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1

Tactic:
change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1

Result:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1

Proof state:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1
⊢ volume = 1 • addHaarMeasure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped

Tactic:
simp only [volume, Basis.addHaar, one_smul]

Result:
no goals

Proof state:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1
⊢ volume = StieltjesFunction.id.measure

Tactic:
conv_rhs =>
  rw [addHaarMeasure_unique StieltjesFunction.id.measure
      (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]

Result:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1
⊢ volume = 1 • addHaarMeasure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped

Proof state:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ StieltjesFunction.id.measure (parallelepiped ⇑(stdOrthonormalBasis ℝ ℝ)) = 1

Tactic:
rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
  simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
    StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

Result:
no goals

Proof state:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
⊢ volume = StieltjesFunction.id.measure

Tactic:
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, tsub_zero,
      StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

Result:
this : StieltjesFunction.id.measure.IsAddLeftInvariant
A : StieltjesFunction.id.measure ↑(stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1
⊢ volume = StieltjesFunction.id.measure