From b9e871204ed472b5bec5cef1b3a2db81ff804d93 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 00:02:29 +0000
Subject: [PATCH 01/16] feat(measure_theory/measure/haar_of_basis): put the
 canonical measure on euclidean space

---
 src/measure_theory/measure/haar_of_basis.lean | 21 +++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
index ae4878316a13c..859fa97bbceb1 100644
--- a/src/measure_theory/measure/haar_of_basis.lean
+++ b/src/measure_theory/measure/haar_of_basis.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import measure_theory.measure.haar
 import analysis.inner_product_space.pi_L2
+import measure_theory.constructions.pi
 
 /-!
 # Additive Haar measure constructed from a basis
@@ -159,3 +160,23 @@ is proved in `orthonormal_basis.volume_parallelepiped`. -/
 /- This instance should not be necessary, but Lean has difficulties to find it in product
 situations if we do not declare it explicitly. -/
 instance real.measure_space : measure_space ℝ := by apply_instance
+
+/-! # Miscellaneous instances for `euclidean_space`
+
+In combination with `measure_space_of_inner_product_space`, these put a `measure_space` structure
+on `euclidean_space`. -/
+namespace euclidean_space
+variables (ι)
+
+-- TODO: do we want these instances for `pi_Lp` too?
+instance : measurable_space (euclidean_space ℝ ι) := measurable_space.pi
+instance : borel_space (euclidean_space ℝ ι) := pi.borel_space
+
+/-- `pi_Lp.equiv` as a `measurable_equiv`. -/
+@[simps to_equiv]
+protected def measurable_equiv : euclidean_space ℝ ι ≃ᵐ (ι → ℝ) :=
+{ to_equiv := pi_Lp.equiv _ _,
+  measurable_to_fun := measurable_id,
+  measurable_inv_fun := measurable_id }
+
+end euclidean_space

From b59d0598138c5d86c923b30770bbdfe080109dc4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 00:34:49 +0000
Subject: [PATCH 02/16] add lemma

---
 src/measure_theory/measure/haar_of_basis.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
index 859fa97bbceb1..cbb1fe7460ded 100644
--- a/src/measure_theory/measure/haar_of_basis.lean
+++ b/src/measure_theory/measure/haar_of_basis.lean
@@ -179,4 +179,6 @@ protected def measurable_equiv : euclidean_space ℝ ι ≃ᵐ (ι → ℝ) :=
   measurable_to_fun := measurable_id,
   measurable_inv_fun := measurable_id }
 
+lemma coe_measurable_equiv : ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.equiv 2 _ := rfl
+
 end euclidean_space

From 006db9c2e37ea8d973b4cab56b345878c15cdbce Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 00:40:31 +0000
Subject: [PATCH 03/16] wip

---
 src/analysis/normed_space/pi_Lp.lean          |  7 +++++++
 src/measure_theory/measure/haar_lebesgue.lean | 11 +++++++++++
 2 files changed, 18 insertions(+)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index da14f060696de..15138aa9131fd 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -714,6 +714,13 @@ protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
   inv_fun := (pi_Lp.equiv _ _).symm,
   ..linear_equiv.refl _ _}
 
+/-- `pi_Lp.equiv` as a continuous linear equivalence. -/
+@[simps {fully_applied := ff}]
+protected def continuous_linear_equiv : pi_Lp p β ≃L[𝕜] Π i, β i :=
+{ to_linear_equiv := pi_Lp.linear_equiv _ _ _,
+  continuous_to_fun := continuous_id,
+  continuous_inv_fun := continuous_id }
+
 section basis
 
 variables (ι)
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index ac4e7f454a807..a71557bad37e9 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -86,6 +86,17 @@ instance is_add_haar_measure_volume_pi (ι : Type*) [fintype ι] :
   is_add_haar_measure (volume : measure (ι → ℝ)) :=
 by { rw ← add_haar_measure_eq_volume_pi, apply_instance }
 
+
+lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
+  measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
+begin
+  refine ⟨measurable_equiv.measurable (euclidean_space.measurable_equiv ι), _⟩,
+  rw ←add_haar_measure_eq_volume_pi,
+  dsimp only [measure_space_of_inner_product_space, basis.add_haar],
+  convert measure.map_id,
+  sorry,
+end
+
 namespace measure
 
 /-!

From bf341beb562069b46a58395df61378da6bf8ef3d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 08:54:38 +0000
Subject: [PATCH 04/16] wip

---
 src/measure_theory/measure/haar_lebesgue.lean |  2 ++
 src/measure_theory/measure/haar_of_basis.lean |  8 +++++
 src/topology/sets/compacts.lean               | 36 ++++++++++++++++++-
 3 files changed, 45 insertions(+), 1 deletion(-)

diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index a71557bad37e9..34a34cf722417 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -93,6 +93,8 @@ begin
   refine ⟨measurable_equiv.measurable (euclidean_space.measurable_equiv ι), _⟩,
   rw ←add_haar_measure_eq_volume_pi,
   dsimp only [measure_space_of_inner_product_space, basis.add_haar],
+  ext1 s hs,
+  rw measure.map_apply _ hs,
   convert measure.map_id,
   sorry,
 end
diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
index cbb1fe7460ded..d827c7b444fe5 100644
--- a/src/measure_theory/measure/haar_of_basis.lean
+++ b/src/measure_theory/measure/haar_of_basis.lean
@@ -111,6 +111,7 @@ end add_comm_group
 section normed_space
 
 variables [normed_add_comm_group E] [normed_space ℝ E]
+variables [normed_add_comm_group F] [normed_space ℝ F]
 
 /-- The parallelepiped spanned by a basis, as a compact set with nonempty interior. -/
 def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E :=
@@ -131,6 +132,13 @@ def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E :=
       rwa [← homeomorph.image_interior, nonempty_image_iff],
     end }
 
