awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ p x

Tactic:
False.elim (hx ⟨xs, Hx⟩)

Premises used: False.elim, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Goal:
μ : Measure ℝ
inst : NoAtoms μ
s : Set ℝ
p : ℝ → Prop
h : ∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Ioo a b → p x
T : (↑s : Type) × (↑s : Type) → Set ℝ := fun (p : (↑s : Type) × (↑s : Type)) ↦ Ioo (↑p.1 : ℝ) (↑p.2 : ℝ)
u : Set ℝ := ⋃ (i : (↑s : Type) × (↑s : Type)), T i
hfinite : (s \ u).Finite
A : Set ((↑s : Type) × (↑s : Type))
A_count : A.Countable
hA : Eq (α := Set ℝ) (⋃ i ∈ A, T i) (⋃ (i : (↑s : Type) × (↑s : Type)), T i)
M : ∀ᵐ (x : ℝ) ∂μ, x ∉ s \ u
M' : ∀ᵐ (x : ℝ) ∂μ, ∀ i ∈ A, x ∈ s ∩ T i → p x
x : ℝ
hx : x ∉ s \ u
h'x : ∀ i ∈ A, x ∈ s ∩ T i → p x
xs : x ∈ s
Hx : x ∉ ⋃ (i : (↑s : Type) × (↑s : Type)), T i
⊢ p x

Tactic:
exact False.elim (hx ⟨xs, Hx⟩)

Premises used: False.elim, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
a : ℂ
⊢ (measurableEquivPi : (a : ℂ) → Fin 2 → ℝ) a = ![a.re, a.im]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
p : Fin 2 → ℝ
⊢ (measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) p = (↑(p 0) : ℂ) + (↑(p 1) : ℂ) * I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
a : ℂ
⊢ (measurableEquivRealProd : (a : ℂ) → ℝ × ℝ) a = (a.re, a.im)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
p : ℝ × ℝ
⊢ (measurableEquivRealProd.symm : (a : ℝ × ℝ) → ℂ) p = { re := p.1, im := p.2 : ℂ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
⊢ MeasurePreserving (α := ℂ) (β := Fin 2 → ℝ) (⇑measurableEquivPi.symm.symm : (a : ℂ) → Fin 2 → ℝ)
    (Measure.map (α := Fin 2 → ℝ) (⇑measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) volume) volume

Tactic:
(measurableEquivPi.symm.measurable.measurePreserving volume).symm

Premises used: MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.symm, MeasureTheory.MeasureSpace.volume, Complex.measurableEquivPi, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
h :
  Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1) volume
    (Measure.map (α := Fin 2 → ℝ) (⇑measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) volume)
⊢ MeasurePreserving (α := ℂ) (β := Fin 2 → ℝ) (⇑measurableEquivPi : (a : ℂ) → Fin 2 → ℝ) volume volume

Tactic:
convert! (measurableEquivPi.symm.measurable.measurePreserving volume).symm

Premises used: MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.symm, MeasureTheory.MeasureSpace.volume, Complex.measurableEquivPi, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
h :
  Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1)
    (Basis.map (Pi.basisFun ℝ (Fin 2))
        (↑(ContinuousLinearEquiv.symm basisOneI.equivFun.toContinuousLinearEquiv) : (Fin 2 → ℝ) ≃ₗ[ℝ] ℂ)).addHaar
    volume
⊢ Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1) volume
    (Measure.map (α := Fin 2 → ℝ) (⇑measurableEquivPi.symm : (a : Fin 2 → ℝ) → ℂ) volume)

Tactic:
rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
    measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
    ContinuousLinearEquiv.coe_symm_toHomeomorph, Basis.map_addHaar, eq_comm]

Premises used: Module.Basis.parallelepiped_basisFun, eq_comm, ContinuousLinearEquiv.coe_symm_toHomeomorph, MeasureTheory.addHaarMeasure_eq_volume_pi, Complex.measurableEquivPi, Module.Basis.addHaar, Homeomorph.toMeasurableEquiv_symm_coe, Module.Basis.map_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
⊢ Eq (α := autoParam (Measure ℂ) MeasurePreserving._auto_1)
    (Basis.map (Pi.basisFun ℝ (Fin 2))
        (↑(ContinuousLinearEquiv.symm basisOneI.equivFun.toContinuousLinearEquiv) : (Fin 2 → ℝ) ≃ₗ[ℝ] ℂ)).addHaar
    volume

Tactic:
(Basis.addHaar_eq_iff _ _).mpr Complex.orthonormalBasisOneI.volume_parallelepiped

Premises used: Iff.mpr, OrthonormalBasis.volume_parallelepiped, Complex.orthonormalBasisOneI, Module.Basis.addHaar_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Goal:
⊢ MeasurePreserving (α := ℂ) (β := ℝ × ℝ) (⇑measurableEquivRealProd : (a : ℂ) → ℝ × ℝ) volume volume

