awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace E
inst_8 : BorelSpace F
inst_9 : SecondCountableTopology F
inst_10 : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
erw :
  Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
        (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
          (image.{u_2, u_3} (α := E) (⇑(↑(↑f : E ≃ₗ[ℝ] F) : E →ₗ[ℝ] F) : (a : E) → F)
            (_root_.parallelepiped.{u_1, u_2} (ι := ι) (⇑b : (a : ι) → E)))) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
erw₁ :
  Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞) (_root_.parallelepiped.{u_1, u_2} (ι := ι) (⇑b : (a : ι) → E)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((b.addHaar : Measure E) : (a : Set E) → ℝ≥0∞)
        (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F)
          (_root_.parallelepiped.{u_1, u_3} (ι := ι)
            (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑(↑f : E ≃ₗ[ℝ] F) : (a : E) → F)
              (⇑b : (a : ι) → E)))) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have erw₂ : Eq (α := ℝ≥0∞) 1 1
Tactic: erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
⊢ Eq (α := Measure ℝ) (addHaarMeasure Icc01) volume
have h : addHaarMeasure Icc01 =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) ((volume : (a : Set ℝ) → ℝ≥0∞) (↑Icc01 : Set ℝ) : ℝ≥0∞)
    (addHaarMeasure Icc01)
Tactic: convert! (addHaarMeasure_unique volume Icc01).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Eq (α := Measure (ι → ℝ)) (addHaarMeasure (piIcc01 ι) : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))
have h : addHaarMeasure (piIcc01 ι) =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
    (addHaarMeasure (piIcc01 ι))
Tactic: convert! (addHaarMeasure_unique volume (piIcc01 ι)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have by_contra : ∀ (h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have apply : LT.lt (α := ℝ≥0∞) ∞ ∞
Tactic: apply lt_irrefl ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set E) → ℝ≥0∞) s) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) ({u n} + s))
have e_f : Eq (α := ℕ → ℝ≥0∞) (fun (x : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) s) fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) ({u n} + s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (x : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) s) fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) ({u n} + s)
have e_f : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({u n} + s) : ℝ≥0∞)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), {u n} + s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⋃ (i : ℕ), {u i}) + s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
Tactic: rw [← iUnion_add, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ((⋃ (i : ℕ), {u i}) + s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), {u n} + s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
Tactic: rw [← iUnion_add, iUnion_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ∞ ∞
have _ : Eq (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set E) → ℝ≥0∞) s) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) ({u n} + s))
Tactic: calc
    ∞ = ∑' _ : ℕ, μ s := (ENNReal.tsum_const_eq_top_of_ne_zero h).symm
    _ = ∑' n : ℕ, μ ({u n} + s) := by
      congr 1; ext1 n; simp only [image_add_left, measure_preimage_add, singleton_add]
    _ = μ (⋃ n, {u n} + s) := Eq.symm <| measure_iUnion hs fun n => by
      simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's
    _ = μ (range u + s) := by rw [← iUnion_add, iUnion_singleton_eq_range]
    _ < ∞ := (hu.add sb).measure_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
_ : Eq (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set E) → ℝ≥0∞) s) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) ({u n} + s))
⊢ LT.lt (α := ℝ≥0∞) ∞ ∞
have _₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), {u n} + s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞)
Tactic: calc
    ∞ = ∑' _ : ℕ, μ s := (ENNReal.tsum_const_eq_top_of_ne_zero h).symm
    _ = ∑' n : ℕ, μ ({u n} + s) := by
      congr 1; ext1 n; simp only [image_add_left, measure_preimage_add, singleton_add]
    _ = μ (⋃ n, {u n} + s) := Eq.symm <| measure_iUnion hs fun n => by
      simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's
    _ = μ (range u + s) := by rw [← iUnion_add, iUnion_singleton_eq_range]
    _ < ∞ := (hu.add sb).measure_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
| ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
Tactic: rw [← iUnion_inter_closedBall_nat s 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
have conv_lhs : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
  (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
Tactic: conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
Tactic: calc
      μ s ≤ ∑' n : ℕ, μ (s ∩ closedBall 0 n) := by
        conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
        exact measure_iUnion_le _
      _ = 0 := by simp only [H, tsum_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₂ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 (↑n : ℝ))) 0
Tactic: calc
      μ s ≤ ∑' n : ℕ, μ (s ∩ closedBall 0 n) := by
        conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
        exact measure_iUnion_le _
      _ = 0 := by simp only [H, tsum_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices H : ∀ R, μ (s ∩ closedBall 0 R) = 0 by
    rw [← nonpos_iff_eq_zero]
    calc
      μ s ≤ ∑' n : ℕ, μ (s ∩ closedBall 0 n) := by
        conv_lhs => rw [← iUnion_inter_closedBall_nat s 0]
        exact measure_iUnion_le _
      _ = 0 := by simp only [H, tsum_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
R : ℝ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall 0 R) : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s ∩ closedBall 0 R)
Tactic: apply addHaar_eq_zero_of_disjoint_translates_aux μ u
    (isBounded_closedBall.subset inter_subset_right) hu _ (h's.inter measurableSet_closedBall)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s)
h's : MeasurableSet s
R : ℝ
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {u n} + s ∩ closedBall 0 R)
have refine : ∀ (n : ℕ), {u n} + s ∩ closedBall 0 R ≤ {u n} + s
Tactic: refine pairwise_disjoint_mono hs fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (x : E) (hx : x ∉ s), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨x, hx⟩ : ∃ x, x ∉ s := by
    simpa only [Submodule.eq_top_iff', not_exists, Ne, not_forall] using hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (c : ℝ) (cpos : 0 < c) (cone : c < 1), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨c, cpos, cone⟩ : ∃ c : ℝ, 0 < c ∧ c < 1 := ⟨1 / 2, by simp, by norm_num⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have A : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
Tactic: have A : IsBounded (range fun n : ℕ => c ^ n • x) :=
    have : Tendsto (fun n : ℕ => c ^ n • x) atTop (𝓝 ((0 : ℝ) • x)) :=
      (tendsto_pow_atTop_nhds_zero_of_lt_one cpos.le cone).smul_const x
    isBounded_range_of_tendsto _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ {c ^ n • x} + (↑s : Set E))
Tactic: apply addHaar_eq_zero_of_disjoint_translates μ _ A _
    (Submodule.closed_of_finiteDimensional s).measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (n : ℕ) ↦ {c ^ n • x} + (↑s : Set E)) m n
have simp : ∀ ⦃a : E⦄, -(c ^ m • x) + a ∈ s → -(c ^ n • x) + a ∉ s
Tactic: simp only [Function.onFun, image_add_left, singleton_add, disjoint_left, mem_preimage,
    SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
⊢ (c ^ n - c ^ m) • x ∈ s
have h : (c ^ n - c ^ m) • x = -(c ^ m • x) + y - (-(c ^ n • x) + y)
Tactic: convert! s.sub_mem hym hyn using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
⊢ False
have A₁ : (c ^ n - c ^ m) • x ∈ s
Tactic: have A : (c ^ n - c ^ m) • x ∈ s := by
    convert! s.sub_mem hym hyn using 1
    simp only [sub_smul, neg_sub_neg, add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
⊢ False
have H : c ^ n - c ^ m ≠ 0
Tactic: have H : c ^ n - c ^ m ≠ 0 := by
    simpa only [sub_eq_zero, Ne] using (pow_right_strictAnti₀ cpos cone).injective.ne hmn.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ x ∈ s
have h : x = (c ^ n - c ^ m)⁻¹ • (c ^ n - c ^ m) • x
Tactic: convert! s.smul_mem (c ^ n - c ^ m)⁻¹ A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ x = (c ^ n - c ^ m)⁻¹ • (c ^ n - c ^ m) • x
have h : x = ((c ^ n - c ^ m)⁻¹ * (c ^ n - c ^ m)) • x
Tactic: rw [smul_smul, inv_mul_cancel₀ H, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
h : x = ((c ^ n - c ^ m)⁻¹ * (c ^ n - c ^ m)) • x
⊢ x = (c ^ n - c ^ m)⁻¹ • (c ^ n - c ^ m) • x
have h₁ : x = HSMul.hSMul (α := ℝ) 1 x
Tactic: rw [smul_smul, inv_mul_cancel₀ H, one_smul]