+#check positive_compacts.i
+
+lemma basis.parallelepiped_map (b : basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
+  (b.map e).parallelepiped = b.parallelepiped.map _ _ :=
+sorry
+
+#exit
 variables [measurable_space E] [borel_space E]
 
 /-- The Lebesgue measure associated to a basis, giving measure `1` to the parallelepiped spanned
diff --git a/src/topology/sets/compacts.lean b/src/topology/sets/compacts.lean
index e4a4b96b9fb58..53dc88c5af3f4 100644
--- a/src/topology/sets/compacts.lean
+++ b/src/topology/sets/compacts.lean
@@ -26,7 +26,7 @@ For a topological space `α`,
 
 open set
 
-variables {α β : Type*} [topological_space α] [topological_space β]
+variables {α β γ : Type*} [topological_space α] [topological_space β] [topological_space γ]
 
 namespace topological_space
 
@@ -96,6 +96,11 @@ protected def map (f : α → β) (hf : continuous f) (K : compacts α) : compac
 @[simp] lemma coe_map {f : α → β} (hf : continuous f) (s : compacts α) :
   (s.map f hf : set β) = f '' s := rfl
 
+@[simp] lemma map_id (K : compacts α) : K.map id continuous_id = K := compacts.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g) (K : compacts α) :
+  K.map (f ∘ g) (hf.comp hg) = (K.map g hg).map f hf := compacts.ext $ set.image_comp _ _ _
+
 /-- A homeomorphism induces an equivalence on compact sets, by taking the image. -/
 @[simp] protected def equiv (f : α ≃ₜ β) : compacts α ≃ compacts β :=
 { to_fun := compacts.map f f.continuous,
@@ -225,6 +230,26 @@ order_top.lift (coe : _ → set α) (λ _ _, id) rfl
 @[simp] lemma coe_top [compact_space α] [nonempty α] :
   (↑(⊤ : positive_compacts α) : set α) = univ := rfl
 
+/-- The image of a positive compact set under a continuous open map. -/
+protected def map (f : α → β) (hf : continuous f) (hf' : is_open_map f) (K : positive_compacts α) :
+  positive_compacts β :=
+{ interior_nonempty' :=
+    (K.interior_nonempty'.image _).mono (hf'.image_interior_subset K.to_compacts),
+  ..K.map f hf }
+
+@[simp] lemma coe_map {f : α → β} (hf : continuous f) (hf' : is_open_map f)
+  (s : positive_compacts α) :
+  (s.map f hf hf' : set β) = f '' s := rfl
+
+@[simp] lemma map_id (K : positive_compacts α) : K.map id continuous_id is_open_map.id = K :=
+positive_compacts.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g)
+  (hf' : is_open_map f) (hg' : is_open_map g)
+  (K : positive_compacts α) :
+  K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
+positive_compacts.ext $ set.image_comp _ _ _
+
 lemma _root_.exists_positive_compacts_subset [locally_compact_space α] {U : set α} (ho : is_open U)
   (hn : U.nonempty) : ∃ K : positive_compacts α, ↑K ⊆ U :=
 let ⟨x, hx⟩ := hn, ⟨K, hKc, hxK, hKU⟩ := exists_compact_subset ho hx in ⟨⟨⟨K, hKc⟩, ⟨x, hxK⟩⟩, hKU⟩
@@ -325,6 +350,15 @@ instance : inhabited (compact_opens α) := ⟨⊥⟩
 @[simp] lemma coe_map {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : compact_opens α) :
   (s.map f hf hf' : set β) = f '' s := rfl
 
+@[simp] lemma map_id (K : compact_opens α) : K.map id continuous_id is_open_map.id = K :=
+compact_opens.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g)
+  (hf' : is_open_map f) (hg' : is_open_map g)
+  (K : compact_opens α) :
+  K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
+compact_opens.ext $ set.image_comp _ _ _
+
 /-- The product of two `compact_opens`, as a `compact_opens` in the product space. -/
 protected def prod (K : compact_opens α) (L : compact_opens β) :
   compact_opens (α × β) :=

From 358d353a602d30886ca8241cd38713af41a402ea Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 08:55:26 +0000
Subject: [PATCH 05/16] feat(topology/sets/compacts): add
 `positive_compacts.map`

Also adds some missing functorial lemmas about `map`
---
 src/topology/sets/compacts.lean | 54 ++++++++++++++++++++++++++++++---
 1 file changed, 49 insertions(+), 5 deletions(-)

diff --git a/src/topology/sets/compacts.lean b/src/topology/sets/compacts.lean
index e4a4b96b9fb58..4057132130f5f 100644
--- a/src/topology/sets/compacts.lean
+++ b/src/topology/sets/compacts.lean
@@ -26,7 +26,7 @@ For a topological space `α`,
 
 open set
 
-variables {α β : Type*} [topological_space α] [topological_space β]
+variables {α β γ : Type*} [topological_space α] [topological_space β] [topological_space γ]
 
 namespace topological_space
 
@@ -96,17 +96,32 @@ protected def map (f : α → β) (hf : continuous f) (K : compacts α) : compac
 @[simp] lemma coe_map {f : α → β} (hf : continuous f) (s : compacts α) :
   (s.map f hf : set β) = f '' s := rfl
 
+@[simp] lemma map_id (K : compacts α) : K.map id continuous_id = K := compacts.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g) (K : compacts α) :
+  K.map (f ∘ g) (hf.comp hg) = (K.map g hg).map f hf := compacts.ext $ set.image_comp _ _ _
+
 /-- A homeomorphism induces an equivalence on compact sets, by taking the image. -/
-@[simp] protected def equiv (f : α ≃ₜ β) : compacts α ≃ compacts β :=
+@[simps] protected def equiv (f : α ≃ₜ β) : compacts α ≃ compacts β :=
 { to_fun := compacts.map f f.continuous,
   inv_fun := compacts.map _ f.symm.continuous,
   left_inv := λ s, by { ext1, simp only [coe_map, ← image_comp, f.symm_comp_self, image_id] },
   right_inv := λ s, by { ext1, simp only [coe_map, ← image_comp, f.self_comp_symm, image_id] } }
 
+@[simp] lemma equiv_refl : compacts.equiv (homeomorph.refl α) = equiv.refl _ :=
+equiv.ext map_id
+
+lemma equiv_trans (f : α ≃ₜ β) (g : β ≃ₜ γ) :
+  compacts.equiv (f.trans g) = (compacts.equiv f).trans (compacts.equiv g) :=
+equiv.ext $ map_comp _ _ _ _
+
+lemma equiv_symm (f : α ≃ₜ β) : compacts.equiv f.symm = (compacts.equiv f).symm :=
+rfl
+
 /-- The image of a compact set under a homeomorphism can also be expressed as a preimage. -/
-lemma equiv_to_fun_val (f : α ≃ₜ β) (K : compacts α) :
-  (compacts.equiv f K).1 = f.symm ⁻¹' K.1 :=
-congr_fun (image_eq_preimage_of_inverse f.left_inv f.right_inv) K.1
+lemma coe_equiv_apply_eq_preimage (f : α ≃ₜ β) (K : compacts α) :
+  (compacts.equiv f K : set β) = f.symm ⁻¹' (K : set α) :=
+f.to_equiv.image_eq_preimage K
 
 /-- The product of two `compacts`, as a `compacts` in the product space. -/
 protected def prod (K : compacts α) (L : compacts β) : compacts (α × β) :=
@@ -225,6 +240,26 @@ order_top.lift (coe : _ → set α) (λ _ _, id) rfl
 @[simp] lemma coe_top [compact_space α] [nonempty α] :
   (↑(⊤ : positive_compacts α) : set α) = univ := rfl
 
+/-- The image of a positive compact set under a continuous open map. -/
+protected def map (f : α → β) (hf : continuous f) (hf' : is_open_map f) (K : positive_compacts α) :
+  positive_compacts β :=
+{ interior_nonempty' :=
+    (K.interior_nonempty'.image _).mono (hf'.image_interior_subset K.to_compacts),
+  ..K.map f hf }
+
+@[simp] lemma coe_map {f : α → β} (hf : continuous f) (hf' : is_open_map f)
+  (s : positive_compacts α) :
+  (s.map f hf hf' : set β) = f '' s := rfl
+
+@[simp] lemma map_id (K : positive_compacts α) : K.map id continuous_id is_open_map.id = K :=
+positive_compacts.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g)
+  (hf' : is_open_map f) (hg' : is_open_map g)
+  (K : positive_compacts α) :
+  K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
+positive_compacts.ext $ set.image_comp _ _ _
+
 lemma _root_.exists_positive_compacts_subset [locally_compact_space α] {U : set α} (ho : is_open U)
   (hn : U.nonempty) : ∃ K : positive_compacts α, ↑K ⊆ U :=
 let ⟨x, hx⟩ := hn, ⟨K, hKc, hxK, hKU⟩ := exists_compact_subset ho hx in ⟨⟨⟨K, hKc⟩, ⟨x, hxK⟩⟩, hKU⟩
@@ -325,6 +360,15 @@ instance : inhabited (compact_opens α) := ⟨⊥⟩
 @[simp] lemma coe_map {f : α → β} (hf : continuous f) (hf' : is_open_map f) (s : compact_opens α) :
   (s.map f hf hf' : set β) = f '' s := rfl
 
+@[simp] lemma map_id (K : compact_opens α) : K.map id continuous_id is_open_map.id = K :=
+compact_opens.ext $ set.image_id _
+
+lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g)
+  (hf' : is_open_map f) (hg' : is_open_map g)
+  (K : compact_opens α) :
+  K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
+compact_opens.ext $ set.image_comp _ _ _
+
 /-- The product of two `compact_opens`, as a `compact_opens` in the product space. -/
 protected def prod (K : compact_opens α) (L : compact_opens β) :
   compact_opens (α × β) :=

From 6ed508e249b699e892dd7a08fd94f34a6a3f567e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 26 Apr 2023 10:31:27 +0000
Subject: [PATCH 06/16] chore(measure_theory/measure/haar_of_basis): lemmas
 about `basis.parallelepiped`

These are bundled versions of the lemmas about `parallelepiped`.
---
 src/measure_theory/measure/haar_of_basis.lean | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
index ae4878316a13c..034f97dd70fe8 100644
--- a/src/measure_theory/measure/haar_of_basis.lean
+++ b/src/measure_theory/measure/haar_of_basis.lean
@@ -109,7 +109,7 @@ end add_comm_group
 
 section normed_space
 
-variables [normed_add_comm_group E] [normed_space ℝ E]
+variables [normed_add_comm_group E] [normed_add_comm_group F] [normed_space ℝ E] [normed_space ℝ F]
 
 /-- The parallelepiped spanned by a basis, as a compact set with nonempty interior. -/
 def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E :=
@@ -130,6 +130,23 @@ def basis.parallelepiped (b : basis ι ℝ E) : positive_compacts E :=
       rwa [← homeomorph.image_interior, nonempty_image_iff],
     end }
 
+@[simp] lemma basis.coe_parallelepiped (b : basis ι ℝ E) :
+  (b.parallelepiped : set E) = parallelepiped b :=
+rfl
+
+@[simp] lemma basis.parallelepiped_reindex (b : basis ι ℝ E) (e : ι ≃ ι') :
+  (b.reindex e).parallelepiped = b.parallelepiped :=
+positive_compacts.ext $
+  (congr_arg parallelepiped (b.coe_reindex _)).trans (parallelepiped_comp_equiv b e.symm)
+
+lemma basis.parallelepiped_map (b : basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
+  (b.map e).parallelepiped = b.parallelepiped.map e
+    (by haveI := finite_dimensional.of_fintype_basis b; exact
+      e.to_linear_map.continuous_of_finite_dimensional)
+    (by haveI := finite_dimensional.of_fintype_basis (b.map e); exact
+      e.to_linear_map.is_open_map_of_finite_dimensional e.surjective) :=
+positive_compacts.ext (image_parallelepiped e.to_linear_map _).symm
+
 variables [measurable_space E] [borel_space E]
 
 /-- The Lebesgue measure associated to a basis, giving measure `1` to the parallelepiped spanned

From 954e92beffaac09292075ba62246e499a7ecc90e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 14 May 2023 22:33:23 +0000
Subject: [PATCH 07/16] fix bad merge

---
 src/topology/sets/compacts.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/topology/sets/compacts.lean b/src/topology/sets/compacts.lean
index 129de284caa29..8dc271235107e 100644
--- a/src/topology/sets/compacts.lean
+++ b/src/topology/sets/compacts.lean
@@ -369,15 +369,6 @@ lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continu
   K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
 compact_opens.ext $ set.image_comp _ _ _
 
-@[simp] lemma map_id (K : compact_opens α) : K.map id continuous_id is_open_map.id = K :=
-compact_opens.ext $ set.image_id _
-
-lemma map_comp (f : β → γ) (g : α → β) (hf : continuous f) (hg : continuous g)
-  (hf' : is_open_map f) (hg' : is_open_map g)
-  (K : compact_opens α) :
-  K.map (f ∘ g) (hf.comp hg) (hf'.comp hg') = (K.map g hg hg').map f hf hf' :=
-compact_opens.ext $ set.image_comp _ _ _
-
 /-- The product of two `compact_opens`, as a `compact_opens` in the product space. -/
 protected def prod (K : compact_opens α) (L : compact_opens β) :
   compact_opens (α × β) :=

From 729517774275b08ba9cbdb90307b26d8e7eca546 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 08:36:55 +0000
Subject: [PATCH 08/16] wip

---
 src/measure_theory/measure/haar_lebesgue.lean | 30 +++++++++++--------
 1 file changed, 18 insertions(+), 12 deletions(-)

diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index 23eb0fca65346..3d743a4616ec5 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -96,18 +96,6 @@ instance is_add_haar_measure_volume_pi (ι : Type*) [fintype ι] :
 by { rw ← add_haar_measure_eq_volume_pi, apply_instance }
 
 
-lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
-  measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
-begin
-  refine ⟨measurable_equiv.measurable (euclidean_space.measurable_equiv ι), _⟩,
-  rw ←add_haar_measure_eq_volume_pi,
-  dsimp only [measure_space_of_inner_product_space, basis.add_haar],
-  ext1 s hs,
-  rw measure.map_apply _ hs,
-  convert measure.map_id,
-  sorry,
-end
-
 namespace measure
 
 /-!
@@ -449,6 +437,24 @@ by rw [integral_comp_inv_smul μ f R, abs_of_nonneg ((pow_nonneg hR _))]
 /-! We don't need to state `map_add_haar_neg` here, because it has already been proved for
 general Haar measures on general commutative groups. -/
 
+lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
+  measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
+begin
+  change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
+  refine ⟨measurable_equiv.measurable _, _⟩,
+  rw ←add_haar_measure_eq_volume_pi,
+  dsimp only [measure_space_of_inner_product_space, basis.add_haar],
+  ext1 s hs,
+  rw measure.map_apply (measurable_equiv.measurable _) hs,
+  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ _ _, from rfl)],
+  rw add_haar_preimage_continuous_linear_equiv,
+  -- rw add_haar_measure
+  sorry,
+end
+
+#exit
+
+
 /-! ### Measure of balls -/
 
 lemma add_haar_ball_center

From cb2bc14503c7b3f4e5068e9342d83ee43bc0c89d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 12:43:33 +0000
Subject: [PATCH 09/16] reduce diff

---
 src/measure_theory/measure/haar_lebesgue.lean | 1 -
 src/measure_theory/measure/haar_of_basis.lean | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index e2681a99827a6..8396c46d64e25 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -95,7 +95,6 @@ instance is_add_haar_measure_volume_pi (ι : Type*) [fintype ι] :
   is_add_haar_measure (volume : measure (ι → ℝ)) :=
 by { rw ← add_haar_measure_eq_volume_pi, apply_instance }
 
-
 namespace measure
 
 /-!
diff --git a/src/measure_theory/measure/haar_of_basis.lean b/src/measure_theory/measure/haar_of_basis.lean
index fc42bf107e8c8..3da1e80196ca2 100644
--- a/src/measure_theory/measure/haar_of_basis.lean
+++ b/src/measure_theory/measure/haar_of_basis.lean
@@ -5,7 +5,6 @@ Authors: Sébastien Gouëzel
 -/
 import measure_theory.measure.haar
 import analysis.inner_product_space.pi_L2
-import measure_theory.constructions.pi
 
 /-!
 # Additive Haar measure constructed from a basis

From 0842c48f2dfb380f12950a7550b8c79920194e4b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 12:56:33 +0000
Subject: [PATCH 10/16] wip

---
 src/analysis/normed_space/pi_Lp.lean          | 5 +++++
 src/measure_theory/measure/haar_lebesgue.lean | 3 ++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index d6ead6efaefb7..3bf57665d58f1 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -714,6 +714,11 @@ protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
   inv_fun := (pi_Lp.equiv _ _).symm,
   ..linear_equiv.refl _ _}
 
+@[simp] lemma det_linear_equiv : (pi_Lp.linear_equiv p 𝕜 β).det = 1 := linear_equiv.det_refl
+
+@[simp] lemma det_linear_equiv_symm : (pi_Lp.linear_equiv p 𝕜 β).symm.det = 1 :=
+linear_equiv.det_refl
+
 /-- `pi_Lp.equiv` as a continuous linear equivalence. -/
 @[simps {fully_applied := ff}]
 protected def continuous_linear_equiv : pi_Lp p β ≃L[𝕜] Π i, β i :=
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index 8396c46d64e25..eee20fd545a8e 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -445,8 +445,9 @@ begin
   dsimp only [measure_space_of_inner_product_space, basis.add_haar],
   ext1 s hs,
   rw measure.map_apply (measurable_equiv.measurable _) hs,
-  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ _ _, from rfl)],
+  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
   rw add_haar_preimage_continuous_linear_equiv,
+  convert one_mul _,
   -- rw add_haar_measure
   sorry,
 end

From eb5644a92938142f0b48146e8c3ef3b7c974e445 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 14:21:34 +0000
Subject: [PATCH 11/16] whoops, sloppy types

---
 src/analysis/normed_space/pi_Lp.lean          |  5 ++-
 src/measure_theory/measure/haar_lebesgue.lean | 33 ++++---------------
 src/measure_theory/measure/haar_of_inner.lean | 16 +++++++++
 3 files changed, 26 insertions(+), 28 deletions(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index 3bf57665d58f1..20a5cf2d1b5dd 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -714,7 +714,10 @@ protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
   inv_fun := (pi_Lp.equiv _ _).symm,
   ..linear_equiv.refl _ _}
 
-@[simp] lemma det_linear_equiv : (pi_Lp.linear_equiv p 𝕜 β).det = 1 := linear_equiv.det_refl
+@[simp] lemma det_linear_equiv : (pi_Lp.linear_equiv p 𝕜 β : pi_Lp p β ≃ₗ[𝕜] Π i, β i).det = 1 :=
+linear_map.det_id
+
+#check basis.det
 
 @[simp] lemma det_linear_equiv_symm : (pi_Lp.linear_equiv p 𝕜 β).symm.det = 1 :=
 linear_equiv.det_refl
diff --git a/src/measure_theory/measure/haar_lebesgue.lean b/src/measure_theory/measure/haar_lebesgue.lean
index eee20fd545a8e..b86b7cffa954e 100644
--- a/src/measure_theory/measure/haar_lebesgue.lean
+++ b/src/measure_theory/measure/haar_lebesgue.lean
@@ -269,18 +269,17 @@ add_haar_preimage_linear_map μ hf s
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_linear_equiv
   (f : E ≃ₗ[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ennreal.of_real (abs f.det⁻¹) * μ s :=
 begin
   have A : (f : E →ₗ[ℝ] E).det ≠ 0 := (linear_equiv.is_unit_det' f).ne_zero,
   convert add_haar_preimage_linear_map μ A s,
-  simp only [linear_equiv.det_coe_symm]
 end
 
 /-- The preimage of a set `s` under a continuous linear equiv `f` has measure
 equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
 @[simp] lemma add_haar_preimage_continuous_linear_equiv
   (f : E ≃L[ℝ] E) (s : set E) :
-  μ (f ⁻¹' s) = ennreal.of_real (abs (f.symm : E →ₗ[ℝ] E).det) * μ s :=
+  μ (f ⁻¹' s) = ennreal.of_real (abs f.det⁻¹) * μ s :=
 add_haar_preimage_linear_equiv μ _ s
 
 /-- The image of a set `s` under a linear map `f` has measure
@@ -292,11 +291,10 @@ begin
   rcases ne_or_eq f.det 0 with hf|hf,
   { let g := (f.equiv_of_det_ne_zero hf).to_continuous_linear_equiv,
     change μ (g '' s) = _,
-    rw [continuous_linear_equiv.image_eq_preimage g s, add_haar_preimage_continuous_linear_equiv],
-    congr,
-    ext x,
-    simp only [linear_equiv.coe_to_continuous_linear_equiv, linear_equiv.of_is_unit_det_apply,
-               linear_equiv.coe_coe, continuous_linear_equiv.symm_symm], },
+    rw [continuous_linear_equiv.image_eq_preimage g s, add_haar_preimage_continuous_linear_equiv,
+      continuous_linear_equiv.symm_to_linear_equiv, linear_equiv.det_symm, units.coe_inv, inv_inv,
+      linear_equiv.coe_det, linear_equiv.to_linear_equiv_to_continuous_linear_equiv,
+      linear_equiv.coe_of_is_unit_det] },
   { simp only [hf, zero_mul, ennreal.of_real_zero, abs_zero],
     have : μ f.range = 0 :=
       add_haar_submodule μ _ (linear_map.range_lt_top_of_det_eq_zero hf).ne,
@@ -436,25 +434,6 @@ by rw [integral_comp_inv_smul μ f R, abs_of_nonneg ((pow_nonneg hR _))]
 /-! We don't need to state `map_add_haar_neg` here, because it has already been proved for
 general Haar measures on general commutative groups. -/
 
-lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
-  measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
-begin
-  change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
-  refine ⟨measurable_equiv.measurable _, _⟩,
-  rw ←add_haar_measure_eq_volume_pi,
-  dsimp only [measure_space_of_inner_product_space, basis.add_haar],
-  ext1 s hs,
-  rw measure.map_apply (measurable_equiv.measurable _) hs,
-  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
-  rw add_haar_preimage_continuous_linear_equiv,
-  convert one_mul _,
-  -- rw add_haar_measure
-  sorry,
-end
-
-#exit
-
-
 /-! ### Measure of balls -/
 
 lemma add_haar_ball_center
diff --git a/src/measure_theory/measure/haar_of_inner.lean b/src/measure_theory/measure/haar_of_inner.lean
index 0923810fae711..e926c16fb6c1e 100644
--- a/src/measure_theory/measure/haar_of_inner.lean
+++ b/src/measure_theory/measure/haar_of_inner.lean
@@ -68,3 +68,19 @@ begin
   rw ← o.measure_eq_volume,
   exact o.measure_orthonormal_basis b,
 end
+
+lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
+  measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
+begin
+  change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
+  refine ⟨measurable_equiv.measurable _, _⟩,
+  rw ←add_haar_measure_eq_volume_pi,
+  ext1 s hs,
+  rw measure.map_apply (measurable_equiv.measurable _) hs,
+  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
+  rw [add_haar_preimage_continuous_linear_equiv, pi_Lp.continuous_linear_equiv_to_linear_equiv,
+    pi_Lp.det_linear_equiv, units.coe_one, inv_one, abs_one, ennreal.of_real_one, one_mul],
+  -- congr' 1,
+end
+
+#exit

From d1eba19a8db94370b4e11c9c26ac11eba2f02c0d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 14:21:47 +0000
Subject: [PATCH 12/16] remove bad lemma

---
 src/analysis/normed_space/pi_Lp.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index 20a5cf2d1b5dd..d6ead6efaefb7 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -714,14 +714,6 @@ protected def linear_equiv : pi_Lp p β ≃ₗ[𝕜] Π i, β i :=
   inv_fun := (pi_Lp.equiv _ _).symm,
   ..linear_equiv.refl _ _}
 
-@[simp] lemma det_linear_equiv : (pi_Lp.linear_equiv p 𝕜 β : pi_Lp p β ≃ₗ[𝕜] Π i, β i).det = 1 :=
-linear_map.det_id
-
-#check basis.det
-
-@[simp] lemma det_linear_equiv_symm : (pi_Lp.linear_equiv p 𝕜 β).symm.det = 1 :=
-linear_equiv.det_refl
-
 /-- `pi_Lp.equiv` as a continuous linear equivalence. -/
 @[simps {fully_applied := ff}]
 protected def continuous_linear_equiv : pi_Lp p β ≃L[𝕜] Π i, β i :=

From afb1e373832e676ca624d4c420d0740c8290536a Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 16:16:34 +0000
Subject: [PATCH 13/16] wip

---
 src/analysis/inner_product_space/pi_L2.lean   | 19 +++++++
 src/analysis/normed_space/pi_Lp.lean          | 57 ++++++++++++++++++-
 src/measure_theory/measure/haar_of_inner.lean | 28 ++++++---
 3 files changed, 94 insertions(+), 10 deletions(-)

diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean
index 4c865e310c985..e4d8153f13918 100644
--- a/src/analysis/inner_product_space/pi_L2.lean
+++ b/src/analysis/inner_product_space/pi_L2.lean
@@ -229,6 +229,25 @@ lemma euclidean_space.inner_single_right [decidable_eq ι] (i : ι) (a : 𝕜)
   ⟪v, euclidean_space.single i (a : 𝕜)⟫ =  a * conj (v i) :=
 by simp [apply_ite conj, mul_comm]
 
+@[simp] lemma euclidean_space.norm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
+  ‖euclidean_space.single i (a : 𝕜)‖ = ‖a‖ :=
+by rw [@norm_eq_sqrt_inner 𝕜 _ _ _ _ (euclidean_space.single i a),
+  euclidean_space.inner_single_left, euclidean_space.single_apply, if_pos rfl,
+  @norm_eq_sqrt_inner 𝕜, is_R_or_C.inner_apply]
+
+@[simp] lemma euclidean_space.nnnorm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
+  ‖euclidean_space.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
+nnreal.eq $ euclidean_space.norm_single _ _
+
+@[simp] lemma euclidean_space.dist_single_of_eq [decidable_eq ι] (i : ι) (a b : 𝕜) :
+  dist (euclidean_space.single i (a : 𝕜)) (euclidean_space.single i (b : 𝕜)) = dist a b :=
+by rw [pi_Lp.dist_eq_sum, finset.sum_eq_single i, euclidean_space.single_apply, if_pos rfl]
+
+@[simp] lemma euclidean_space.nnnorm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
+  ‖euclidean_space.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
+nnreal.eq $ euclidean_space.norm_single _ _
+
+
 lemma euclidean_space.pi_Lp_congr_left_single [decidable_eq ι] {ι' : Type*} [fintype ι']
   [decidable_eq ι'] (e : ι' ≃ ι) (i' : ι') :
   linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e (euclidean_space.single i' (1:𝕜)) =
diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index d6ead6efaefb7..ec85d614f1aa0 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -623,7 +623,9 @@ linear_isometry_equiv.ext $ λ x, rfl
 
 @[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_single
   [decidable_eq ι] [decidable_eq ι'] (e : ι ≃ ι') (i : ι) (v : E) :
-  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (pi.single i v) = pi.single (e i) v :=
+  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (
+    (pi_Lp.equiv p (λ _, E)).symm $ pi.single i v) =
+      (pi_Lp.equiv p (λ _, E)).symm (pi.single (e i) v) :=
 begin
   funext x,
   simp [linear_isometry_equiv.pi_Lp_congr_left, linear_equiv.Pi_congr_left', equiv.Pi_congr_left',
@@ -649,6 +651,59 @@ end
 @[simp] lemma equiv_symm_smul :
   (pi_Lp.equiv p β).symm (c • x') = c • (pi_Lp.equiv p β).symm x' := rfl
 
+section single
+
+variables (p)
+variables [decidable_eq ι]
+
+@[simp]
+lemma nnnorm_equiv_symm_single (i : ι) (b : β i) :
+  ‖(pi_Lp.equiv p β).symm (pi.single i b)‖₊ = ‖b‖₊ :=
+begin
+  haveI : nonempty ι := ⟨i⟩,
+  unfreezingI { induction p using with_top.rec_top_coe },
+  { simp_rw [nnnorm_eq_csupr, equiv_symm_apply],
+    refine csupr_eq_of_forall_le_of_forall_lt_exists_gt (λ j, _) (λ n hn, ⟨i, hn.trans_eq _⟩),
+    { obtain rfl | hij := decidable.eq_or_ne i j,
+      { rw pi.single_eq_same },
+      { rw [pi.single_eq_of_ne' hij, nnnorm_zero],
+        exact zero_le _ } },
+    { rw pi.single_eq_same } },
+  { have hp0 : (p : ℝ) ≠ 0,
+    { exact_mod_cast (zero_lt_one.trans_le $ fact.out (1 ≤ (p : ℝ≥0∞))).ne' },
+    rw [nnnorm_eq_sum ennreal.coe_ne_top, ennreal.coe_to_real, fintype.sum_eq_single i,
+      equiv_symm_apply, pi.single_eq_same, ←nnreal.rpow_mul, one_div, mul_inv_cancel hp0,
+      nnreal.rpow_one],
+    intros j hij,
+    rw [equiv_symm_apply, pi.single_eq_of_ne hij, nnnorm_zero, nnreal.zero_rpow hp0] },
+end
+
+@[simp]
+lemma norm_equiv_symm_single (i : ι) (b : β i) :
+  ‖(pi_Lp.equiv p β).symm (pi.single i b)‖ = ‖b‖ :=
+congr_arg coe $ nnnorm_equiv_symm_single p β i b
+
+@[simp]
+lemma nndist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
+  nndist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
+    nndist b₁ b₂  :=
+by rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ←equiv_symm_sub, ←pi.single_sub,
+  nnnorm_equiv_symm_single]
+
+@[simp]
+lemma dist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
+  dist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
+    dist b₁ b₂ :=
+congr_arg coe $ nndist_equiv_symm_single_same p β i b₁ b₂
+
+@[simp]
+lemma edist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
+  edist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
+    edist b₁ b₂ :=
+by simpa only [edist_nndist] using congr_arg coe (nndist_equiv_symm_single_same p β i b₁ b₂)
+
+end single
+
 /-- When `p = ∞`, this lemma does not hold without the additional assumption `nonempty ι` because
 the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
 `pi_Lp.nnnorm_equiv_symm_const'` for a version which exchanges the hypothesis `p ≠ ∞` for
diff --git a/src/measure_theory/measure/haar_of_inner.lean b/src/measure_theory/measure/haar_of_inner.lean
index e926c16fb6c1e..5f9d1e50bbcc0 100644
--- a/src/measure_theory/measure/haar_of_inner.lean
+++ b/src/measure_theory/measure/haar_of_inner.lean
@@ -72,15 +72,25 @@ end
 lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
   measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
 begin
-  change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
-  refine ⟨measurable_equiv.measurable _, _⟩,
-  rw ←add_haar_measure_eq_volume_pi,
-  ext1 s hs,
-  rw measure.map_apply (measurable_equiv.measurable _) hs,
-  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
-  rw [add_haar_preimage_continuous_linear_equiv, pi_Lp.continuous_linear_equiv_to_linear_equiv,
-    pi_Lp.det_linear_equiv, units.coe_one, inv_one, abs_one, ennreal.of_real_one, one_mul],
-  -- congr' 1,
+  let b : orthonormal_basis ι ℝ (euclidean_space ℝ ι),
+  { classical,
+    refine (pi_Lp.basis_fun 2 ℝ ι).to_orthonormal_basis ⟨λ i, _, λ i j hij, _⟩,
+    simp [pi_Lp.basis_fun_apply], },
+  -- have : fact (finrank ℝ (euclidean_space ℝ ι) = fintype.card ι) := ⟨_⟩
+  -- let o : orientation ℝ (euclidean_space ℝ ι) (fin $ fintype.card ι) :=
+  --   orientation.map _ (pi_Lp.linear_equiv 2 ℝ (λ _, ℝ)).symm _,
+  -- rw ←o.measure_eq_volume,
+  -- change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
+  -- refine ⟨measurable_equiv.measurable _, _⟩,
+  -- rw ←add_haar_measure_eq_volume_pi,
+  -- ext1 s hs,
+  -- rw measure.map_apply (measurable_equiv.measurable _) hs,
+  -- rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
+  -- -- rw [add_haar_preimage_continuous_linear_equiv, pi_Lp.continuous_linear_equiv_to_linear_equiv,
+  -- --   pi_Lp.det_linear_equiv, units.coe_one, inv_one, abs_one, ennreal.of_real_one, one_mul],
+  -- -- congr' 1,
 end
 
+#check basis.to_orthonormal_basis
+
 #exit

From bf36504a4365829de27fc0f422281d5ae220176f Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 15 May 2023 16:43:35 +0000
Subject: [PATCH 14/16] revert unrelated tweaks

---
 src/analysis/inner_product_space/pi_L2.lean | 19 -------
 src/analysis/normed_space/pi_Lp.lean        | 57 +--------------------
 2 files changed, 1 insertion(+), 75 deletions(-)

diff --git a/src/analysis/inner_product_space/pi_L2.lean b/src/analysis/inner_product_space/pi_L2.lean
index e4d8153f13918..4c865e310c985 100644
--- a/src/analysis/inner_product_space/pi_L2.lean
+++ b/src/analysis/inner_product_space/pi_L2.lean
@@ -229,25 +229,6 @@ lemma euclidean_space.inner_single_right [decidable_eq ι] (i : ι) (a : 𝕜)
   ⟪v, euclidean_space.single i (a : 𝕜)⟫ =  a * conj (v i) :=
 by simp [apply_ite conj, mul_comm]
 
-@[simp] lemma euclidean_space.norm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
-  ‖euclidean_space.single i (a : 𝕜)‖ = ‖a‖ :=
-by rw [@norm_eq_sqrt_inner 𝕜 _ _ _ _ (euclidean_space.single i a),
-  euclidean_space.inner_single_left, euclidean_space.single_apply, if_pos rfl,
-  @norm_eq_sqrt_inner 𝕜, is_R_or_C.inner_apply]
-
-@[simp] lemma euclidean_space.nnnorm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
-  ‖euclidean_space.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
-nnreal.eq $ euclidean_space.norm_single _ _
-
-@[simp] lemma euclidean_space.dist_single_of_eq [decidable_eq ι] (i : ι) (a b : 𝕜) :
-  dist (euclidean_space.single i (a : 𝕜)) (euclidean_space.single i (b : 𝕜)) = dist a b :=
-by rw [pi_Lp.dist_eq_sum, finset.sum_eq_single i, euclidean_space.single_apply, if_pos rfl]
-
-@[simp] lemma euclidean_space.nnnorm_single [decidable_eq ι] (i : ι) (a : 𝕜) :
-  ‖euclidean_space.single i (a : 𝕜)‖₊ = ‖a‖₊ :=
-nnreal.eq $ euclidean_space.norm_single _ _
-
-
 lemma euclidean_space.pi_Lp_congr_left_single [decidable_eq ι] {ι' : Type*} [fintype ι']
   [decidable_eq ι'] (e : ι' ≃ ι) (i' : ι') :
   linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e (euclidean_space.single i' (1:𝕜)) =
diff --git a/src/analysis/normed_space/pi_Lp.lean b/src/analysis/normed_space/pi_Lp.lean
index ec85d614f1aa0..d6ead6efaefb7 100644
--- a/src/analysis/normed_space/pi_Lp.lean
+++ b/src/analysis/normed_space/pi_Lp.lean
@@ -623,9 +623,7 @@ linear_isometry_equiv.ext $ λ x, rfl
 
 @[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_single
   [decidable_eq ι] [decidable_eq ι'] (e : ι ≃ ι') (i : ι) (v : E) :
-  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (
-    (pi_Lp.equiv p (λ _, E)).symm $ pi.single i v) =
-      (pi_Lp.equiv p (λ _, E)).symm (pi.single (e i) v) :=
+  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (pi.single i v) = pi.single (e i) v :=
 begin
   funext x,
   simp [linear_isometry_equiv.pi_Lp_congr_left, linear_equiv.Pi_congr_left', equiv.Pi_congr_left',
@@ -651,59 +649,6 @@ end
 @[simp] lemma equiv_symm_smul :
   (pi_Lp.equiv p β).symm (c • x') = c • (pi_Lp.equiv p β).symm x' := rfl
 
-section single
-
-variables (p)
-variables [decidable_eq ι]
-
-@[simp]
-lemma nnnorm_equiv_symm_single (i : ι) (b : β i) :
-  ‖(pi_Lp.equiv p β).symm (pi.single i b)‖₊ = ‖b‖₊ :=
-begin
-  haveI : nonempty ι := ⟨i⟩,
-  unfreezingI { induction p using with_top.rec_top_coe },
-  { simp_rw [nnnorm_eq_csupr, equiv_symm_apply],
-    refine csupr_eq_of_forall_le_of_forall_lt_exists_gt (λ j, _) (λ n hn, ⟨i, hn.trans_eq _⟩),
-    { obtain rfl | hij := decidable.eq_or_ne i j,
-      { rw pi.single_eq_same },
-      { rw [pi.single_eq_of_ne' hij, nnnorm_zero],
-        exact zero_le _ } },
-    { rw pi.single_eq_same } },
-  { have hp0 : (p : ℝ) ≠ 0,
-    { exact_mod_cast (zero_lt_one.trans_le $ fact.out (1 ≤ (p : ℝ≥0∞))).ne' },
-    rw [nnnorm_eq_sum ennreal.coe_ne_top, ennreal.coe_to_real, fintype.sum_eq_single i,
-      equiv_symm_apply, pi.single_eq_same, ←nnreal.rpow_mul, one_div, mul_inv_cancel hp0,
-      nnreal.rpow_one],
-    intros j hij,
-    rw [equiv_symm_apply, pi.single_eq_of_ne hij, nnnorm_zero, nnreal.zero_rpow hp0] },
-end
-
-@[simp]
-lemma norm_equiv_symm_single (i : ι) (b : β i) :
-  ‖(pi_Lp.equiv p β).symm (pi.single i b)‖ = ‖b‖ :=
-congr_arg coe $ nnnorm_equiv_symm_single p β i b
-
-@[simp]
-lemma nndist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
-  nndist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
-    nndist b₁ b₂  :=
-by rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ←equiv_symm_sub, ←pi.single_sub,
-  nnnorm_equiv_symm_single]
-
-@[simp]
-lemma dist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
-  dist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
-    dist b₁ b₂ :=
-congr_arg coe $ nndist_equiv_symm_single_same p β i b₁ b₂
-
-@[simp]
-lemma edist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
-  edist ((pi_Lp.equiv p β).symm (pi.single i b₁)) ((pi_Lp.equiv p β).symm (pi.single i b₂)) =
-    edist b₁ b₂ :=
-by simpa only [edist_nndist] using congr_arg coe (nndist_equiv_symm_single_same p β i b₁ b₂)
-
-end single
-
 /-- When `p = ∞`, this lemma does not hold without the additional assumption `nonempty ι` because
 the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
 `pi_Lp.nnnorm_equiv_symm_const'` for a version which exchanges the hypothesis `p ≠ ∞` for

From 22e7f9d907e849a5289b39754145fa39eaa3ed0b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 22 May 2023 15:57:41 +0000
Subject: [PATCH 15/16] wip

---
 .../measure/haar/inner_product_space.lean     | 39 +++++++++++--------
 .../measure/lebesgue/eq_haar.lean             | 19 +++++++++
 2 files changed, 41 insertions(+), 17 deletions(-)

diff --git a/src/measure_theory/measure/haar/inner_product_space.lean b/src/measure_theory/measure/haar/inner_product_space.lean
index cfe16ae1a3fee..e6dba695ff320 100644
--- a/src/measure_theory/measure/haar/inner_product_space.lean
+++ b/src/measure_theory/measure/haar/inner_product_space.lean
@@ -72,23 +72,28 @@ end
 lemma euclidean_space.volume_preserving_pi_Lp_equiv (ι : Type*) [fintype ι] :
   measure_preserving (pi_Lp.equiv _ _) (volume : measure (euclidean_space ℝ ι)) volume :=
 begin
-  let b : orthonormal_basis ι ℝ (euclidean_space ℝ ι),
-  { classical,
-    refine (pi_Lp.basis_fun 2 ℝ ι).to_orthonormal_basis ⟨λ i, _, λ i j hij, _⟩,
-    simp [pi_Lp.basis_fun_apply], },
-  -- have : fact (finrank ℝ (euclidean_space ℝ ι) = fintype.card ι) := ⟨_⟩
-  -- let o : orientation ℝ (euclidean_space ℝ ι) (fin $ fintype.card ι) :=
-  --   orientation.map _ (pi_Lp.linear_equiv 2 ℝ (λ _, ℝ)).symm _,
-  -- rw ←o.measure_eq_volume,
-  -- change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
-  -- refine ⟨measurable_equiv.measurable _, _⟩,
-  -- rw ←add_haar_measure_eq_volume_pi,
-  -- ext1 s hs,
-  -- rw measure.map_apply (measurable_equiv.measurable _) hs,
-  -- rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
-  -- -- rw [add_haar_preimage_continuous_linear_equiv, pi_Lp.continuous_linear_equiv_to_linear_equiv,
-  -- --   pi_Lp.det_linear_equiv, units.coe_one, inv_one, abs_one, ennreal.of_real_one, one_mul],
-  -- -- congr' 1,
+  let b : orthonormal_basis ι ℝ (euclidean_space ℝ ι) := default,
+  haveI : fact (finrank ℝ (euclidean_space ℝ ι) = fintype.card ι) := ⟨finrank_euclidean_space⟩,
+  classical,
+  obtain ⟨ιe⟩ := fintype.trunc_equiv_fin ι,
+  let o : orientation ℝ (euclidean_space ℝ ι) (fin $ fintype.card ι) :=
+    basis.orientation ((pi_Lp.basis_fun 2 _ _).reindex ιe),
+    -- orientation.map _ (pi_Lp.linear_equiv 2 ℝ (λ _, ℝ)).symm
+    --   (orientation.comp _ _),
+  rw ←o.measure_eq_volume,
+  change measure_preserving (euclidean_space.measurable_equiv ι) _ _,
+  refine ⟨measurable_equiv.measurable _, _⟩,
+  rw ←add_haar_measure_eq_volume_pi,
+  ext1 s hs,
+  rw measure.map_apply (measurable_equiv.measurable _) hs,
+  rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
+  dsimp [measure_space_of_inner_product_space, o, basis.orientation],
+  simp_rw basis.det_reindex,
+  sorry,
+  sorry,
+  -- rw [add_haar_preimage_continuous_linear_equiv, pi_Lp.continuous_linear_equiv_to_linear_equiv,
+  --   pi_Lp.det_linear_equiv, units.coe_one, inv_one, abs_one, ennreal.of_real_one, one_mul],
+  -- congr' 1,
 end
 
 #check basis.to_orthonormal_basis
diff --git a/src/measure_theory/measure/lebesgue/eq_haar.lean b/src/measure_theory/measure/lebesgue/eq_haar.lean
index 059be3f683cdb..279c33afc871d 100644
--- a/src/measure_theory/measure/lebesgue/eq_haar.lean
+++ b/src/measure_theory/measure/lebesgue/eq_haar.lean
@@ -71,6 +71,25 @@ set_like.coe_injective $ begin
   { exact zero_le_one },
 end
 
+/-- A parallelepiped can be exressed on the standard basis -/
+lemma basis.parallelepiped_eq_map {ι M : Type*} [fintype ι] [normed_add_comm_group M]
+  [normed_space ℝ M] (b : basis ι ℝ M) :
+  b.parallelepiped = (topological_space.positive_compacts.pi_Icc01 ι).map b.equiv_fun.symm
+    b.equiv_funL.symm.continuous
+    (by haveI := finite_dimensional.of_fintype_basis b; exact
+      b.equiv_funL.symm.to_linear_map.is_open_map_of_finite_dimensional
+        b.equiv_fun.symm.surjective) :=
+begin
+  rw ← basis.parallelepiped_basis_fun,
+  refine (congr_arg _ _).trans (basis.parallelepiped_map _ _),
+  ext i,
+  rw [basis.map_apply, basis.apply_eq_iff],
+  ext j,
+  classical,
+  rw [←basis.coord_apply b, basis.coord_equiv_fun_symm, pi.basis_fun_apply],
+  refl,
+end
+
 namespace measure_theory
 
 open measure topological_space.positive_compacts finite_dimensional

From 32e36cf7f057fcdfbc7515a571ec87ad34f79aa2 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 15 Jul 2023 11:31:33 +0000
Subject: [PATCH 16/16] new lemma

---
 src/linear_algebra/determinant.lean                      | 5 +++++
 src/measure_theory/measure/haar/inner_product_space.lean | 1 +
 2 files changed, 6 insertions(+)

diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index c7a57875c72af..c2a99962857b9 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -559,6 +559,11 @@ lemma basis.det_reindex {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (b.reindex e).det v = b.det (v ∘ e) :=
 by rw [basis.det_apply, basis.to_matrix_reindex', det_reindex_alg_equiv, basis.det_apply]
 
+lemma basis.det_reindex' {ι' : Type*} [fintype ι'] [decidable_eq ι']
+  (b : basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
+  (b.reindex e).det = b.det.dom_dom_congr e :=
+alternating_map.ext $ λ _, basis.det_reindex _ _ _
+
 lemma basis.det_reindex_symm {ι' : Type*} [fintype ι'] [decidable_eq ι']
   (b : basis ι R M) (v : ι → M) (e : ι' ≃ ι) :
   (b.reindex e.symm).det (v ∘ e) = b.det v :=
diff --git a/src/measure_theory/measure/haar/inner_product_space.lean b/src/measure_theory/measure/haar/inner_product_space.lean
index e6dba695ff320..da97afa3aa0a5 100644
--- a/src/measure_theory/measure/haar/inner_product_space.lean
+++ b/src/measure_theory/measure/haar/inner_product_space.lean
@@ -88,6 +88,7 @@ begin
   rw measure.map_apply (measurable_equiv.measurable _) hs,
   rw [(show ⇑(euclidean_space.measurable_equiv ι) = pi_Lp.continuous_linear_equiv _ ℝ _, from rfl)],
   dsimp [measure_space_of_inner_product_space, o, basis.orientation],
+  have := basis.det_reindex (pi_Lp.basis_fun 2 ℝ ι) _ ιe,
   simp_rw basis.det_reindex,
   sorry,
   sorry,