awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
H :
  Eq (α := Set ℝ)
    (parallelepiped (ι := Fin (Module.finrank ℝ ℝ)) (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ))
    (Icc 0 1)
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

Premises used: StieltjesFunction.id_leftLim, id, zero_add, ENNReal.ofReal_one, tsub_zero, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, sub_neg_eq_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
H :
  Eq (α := Set ℝ)
    (parallelepiped (ι := Fin (Module.finrank ℝ ℝ)) (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ))
    (Icc (-1) 0)
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]

Premises used: StieltjesFunction.id_leftLim, id, zero_add, ENNReal.ofReal_one, tsub_zero, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, sub_neg_eq_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (↑(Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) : Set ℝ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)

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]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
A :
  Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (↑(Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) : Set ℝ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
rw :
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) 1
    (addHaarMeasure (Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))))
| StieltjesFunction.id.measure

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

Premises used: Real, MeasureTheory.Measure.addHaarMeasure_unique, StieltjesFunction.measure, StieltjesFunction.id, OrthonormalBasis.toBasis, Module.Basis.parallelepiped, stdOrthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
A :
  Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (↑(Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) : Set ℝ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
conv_rhs :
  volume =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) 1
      (addHaarMeasure (Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))))
⊢ Eq (α := Measure ℝ) volume StieltjesFunction.id.measure

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

Premises used: Real, MeasureTheory.Measure.addHaarMeasure_unique, StieltjesFunction.measure, StieltjesFunction.id, OrthonormalBasis.toBasis, Module.Basis.parallelepiped, stdOrthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
A :
  Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (↑(Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))) : Set ℝ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ volume =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) 1
      (addHaarMeasure (Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))))

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

Premises used: one_smul, MeasureTheory.MeasureSpace.volume, Module.Basis.addHaar
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [volume_eq_stieltjes_id]

Premises used: Real.volume_eq_stieltjes_id
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (Ico a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Premises used: Real.volume_val
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ico a b) = max (b - a) 0

Tactic:
simp [measureReal_def, ENNReal.toReal_ofReal']

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_ofReal'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
hab : a ≤ b
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ico a b) = b - a

Tactic:
simp [hab]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (Icc a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Premises used: Real.volume_val
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Icc a b) = max (b - a) 0

Tactic:
simp [measureReal_def, ENNReal.toReal_ofReal']

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_ofReal'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
hab : a ≤ b
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Icc a b) = b - a

Tactic:
simp [hab]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Premises used: Real.volume_val
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIoo a b) = ofReal |b - a|

Tactic:
simp [uIoo, volume_Ioo, max_sub_min_eq_abs]

Premises used: max_sub_min_eq_abs, Set.uIoo, Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo a b) = max (b - a) 0

Tactic:
simp [measureReal_def, ENNReal.toReal_ofReal']

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_ofReal'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
hab : a ≤ b
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo a b) = b - a

Tactic:
simp [hab]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (Ioc a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Premises used: Real.volume_val
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIoc a b) = ofReal |b - a|

Tactic:
simp [uIoc, volume_Ioc, max_sub_min_eq_abs]

Premises used: Set.uIoc, max_sub_min_eq_abs, Real.volume_Ioc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b) = max (b - a) 0

Tactic:
simp [measureReal_def, ENNReal.toReal_ofReal']

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_ofReal'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
hab : a ≤ b
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b) = b - a

Tactic:
simp [hab]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
r : ℝ≥0
⊢ (↑r : ℝ≥0∞) = (volume : (a : Set ℝ) → ℝ≥0∞) (Icc 0 (↑r : ℝ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a r : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (a - r) (a + r)) = ofReal (2 * r)
rw₁ : ofReal (a + r - (a - r)) = ofReal (2 * r)
rw₂ : ofReal (a + r - a + r) = ofReal (2 * r)
rw₃ : ofReal (r + r) = ofReal (2 * r)
rw₄ rw₅ : ofReal (r + r) = ofReal (r + r)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)

Tactic:
rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]

Premises used: sub_add, Real.ball_eq_Ioo, add_sub_cancel_left, two_mul, Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a r : ℝ
hr : 0 ≤ r
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (ball a r) = 2 * r

