awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
h :
  ∀ (x : (i : ι) → α i),
    x ∈ (↑I : Set ι).pi (α := α) t ↔
      Membership.mem (γ := Set ((i : ι) → α i))
        ((↑I : Set ι).restrict (π := α) ⁻¹'
          Set.pi (α := fun (a : (↑(↑I : Set ι) : Type u_2)) ↦ α (↑a : ι)) univ fun (i : (↑(↑I : Set ι) : Type u_2)) ↦
            t (↑i : ι))
        x
⊢ (↑I : Set ι).pi (α := α) t =
    (↑I : Set ι).restrict (π := α) ⁻¹'
      Set.pi (α := fun (a : (↑(↑I : Set ι) : Type u_2)) ↦ α (↑a : ι)) univ fun (i : (↑(↑I : Set ι) : Type u_2)) ↦
        t (↑i : ι)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ (↑I : Set ι).pi (α := α) t ↔
    Membership.mem (γ := Set ((i : ι) → α i))
      ((↑I : Set ι).restrict (π := α) ⁻¹'
        Set.pi (α := fun (a : (↑(↑I : Set ι) : Type u_2)) ↦ α (↑a : ι)) univ fun (i : (↑(↑I : Set ι) : Type u_2)) ↦
          t (↑i : ι))
      x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
⊢ ∃ (I_1 : Set ι) (t_1 : Set ((a : (↑I_1 : Type u_2)) → α (↑a : ι))),
    I_1.Countable ∧ (↑I : Set ι).pi (α := α) t = I_1.restrict (π := α) ⁻¹' t_1

Tactic:
exact ⟨I, univ.pi (fun i ↦ t i), I.countable_toSet, by ext; simp⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Set ι
t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))
hI : I.Countable
⊢ (I.restrict (π := α) ⁻¹' t)ᶜ = I.restrict (π := α) ⁻¹' tᶜ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Set ι
t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))
hI : I.Countable
⊢ ∃ (I_1 : Set ι) (t_1 : Set ((a : (↑I_1 : Type u_2)) → α (↑a : ι))),
    I_1.Countable ∧ (I.restrict (π := α) ⁻¹' t)ᶜ = I_1.restrict (π := α) ⁻¹' t_1

Tactic:
exact ⟨I, tᶜ, hI, by simp⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ), ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ f i = I.restrict (π := α) ⁻¹' t
refine_3 :
  ∀ (I : (i : ℕ) → Set ι) (t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))) (hI : ∀ (i : ℕ), (I i).Countable)
    (hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i),
    ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))),
      I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t

Tactic:
choose! I t hI hf using hf
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t

Tactic:
⟨⋃ n, I n, ⋃ n, (⋃ k, I k).restrict '' (f n), countable_iUnion hI, ?_⟩

