-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_eq_zero_of_disjoint_translates_aux {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : Measure E)
    [IsAddHaarMeasure μ] {s : Set E} (u : ℕ → E) (sb : IsBounded s) (hu : IsBounded (range u))
    (hs : Pairwise (Disjoint on fun n => {u n} + s)) (h's : MeasurableSet s) : μ s = 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ False

Tactic:
apply lt_irrefl ∞

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ ⊤ < ⊤

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
n : ℕ
⊢ MeasurableSet ({u n} + s)

Tactic:
simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ μ (⋃ n, {u n} + s) = μ (range u + s)

Tactic:
rw [← iUnion_add, iUnion_singleton_eq_range]

Result:
no goals

Proof state:
case e_f.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
n : ℕ
⊢ μ s = μ ({u n} + s)

Tactic:
simp only [image_add_left, measure_preimage_add, singleton_add]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
⊢ μ s = 0

Tactic:
by_contra h

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ False

Proof state:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ (fun x => μ s) = fun n => μ ({u n} + s)

Tactic:
ext1 n

Result:
case e_f.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
n : ℕ
⊢ μ s = μ ({u n} + s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ ∑' (x : ℕ), μ s = ∑' (n : ℕ), μ ({u n} + s)

Tactic:
congr 1

Result:
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ s = 0
⊢ (fun x => μ s) = fun n => μ ({u n} + s)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
sb : Bornology.IsBounded s
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬μ 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

Result:
no goals