Tactic:
simp [measureReal_def, hr]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a r : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a - r) (a + r)) = ofReal (2 * r)
rw₁ : ofReal (a + r - (a - r)) = ofReal (2 * r)
rw₂ : ofReal (a + r - a + r) = ofReal (2 * r)
rw₃ : ofReal (r + r) = ofReal (2 * r)
rw₄ rw₅ : ofReal (r + r) = ofReal (r + r)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)

Tactic:
rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]

Premises used: sub_add, add_sub_cancel_left, Real.closedBall_eq_Icc, two_mul, Real.volume_Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a r : ℝ
hr : 0 ≤ r
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (closedBall a r) = 2 * r

Tactic:
simp [measureReal_def, hr]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0∞
inl : (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
inr : ∀ (hr : r ≠ ∞), (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r

Tactic:
rcases eq_or_ne r ∞ with (rfl | hr)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
inl₃ inl₄ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞

Tactic:
rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]

Premises used: two_mul, Metric.eball_top, top_add, Real.volume_univ
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ r ≠ ∞

Tactic:
hr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
inr : ∀ (r : ℝ≥0), (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (ball a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₂ : ofReal ((↑r : ℝ) + (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₃ : ofReal (↑(r + r) : ℝ) = 2 * (↑r : ℝ≥0∞)
inr₄ : (↑(r + r) : ℝ≥0∞) = 2 * (↑r : ℝ≥0∞)
inr₅ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = 2 * (↑r : ℝ≥0∞)
inr₆ inr₇ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)

Tactic:
rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

Premises used: NNReal.coe_add, Real.volume_ball, two_mul, ENNReal.coe_add, ENNReal.ofReal_coe_nnreal, Metric.eball_coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0∞
inl : (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
inr : ∀ (hr : r ≠ ∞), (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r

Tactic:
rcases eq_or_ne r ∞ with (rfl | hr)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
inl₃ inl₄ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞

Tactic:
rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]

Premises used: two_mul, top_add, Metric.closedEBall_top, Real.volume_univ
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
inr : ∀ (r : ℝ≥0), (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₂ : ofReal ((↑r : ℝ) + (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₃ : ofReal (↑(r + r) : ℝ) = 2 * (↑r : ℝ≥0∞)
inr₄ : (↑(r + r) : ℝ≥0∞) = 2 * (↑r : ℝ≥0∞)
inr₅ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = 2 * (↑r : ℝ≥0∞)
inr₆ inr₇ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)

Tactic:
rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

Premises used: Real.volume_closedBall, NNReal.coe_add, two_mul, ENNReal.coe_add, ENNReal.ofReal_coe_nnreal, Metric.closedEBall_coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
⊢ NoAtoms (α := ℝ) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
⟨fun _ => volume_singleton⟩

Premises used: Real.volume_singleton, MeasureTheory.NoAtoms.mk
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (min a b) (max a b)) = ofReal |b - a|
rw₁ : ofReal (max a b - min a b) = ofReal |b - a|
rw₂ rw₃ : ofReal |b - a| = ofReal |b - a|
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIcc a b) = ofReal |b - a|

Tactic:
rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]

Premises used: Set.Icc_min_max, Real.volume_Icc, max_sub_min_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a b : ℝ
⊢ Measure.real (m := MeasureSpace.toMeasurableSpace) volume (uIcc a b) = |b - a|

Tactic:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo a (a + (↑n : ℝ))) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
rw : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioi a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← measure_congr Ioi_ae_eq_Ici]

Premises used: MeasureTheory.measure_congr, MeasureTheory.Ioi_ae_eq_Ici
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioi a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (a - (↑n : ℝ)) a) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
rw : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iio a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← measure_congr Iio_ae_eq_Iic]

Premises used: MeasureTheory.measure_congr, MeasureTheory.Iio_ae_eq_Iic
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
a : ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iio a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
x : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (x - 1) (x + 1)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [Real.volume_Ioo, ENNReal.ofReal_lt_top]