Tactic:
(volume_preserving_finTwoArrow ℝ).comp volume_preserving_equiv_pi

Premises used: Eq.mpr, Real, Fin.cons, Fin.induction.go, Fin.induction, Complex.volume_preserving_equiv_pi, Fin.cases, MeasureTheory.MeasurePreserving.comp, MeasureTheory.volume_preserving_finTwoArrow, Matrix.vecCons
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
simp_rw : Set.Nonempty (α := ℝ) (Ioo 0 1)
simp_rw₁ : LT.lt (α := ℝ) 0 1
⊢ Set.Nonempty (α := ℝ) (interior (Icc 0 1))

Tactic:
simp_rw [interior_Icc, nonempty_Ioo, zero_lt_one]

Premises used: interior_Icc, Set.nonempty_Ioo, zero_lt_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Finite ι
⊢ Set.Nonempty.{u_1} (α := ι → ℝ) (interior (Set.pi (α := fun (a : ι) ↦ ℝ) univ fun (x : ι) ↦ Icc 0 1))

Tactic:
simp only [interior_pi_set, Set.toFinite, interior_Icc, univ_pi_nonempty_iff, nonempty_Ioo,
      imp_true_iff, zero_lt_one]

Premises used: interior_Icc, Set.univ_pi_nonempty_iff, Set.nonempty_Ioo, imp_true_iff, zero_lt_one, Set.toFinite, interior_pi_set
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = (↑(PositiveCompacts.piIcc01 ι) : Set (ι → ℝ))

Tactic:
Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)

Premises used: Set.uIcc_of_le, Eq.symm, Eq.trans, Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
refine_1 : (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = uIcc (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1
refine_2 : LE.le.{u_1} (α := ι → ℝ) (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = (↑(PositiveCompacts.piIcc01 ι) : Set (ι → ℝ))

Tactic:
refine Eq.trans ?_ ((uIcc_of_le ?_).trans (Set.pi_univ_Icc _ _).symm)

Premises used: Set.uIcc_of_le, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Eq.{u_1 + 1} (α := Set ((j : ι) → ℝ)) (_root_.parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (1 i))
    (uIcc 0 1)

Tactic:
parallelepiped_single (ι := ι) 1

Premises used: OfNat.ofNat, parallelepiped_single
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = uIcc (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1

Tactic:
convert! parallelepiped_single (ι := ι) 1

Premises used: OfNat.ofNat, parallelepiped_single
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ (↑(parallelepiped (Pi.basisFun ℝ ι)) : Set (ι → ℝ)) = uIcc (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1

Tactic:
classical convert! parallelepiped_single (ι := ι) 1
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ LE.le.{u_1} (α := ι → ℝ) (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ LE.le.{u_1} (α := ι → ℝ) (fun (i : ι) ↦ 0) fun (i : ι) ↦ 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
rw : b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)

Tactic:
rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]

Premises used: Module.Basis.parallelepiped_basisFun, Module.Basis.parallelepiped_map
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
e_b :
  ∀ (x : ι),
    Eq.{u_2 + 1} (α := E) ((b : (a : ι) → E) x : E) ((Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm : (a : ι) → E) x : E)
⊢ b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
x : ι
⊢ Eq.{u_2 + 1} (α := E) ((b : (a : ι) → E) x : E) ((Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm : (a : ι) → E) x : E)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
rw : b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (parallelepiped (Pi.basisFun ℝ ι))
rw₁ rw₂ rw₃ : b.parallelepiped = (Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm).parallelepiped
e_b :
  ∀ (x : ι),
    Eq.{u_2 + 1} (α := E) ((b : (a : ι) → E) x : E) ((Basis.map (Pi.basisFun ℝ ι) b.equivFun.symm : (a : ι) → E) x : E)
⊢ b.parallelepiped = PositiveCompacts.map (⇑b.equivFun.symm : (a : ι → ℝ) → E) ⋯ ⋯ (PositiveCompacts.piIcc01 ι)

Tactic:
classical
  rw [← Basis.parallelepiped_basisFun, ← Basis.parallelepiped_map]
  congr with x
  simp [Pi.single_apply]

Premises used: Module.Basis.parallelepiped_basisFun, Pi.single_apply, Module.Basis.parallelepiped_map
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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
rw :
  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∞)
⊢ Eq (α := Measure F) (Measure.map (⇑f : (a : E) → F) b.addHaar) (b.map (↑f : E ≃ₗ[ℝ] F)).addHaar

Tactic:
rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable
    (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map]

Premises used: Module.Basis.coe_map, MeasureTheory.Measure.map_apply, eq_comm, Module.Basis.addHaar_eq_iff, Module.Basis.coe_parallelepiped, ContinuousLinearEquiv.continuous, Continuous.measurable, TopologicalSpace.PositiveCompacts.isCompact, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
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∞)
erw₂ erw₃ : Eq (α := ℝ≥0∞) 1 1
⊢ 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∞)

Tactic:
erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]

