awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
inl :
  ∀
    (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∞)
⊢ Eq (α := ℝ≥0∞)
    ((StieltjesFunction.id.measure : (a : Set ℝ) → ℝ≥0∞)
        (parallelepiped (ι := Fin (Module.finrank ℝ ℝ))
          (⇑(stdOrthonormalBasis ℝ ℝ) : (a : Fin (Module.finrank ℝ ℝ)) → ℝ)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have inr : ∀
  (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: rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (hypothesis)
Goal:
this : IsAddLeftInvariant StieltjesFunction.id.measure
⊢ Eq (α := Measure ℝ) volume StieltjesFunction.id.measure
have A : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
| StieltjesFunction.id.measure
have rw : HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) 1
  (addHaarMeasure (Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))))
Tactic: rw [addHaarMeasure_unique StieltjesFunction.id.measure
        (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ Eq (α := Measure ℝ) volume StieltjesFunction.id.measure
have conv_rhs : volume =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) 1
    (addHaarMeasure (Module.Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ ℝ))))
Tactic: conv_rhs =>
    rw [addHaarMeasure_unique StieltjesFunction.id.measure
        (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a r : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)
have rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (a - r) (a + r)) = ofReal (2 * r)
Tactic: rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a r : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Ioo (a - r) (a + r)) = ofReal (2 * r)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)
have rw₁ : ofReal (a + r - (a - r)) = ofReal (2 * r)
Tactic: rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)
have rw₂ : ofReal (a + r - a + r) = ofReal (2 * r)
Tactic: rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)
have rw₃ : ofReal (r + r) = ofReal (2 * r)
Tactic: rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (ball a r) = ofReal (2 * r)
have rw₄ : ofReal (r + r) = ofReal (r + r)
Tactic: rw [ball_eq_Ioo, volume_Ioo, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a r : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)
have rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a - r) (a + r)) = ofReal (2 * r)
Tactic: rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a r : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a - r) (a + r)) = ofReal (2 * r)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)
have rw₁ : ofReal (a + r - (a - r)) = ofReal (2 * r)
Tactic: rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)
have rw₂ : ofReal (a + r - a + r) = ofReal (2 * r)
Tactic: rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)
have rw₃ : ofReal (r + r) = ofReal (2 * r)
Tactic: rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a r) = ofReal (2 * r)
have rw₄ : ofReal (r + r) = ofReal (r + r)
Tactic: rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r
have inl : (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rcases eq_or_ne r ∞ with (rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
inl : (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r
have inr : ∀ (hr : r ≠ ∞), (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r
Tactic: rcases eq_or_ne r ∞ with (rfl | hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
Tactic: rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₃ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [Metric.eball_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a r) = 2 * r
have inr : ∀ (r : ℝ≥0), (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr : (volume : (a : Set ℝ) → ℝ≥0∞) (ball a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (ball a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (ball a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₂ : ofReal ((↑r : ℝ) + (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₃ : ofReal (↑(r + r) : ℝ) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₄ : (↑(r + 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₅ : (↑r : ℝ≥0∞) + (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (eball a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₆ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞)
Tactic: rw [Metric.eball_coe, volume_ball, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r
have inl : (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rcases eq_or_ne r ∞ with (rfl | hr)
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
inl : (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r
have inr : ∀ (hr : r ≠ ∞), (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r
Tactic: rcases eq_or_ne r ∞ with (rfl | hr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
Tactic: rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
Tactic: rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
inl : (volume : (a : Set ℝ) → ℝ≥0∞) univ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₁ : ∞ = HMul.hMul (α := ℝ≥0∞) 2 ∞
inl₂ : ∞ = HAdd.hAdd (α := ℝ≥0∞) ∞ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a ∞) = HMul.hMul (α := ℝ≥0∞) 2 ∞
have inl₃ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [Metric.closedEBall_top, volume_univ, two_mul, _root_.top_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a r) = 2 * r
have inr : ∀ (r : ℝ≥0), (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr : (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
r : ℝ≥0
inr : (volume : (a : Set ℝ) → ℝ≥0∞) (closedBall a (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
inr₁ : ofReal (2 * (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₂ : ofReal ((↑r : ℝ) + (↑r : ℝ)) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₃ : ofReal (↑(r + r) : ℝ) = 2 * (↑r : ℝ≥0∞)
Tactic: rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₄ : (↑(r + 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₅ : (↑r : ℝ≥0∞) + (↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (closedEBall a (↑r : ℝ≥0∞)) = 2 * (↑r : ℝ≥0∞)
have inr₆ : (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞) + (↑r : ℝ≥0∞)
Tactic: rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a b : ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIcc a b) = ofReal |b - a|
have rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (min a b) (max a b)) = ofReal |b - a|
Tactic: rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a b : ℝ
rw : (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (min a b) (max a b)) = ofReal |b - a|
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIcc a b) = ofReal |b - a|
have rw₁ : ofReal (max a b - min a b) = ofReal |b - a|
Tactic: rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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|
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (uIcc a b) = ofReal |b - a|
have rw₂ : ofReal |b - a| = ofReal |b - a|
Tactic: rw [← Icc_min_max, volume_Icc, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici a) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioi a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← measure_congr Ioi_ae_eq_Ici]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
a : ℝ
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iic a) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iio a) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← measure_congr Iio_ae_eq_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
s : Set ℝ
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
have pos : ∀ (hs : Bornology.IsBounded s), (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
Tactic: by_cases hs : Bornology.IsBounded s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
s : Set ℝ
pos : ∀ (hs : Bornology.IsBounded s), (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
have neg : ∀ (hs : ¬Bornology.IsBounded s), (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
Tactic: by_cases hs : Bornology.IsBounded s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
s : Set ℝ
hs : Bornology.IsBounded s
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
have pos : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
  ((volume : (a : Set ℝ) → ℝ≥0∞) (Icc (sInf s) (sSup s)) : ℝ≥0∞)
Tactic: rw [Real.ediam_eq hs, ← volume_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
s : Set ℝ
hs : ¬Bornology.IsBounded s
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) s ≤ ediam s
have neg : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Metric.ediam_of_unbounded hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
p : ℝ → Prop
a : ℝ
h : ∀ᶠ (x : ℝ) in 𝓝 a, p x
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | p x} : ℝ≥0∞)
have 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∞)
Tactic: rcases h.exists_Ioo_subset with ⟨l, u, hx, hs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
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∞) {x : ℝ | p x} : ℝ≥0∞)
have grw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioo l u) : ℝ≥0∞)
Tactic: grw [← hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.Basic (goal)
Goal:
ι : Type u_1
inst : Fintype ι
a b : ι → ℝ
⊢ Eq (α := ℝ≥0∞) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (Icc a b) : ℝ≥0∞)
    (∏ i : ι, ofReal (b i - a i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∏ i : ι, (volume : (a : Set ℝ) → ℝ≥0∞) (Icc (a i) (b i))) (∏ i : ι, ofReal (b i - a i))
Tactic: rw [← pi_univ_Icc, volume_pi_pi]