awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
have : Tendsto (fun r : ℝ => μ (toMeasurable μ s ∩ ({x} + r • t)) / μ ({x} + r • t))
    (𝓝[>] 0) (𝓝 1) := by
    apply
      tendsto_addHaar_inter_smul_one_of_density_one_aux μ _ (measurableSet_toMeasurable _ _) _ _
        t ht h't h''t
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' h tendsto_const_nhds
    · refine Eventually.of_forall fun r ↦ ?_
      gcongr
      apply subset_toMeasurable
    · filter_upwards [self_mem_nhdsWithin]
      rintro r -
      apply ENNReal.div_le_of_le_mul
      rw [one_mul]
      exact measure_mono inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
this.congr fun r => ?_

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
refine :
  ∀ (r : ℝ),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
refine this.congr fun r => ?_

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
r : ℝ
e_a :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
r : ℝ
e_a : MeasurableSet ({x} + r • t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)

Tactic:
apply measure_toMeasurable_inter_of_sFinite

Premises used: MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
r : ℝ
e_a : MeasurableSet (α := E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • t))
⊢ MeasurableSet ({x} + r • t)

Tactic:
simp only [image_add_left, singleton_add]

Premises used: Set.image_add_left, Set.singleton_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h''t : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (toMeasurable μ s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
r : ℝ
⊢ MeasurableSet (α := E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • t))

Tactic:
apply (continuous_const_add (-x)).measurable (ht.const_smul₀ r)

Premises used: MeasurableSet.const_smul₀, Continuous.measurable, continuous_const_add, Neg.neg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t' : Set E),
    MeasurableSet t' ∧
      t' ⊆ t ∧
        LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exists_subset_measure_lt_top ht h't.bot_lt

Premises used: MeasureTheory.Measure.exists_subset_measure_lt_top, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t' : Set E) (t'_meas : MeasurableSet t') (t't : t' ⊆ t)
    (t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞))
    (t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty

Tactic:
obtain ⟨t', t'_meas, t't, t'pos, t'top⟩ : ∃ t', MeasurableSet t' ∧ t' ⊆ t ∧ 0 < μ t' ∧ μ t' < ⊤ :=
    exists_subset_measure_lt_top ht h't.bot_lt

Premises used: MeasureTheory.Measure.exists_subset_measure_lt_top, Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
h₁ :
  ∀ (a : ℝ),
    0 <
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t')) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) ({x} + a • t') : ℝ≥0∞) →
      (s ∩ ({x} + a • t)).Nonempty
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty

Tactic:
filter_upwards [(tendsto_order.1
          (tendsto_addHaar_inter_smul_one_of_density_one μ s x h t' t'_meas t'pos.ne' t'top.ne)).1
      0 zero_lt_one]

Premises used: tendsto_order, LT.lt.ne', MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one, zero_lt_one, And.left, Iff.mp, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr

Premises used: ENNReal.zero_div, ENNReal.not_lt_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ (s ∩ ({x} + r • t')) ≠ 0 := fun h' => by
    simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (s ∩ ({x} + r • t')).Nonempty

Tactic:
have : (s ∩ ({x} + r • t')).Nonempty := nonempty_of_measure_ne_zero this
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
this : (s ∩ ({x} + r • t')).Nonempty
apply : {x} + r • t' ⊆ {x} + r • t
⊢ (s ∩ ({x} + r • t)).Nonempty

Tactic:
apply this.mono (inter_subset_inter Subset.rfl _)

Premises used: Set.inter_subset_inter, Set.Nonempty.mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
this : (s ∩ ({x} + r • t')).Nonempty
⊢ {x} + r • t' ⊆ {x} + r • t

Tactic:
add_subset_add Subset.rfl (smul_set_mono t't)

Premises used: Set.smul_set_mono, Set.Subset.rfl, Set.add_subset_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞)
t'top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t' : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ
hr :
  0 <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) ({x} + r • t') : ℝ≥0∞)
this_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t')) : ℝ≥0∞) (0 : ℝ≥0∞)
this : (s ∩ ({x} + r • t')).Nonempty
⊢ {x} + r • t' ⊆ {x} + r • t

Tactic:
exact add_subset_add Subset.rfl (smul_set_mono t't)

Premises used: Set.smul_set_mono, Set.Subset.rfl, Set.add_subset_add
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
⊢ g - f =ᶠ[ae (μ.restrict s)] fun (x : α) ↦ (↑(g x - f x).toNNReal : ℝ)

Tactic:
have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
    hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun (x : α) ↦ (↑(g x - f x).toNNReal : ℝ)
rw :
  (ae (μ.restrict s)).EventuallyEq (β := ENNReal) (fun (y : α) ↦ ENNReal.ofReal ((g - f) y)) fun (a : α) ↦
    (↑(g a - f a).toNNReal : ENNReal)
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ENNReal) (regionBetween f g s) =
    ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs,
    integral_congr_ae h, lintegral_congr_ae,
    lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn.sub, MeasureTheory.integral_congr_ae, MeasureTheory.Integrable.aemeasurable, MeasureTheory.lintegral_congr_ae, Iff.mp, volume_regionBetween_eq_lintegral, MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (μ.restrict s)] g
h : g - f =ᶠ[ae (μ.restrict s)] fun (x : α) ↦ (↑(g x - f x).toNNReal : ℝ)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ENNReal) (fun (y : α) ↦ ENNReal.ofReal ((g - f) y)) fun (y : α) ↦
    ENNReal.ofReal ((g - f) y)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst_1 : SigmaFinite μ
f_int : IntegrableOn f s μ
g_int : IntegrableOn g s μ
hs : MeasurableSet s
hfg : ∀ x ∈ s, f x ≤ g x
⊢ ((μ.prod volume : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ENNReal) (regionBetween f g s) =
    ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)

Tactic:
volume_regionBetween_eq_integral' f_int g_int hs
    ((ae_restrict_iff' hs).mpr (Eventually.of_forall hfg))

Premises used: Iff.mpr, Filter.Eventually.of_forall, volume_regionBetween_eq_integral', MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
⊢ @Integrable E _ _ ℝ MeasureSpace.toMeasurableSpace (⇑f : (a : ℝ) → E) volume

Tactic:
integrable_of_summable_norm_restrict (.of_nonneg_of_le
    (fun n : ℤ => mul_nonneg (norm_nonneg
      (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
        ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_

Premises used: mul_nonneg, ENNReal.toReal_nonneg, Summable.of_nonneg_of_le, MeasureTheory.integrable_of_summable_norm_restrict
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
hf :
  Summable (α := ℝ) fun (n : ℤ) ↦
    Norm.norm (E := C((↑(Icc 0 1) : Type), E))
      (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
refine_1 :
  ∀ (n : ℤ),
    ‖ContinuousMap.restrict
            (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) f‖ *
        Measure.real (m := MeasureSpace.toMeasurableSpace) volume
          (↑{ carrier := Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), isCompact' := ⋯ : Compacts ℝ } : Set ℝ) ≤
      Norm.norm (E := C((↑(Icc 0 1) : Type), E))
        (ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight (↑n : ℝ))))
refine_2 :
  Eq (α := Set ℝ) (⋃ (i : ℤ), (↑{ carrier := Icc (↑i : ℝ) (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1), isCompact' := ⋯ } : Set ℝ))
    univ
⊢ @Integrable E _ _ ℝ MeasureSpace.toMeasurableSpace (⇑f : (a : ℝ) → E) volume

Tactic:
refine integrable_of_summable_norm_restrict (.of_nonneg_of_le
    (fun n : ℤ => mul_nonneg (norm_nonneg
      (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
        ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_

Premises used: mul_nonneg, ENNReal.toReal_nonneg, Summable.of_nonneg_of_le, MeasureTheory.integrable_of_summable_norm_restrict