Premises used: ContinuousLinearEquiv.toLinearEquiv, image_parallelepiped, LinearEquiv.toEquiv, Equiv.preimage_image, Module.Basis.addHaar_self
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
⊢ HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) ((volume : (a : Set ℝ) → ℝ≥0∞) (↑Icc01 : Set ℝ) : ℝ≥0∞)
      (addHaarMeasure Icc01) =
    volume

Tactic:
(addHaarMeasure_unique volume Icc01).symm

Premises used: MeasureTheory.Measure.addHaarMeasure_unique, MeasureTheory.MeasureSpace.volume, TopologicalSpace.PositiveCompacts.Icc01, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
h :
  addHaarMeasure Icc01 =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) ((volume : (a : Set ℝ) → ℝ≥0∞) (↑Icc01 : Set ℝ) : ℝ≥0∞)
      (addHaarMeasure Icc01)
⊢ Eq (α := Measure ℝ) (addHaarMeasure Icc01) volume

Tactic:
convert! (addHaarMeasure_unique volume Icc01).symm

Premises used: MeasureTheory.Measure.addHaarMeasure_unique, MeasureTheory.MeasureSpace.volume, TopologicalSpace.PositiveCompacts.Icc01, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
⊢ addHaarMeasure Icc01 =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure ℝ) ((volume : (a : Set ℝ) → ℝ≥0∞) (↑Icc01 : Set ℝ) : ℝ≥0∞)
      (addHaarMeasure Icc01)

Tactic:
simp [Icc01]

Premises used: TopologicalSpace.PositiveCompacts.Icc01
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (addHaarMeasure (piIcc01 ι)) =
    volume

Tactic:
(addHaarMeasure_unique volume (piIcc01 ι)).symm

Premises used: MeasureTheory.Measure.addHaarMeasure_unique, MeasureTheory.MeasureSpace.volume, Eq.symm, TopologicalSpace.PositiveCompacts.piIcc01
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
h :
  addHaarMeasure (piIcc01 ι) =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (addHaarMeasure (piIcc01 ι))
⊢ Eq (α := Measure (ι → ℝ)) (addHaarMeasure (piIcc01 ι) : Measure (ι → ℝ)) (volume : Measure (ι → ℝ))

Tactic:
convert! (addHaarMeasure_unique volume (piIcc01 ι)).symm

Premises used: MeasureTheory.Measure.addHaarMeasure_unique, MeasureTheory.MeasureSpace.volume, Eq.symm, TopologicalSpace.PositiveCompacts.piIcc01
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (addHaarMeasure (piIcc01 ι))

Tactic:
simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk,
    Compacts.coe_mk, Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]

Premises used: MeasureTheory.volume_pi_pi, sub_zero, TopologicalSpace.Compacts.coe_mk, Real.volume_Icc, ENNReal.ofReal_one, one_smul, TopologicalSpace.PositiveCompacts.coe_mk, Finset.prod_const_one, Set.Icc, OfNat.ofNat, TopologicalSpace.PositiveCompacts.piIcc01
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Fintype ι
⊢ IsAddHaarMeasure.{u_1} (G := ι → ℝ) volume

Tactic:
inferInstance

Premises used: inferInstance
-- 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
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
by_contra : ∀ (h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra h
-- 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
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∞)
apply : LT.lt (α := ℝ≥0∞) ∞ ∞
⊢ False

Tactic:
apply lt_irrefl ∞

Premises used: lt_irrefl, Top.top
-- 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
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)

Tactic:
(ENNReal.tsum_const_eq_top_of_ne_zero h).symm

Premises used: ENNReal.tsum_const_eq_top_of_ne_zero, Eq.symm
-- 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
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∞)
e_f : Eq (α := ℕ → ℝ≥0∞) (fun (x : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) s) fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) ({u n} + s)
⊢ Eq (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set E) → ℝ≥0∞) s) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) ({u n} + s))

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
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∞)
e_f : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({u n} + s) : ℝ≥0∞)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (x : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) s) fun (n : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) ({u n} + s)

Tactic:
ext1 n
-- 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
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∞)
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ({u n} + s) : ℝ≥0∞)

Tactic:
simp only [image_add_left, measure_preimage_add, singleton_add]

Premises used: Set.image_add_left, Set.singleton_add, MeasureTheory.measure_preimage_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
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∞)
n : ℕ
⊢ MeasurableSet ({u n} + s)

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

Premises used: measurable_id, Measurable.const_add, 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
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (range u + 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∞)

Tactic:
rw [← iUnion_add, iUnion_singleton_eq_range]

Premises used: Set.iUnion_add, Set.iUnion_singleton_eq_range
-- 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
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∞) ((μ : (a : Set E) → ℝ≥0∞) (range u + s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(hu.add sb).measure_lt_top

Premises used: Bornology.IsBounded.measure_lt_top, Bornology.IsBounded.add