Premises used: ENNReal.ofReal_lt_top, Real.volume_Ioo
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
x y : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((Measure.restrict volume (Icc x y) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
x y : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((Measure.restrict volume (Ico x y) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
x y : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((Measure.restrict volume (Ioc x y) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
x y : ℝ
⊢ LT.lt (α := ℝ≥0∞) ((Measure.restrict volume (Ioo x y) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
pos : ∀ (hs : Bornology.IsBounded s), (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
neg : ∀ (hs : ¬Bornology.IsBounded s), (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s

Tactic:
by_cases hs : Bornology.IsBounded s

Premises used: Bornology.IsBounded
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : Bornology.IsBounded s
pos :
  LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Icc (sInf s) (sSup s)) : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s

Tactic:
rw [Real.ediam_eq hs, ← volume_Icc]

Premises used: Real.ediam_eq, Real.volume_Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : Bornology.IsBounded s
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Icc (sInf s) (sSup s)) : ℝ≥0∞)

Tactic:
volume.mono hs.subset_Icc_sInf_sSup

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : Bornology.IsBounded s
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞) (Icc (sInf s) (sSup s)) : ℝ≥0∞)

Tactic:
exact volume.mono hs.subset_Icc_sInf_sSup

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : ¬Bornology.IsBounded s
neg : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s

Tactic:
rw [Metric.ediam_of_unbounded hs]

Premises used: Metric.ediam_of_unbounded
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
rcases :
  ∀ (l u : ℝ) (hx : a ∈ Ioo l u) (hs : Ioo l u ⊆ {x : ℝ | p x}),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | p x} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | p x} : ℝ≥0∞)

Tactic:
rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩

Premises used: Filter.Eventually.exists_Ioo_subset
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x : ℝ | p x}
grw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo l u) : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | p x} : ℝ≥0∞)

Tactic:
grw [← hs]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
l u : ℝ
hx : a ∈ Ioo l u
hs : Ioo l u ⊆ {x : ℝ | p x}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo l u) : ℝ≥0∞)

Tactic:
simpa [-mem_Ioo] using hx.1.trans hx.2

Premises used: Set.mem_Ioo, And.right, And.left, LT.lt.trans
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
rw : Eq (α := ℝ≥0∞) (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a i) (b i))) (∏ i : ι, ofReal (b i - a i))
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
    (∏ i : ι, ofReal (b i - a i) : ℝ≥0∞)

Tactic:
rw [← pi_univ_Icc, volume_pi_pi]

Premises used: MeasureTheory.volume_pi_pi, Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
⊢ Eq (α := ℝ≥0∞) (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a i) (b i))) (∏ i : ι, ofReal (b i - a i))

Tactic:
simp only [Real.volume_Icc]

Premises used: Real.volume_Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Icc a b)) = ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Premises used: Iff.mpr, Real.volume_Icc_pi, ENNReal.toReal_ofReal, ENNReal.toReal_prod, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (a i) (b i)) :
      ℝ≥0∞)
    (∏ i : ι, ofReal (b i - a i) : ℝ≥0∞)

Tactic:
(measure_congr Measure.univ_pi_Ioo_ae_eq_Icc).trans volume_Icc_pi

Premises used: MeasureTheory.measure_congr, MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc, Real.volume_Icc_pi, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal
      (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioo (a i) (b i))) =
    ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ioo, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Premises used: Iff.mpr, Real.volume_pi_Ioo, ENNReal.toReal_ofReal, ENNReal.toReal_prod, sub_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (a i) (b i)) :
      ℝ≥0∞)
    (∏ i : ι, ofReal (b i - a i) : ℝ≥0∞)

Tactic:
(measure_congr Measure.univ_pi_Ioc_ae_eq_Icc).trans volume_Icc_pi

Premises used: MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc, MeasureTheory.measure_congr, Real.volume_Icc_pi, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ ENNReal.toReal
      (((volume : Measure ((i : ι) → ℝ)) : (a : Set ((i : ι) → ℝ)) → ℝ≥0∞)
        (Set.pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ Ioc (a i) (b i))) =
    ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ioc, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Premises used: Iff.mpr, Real.volume_pi_Ioc, ENNReal.toReal_ofReal, ENNReal.toReal_prod, sub_nonneg