Premises used: Set.countable_iUnion, And.intro, Exists.intro, Set.image, Set.restrict, Set.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
refine_3 :
  Eq (α := Set ((i : ι) → α i)) (⋃ (i : ℕ), f i)
    (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
      (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
⊢ ∃ (I : Set ι) (t : Set ((a : (↑I : Type u_2)) → α (↑a : ι))), I.Countable ∧ ⋃ (i : ℕ), f i = I.restrict (π := α) ⁻¹' t

Tactic:
refine ⟨⋃ n, I n, ⋃ n, (⋃ k, I k).restrict '' (f n), countable_iUnion hI, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
refine_3 :
  ∀ (x : (a : ι) → α a),
    Membership.mem (γ := Set ((a : ι) → α a)) (⋃ (i : ℕ), f i) x ↔
      Membership.mem (γ := Set ((a : ι) → α a))
        (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
          (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
        x
⊢ Eq (α := Set ((i : ι) → α i)) (⋃ (i : ℕ), f i)
    (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
      (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
refine_3 :
  (∃ (i : ℕ), (I i).restrict (π := α) x ∈ t i) ↔
    ∃ (i : ℕ) (x_1 : (a : ι) → α a),
      (I i).restrict (π := α) x_1 ∈ t i ∧
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
          (restrict (π := α) (⋃ (n : ℕ), I n) x)
⊢ Membership.mem (γ := Set ((a : ι) → α a)) (⋃ (i : ℕ), f i) x ↔
    Membership.mem (γ := Set ((a : ι) → α a))
      (preimage (β := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n))
        (⋃ (n : ℕ), restrict (π := α) (⋃ (k : ℕ), I k) '' f n))
      x

Tactic:
simp only [hf, mem_iUnion, mem_preimage, preimage_iUnion, mem_image]

Premises used: Set.mem_iUnion, Set.mem_image, Set.preimage_iUnion, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
⊢ (∃ (i : ℕ), (I i).restrict (π := α) x ∈ t i) ↔
    ∃ (i : ℕ) (x_1 : (a : ι) → α a),
      (I i).restrict (π := α) x_1 ∈ t i ∧
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
          (restrict (π := α) (⋃ (n : ℕ), I n) x)

Tactic:
⟨fun ⟨i, hi⟩ ↦ ⟨i, x, hi, rfl⟩, fun ⟨n, x', hn, hx⟩ ↦ ⟨n, ?_⟩⟩

Premises used: _private.0.MeasureTheory.MeasurableSet.eq_preimage_restrict_countable.match_2, Membership.mem, Exists, And, And.intro, Iff.intro, Exists.intro, Set.restrict, _private.0.MeasureTheory.MeasurableSet.eq_preimage_restrict_countable.match_1, Eq, Set.iUnion, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
refine_3 :
  (∃ (i : ℕ) (x_1 : (a : ι) → α a),
      (I i).restrict (π := α) x_1 ∈ t i ∧
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
          (restrict (π := α) (⋃ (n : ℕ), I n) x)) →
    ∀ (n : ℕ) (x' : (a : ι) → α a) (hn : (I n).restrict (π := α) x' ∈ t n)
      (hx :
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
          (restrict (π := α) (⋃ (n : ℕ), I n) x)),
      (I n).restrict (π := α) x ∈ t n
⊢ (∃ (i : ℕ), (I i).restrict (π := α) x ∈ t i) ↔
    ∃ (i : ℕ) (x_1 : (a : ι) → α a),
      (I i).restrict (π := α) x_1 ∈ t i ∧
        Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
          (restrict (π := α) (⋃ (n : ℕ), I n) x)

Tactic:
refine ⟨fun ⟨i, hi⟩ ↦ ⟨i, x, hi, rfl⟩, fun ⟨n, x', hn, hx⟩ ↦ ⟨n, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
h :
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
n : ℕ
x' : (a : ι) → α a
hn : (I n).restrict (π := α) x' ∈ t n
hx :
  Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
    (restrict (π := α) (⋃ (n : ℕ), I n) x)
⊢ ∀ (x : (i : ι) → α i),
    (I n).restrict (π := α) x =
      (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
          (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
            α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
        (restrict (π := α) (⋃ (k : ℕ), I k) x)

Tactic:
have (x : Π i, α i) : (I n).restrict x =
      (fun (x : Π (i : ⋃ k, I k), α i) (i : I n) ↦ x ⟨i.1, subset_iUnion I n i.2⟩)
      ((⋃ k, I k).restrict x) := rfl
-- Module: Mathlib.MeasureTheory.Constructions.Cylinders
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
f : ℕ → Set ((a : ι) → α a)
df : Pairwise (Disjoint on f)
mf : ∀ (i : ℕ), MeasurableSet (f i)
I : (i : ℕ) → Set ι
t : (i : ℕ) → Set ((a : (↑(I i) : Type u_2)) → α (↑a : ι))
hI : ∀ (i : ℕ), (I i).Countable
hf : ∀ (i : ℕ), f i = (I i).restrict (π := α) ⁻¹' t i
x : (a : ι) → α a
h :
  ∃ (i : ℕ) (x_1 : (a : ι) → α a),
    (I i).restrict (π := α) x_1 ∈ t i ∧
      Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x_1)
        (restrict (π := α) (⋃ (n : ℕ), I n) x)
n : ℕ
x' : (a : ι) → α a
hn : (I n).restrict (π := α) x' ∈ t n
hx :
  Eq (α := (a : (↑(⋃ (n : ℕ), I n) : Type u_2)) → α (↑a : ι)) (restrict (π := α) (⋃ (n : ℕ), I n) x')
    (restrict (π := α) (⋃ (n : ℕ), I n) x)
this :
  ∀ (x : (i : ι) → α i),
    (I n).restrict (π := α) x =
      (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
          (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
            α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
        (restrict (π := α) (⋃ (k : ℕ), I k) x)
refine_3 :
  (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
        (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
          α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
      (restrict (π := α) (⋃ (k : ℕ), I k) x) ∈
    t n
refine_3₁ :
  (fun (x : (i : (↑(⋃ (k : ℕ), I k) : Type u_2)) → α (↑i : ι)) (i : (↑(I n) : Type u_2)) ↦
        (x (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) :
          α (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Set ι) (⋃ (k : ℕ), I k) x) (↑i : ι) ⋯) : ι)))
      (restrict (π := α) (⋃ (n : ℕ), I n) x') ∈
    t n
refine_3₂ refine_3₃ refine_3₄ refine_3₅ : (I n).restrict (π := α) x' ∈ t n
⊢ (I n).restrict (π := α) x ∈ t n

Tactic:
rwa [this, ← hx, ← this]
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
s : Set (↑(sphere 0 1) : Type u_1)
r : (↑(Ioi 0) : Type)
rw :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        ((fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦
            (↑((Homeomorph.symm (homeomorphUnitSphereProd E) :
                    (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
                  x) :
              E)) ''
          s ×ˢ Iio r) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        ((fun (x : (↑(sphere 0 1) : Type u_1) × { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }) ↦
            (↑x.2 : ℝ) • (↑x.1 : E)) ''
          s ×ˢ Iio r) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (image (α := (↑{0}ᶜ : Type u_1)) (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
          ((⇑(homeomorphUnitSphereProd E) :
              (a : (↑{0}ᶜ : Type u_1)) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
            s ×ˢ Iio r)) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (Ioo 0 (↑r : ℝ) • Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s) :
      ℝ≥0∞)

Tactic:
rw [← image2_smul, image2_image_right, ← Homeomorph.image_symm, image_image,
    ← image_subtype_val_Ioi_Iio, image2_image_left, image2_swap, ← image_prod]

Premises used: Set.image_image, Set.image2_image_right, Set.image_prod, Set.image2_image_left, Homeomorph.image_symm, Set.image2_smul, Set.image2_swap, Set.image_subtype_val_Ioi_Iio
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
s : Set (↑(sphere 0 1) : Type u_1)
r : (↑(Ioi 0) : Type)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        ((fun (x : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ↦
            (↑((Homeomorph.symm (homeomorphUnitSphereProd E) :
                    (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1))
                  x) :
              E)) ''
          s ×ˢ Iio r) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        ((fun (x : (↑(sphere 0 1) : Type u_1) × { x : ℝ // Membership.mem (γ := Set ℝ) (Ioi 0) x }) ↦
            (↑x.2 : ℝ) • (↑x.1 : E)) ''
          s ×ˢ Iio r) :
      ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 (HMul.hMul (α := ℝ) 1 1) \ closedBall 0 (HMul.hMul (α := ℝ) 0 1)) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)
ha : LE.le (α := ℝ) 0 0
hr : LT.lt (α := ℝ) 0 1
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)

Tactic:
rw [μ.toSphere_apply' .univ, image_univ, Subtype.range_coe, Ioo_smul_sphere_zero]

Premises used: Set.image_univ, Ioo_smul_sphere_zero, Subtype.range_coe, MeasureTheory.Measure.toSphere_apply', MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (ball 0 (HMul.hMul (α := ℝ) 1 1) \ closedBall 0 (HMul.hMul (α := ℝ) 0 1)) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
⊢ LE.le (α := ℝ) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
⊢ Nontrivial E

Tactic:
nontriviality E using not_nonempty_iff_eq_empty

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
        ℝ≥0∞) ≠
    0
⊢ Ne (α := ℝ≥0∞)
    (((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) U : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [μ.toSphere_apply' hUo.measurableSet]

Premises used: IsOpen.measurableSet, MeasureTheory.Measure.toSphere_apply'
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ Ne (α := ℝ≥0∞) (↑(dim E) : ℝ≥0∞) 0

Tactic:
simp [Module.finrank_pos.ne']

Premises used: LT.lt.ne', Module.finrank_pos
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
apply :
  Ne (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
        ℝ≥0∞) ≠
    0

Tactic:
apply mul_ne_zero (by simp [Module.finrank_pos.ne'])

Premises used: mul_ne_zero
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ 0 ∉ Ioo 0 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)).Nonempty

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsOpenPosMeasure
h : Nontrivial E
U : Set (↑(sphere 0 1) : Type u_1)
hUo : IsOpen U
hU : U.Nonempty
⊢ Ne (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
          (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' U)) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
exact isOpen_Ioo.smul_sphere one_ne_zero (by simp) hUo |>.measure_ne_zero _ (by simpa)

Premises used: isOpen_Ioo, IsOpen.smul_sphere, one_ne_zero, IsOpen.measure_ne_zero
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
h : Nontrivial E
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1 \ {0}) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) univ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞)

Tactic:
rw [toSphere_apply_univ', measure_diff_null (measure_singleton _)]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.measure_diff_null, MeasureTheory.Measure.toSphere_apply_univ'
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
⊢ Measure.real (α := (↑(sphere 0 1) : Type u_1)) μ.toSphere univ = (↑(dim E) : ℝ) * μ.real (ball 0 1)

Tactic:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (ball 0 1) : ℝ≥0∞) = 0 ↔
    dim E = 0
⊢ Eq (α := Measure (↑(sphere 0 1) : Type u_1)) μ.toSphere 0 ↔ dim E = 0

Tactic:
rw [← measure_univ_eq_zero, toSphere_apply_univ]

Premises used: MeasureTheory.Measure.toSphere_apply_univ, MeasureTheory.Measure.measure_univ_eq_zero