awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
⊢ MeasurePreserving.{u_4, u_4} (α := WithLp 2 (ι → ℝ)) ofLp (volume : Measure (WithLp 2 (ι → ℝ)))
    (volume : Measure (ι → ℝ))

Tactic:
EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι

Premises used: EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
⊢ MeasurePreserving.{u_4, u_4} (α := ι → ℝ) (β := WithLp 2 (ι → ℝ)) (toLp 2) (volume : Measure (ι → ℝ))
    (volume : Measure (WithLp 2 (ι → ℝ)))

Tactic:
(EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp ι).symm

Premises used: MeasureTheory.MeasurePreserving.symm, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
rw : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (volume : Measure (ι → ℝ))) (dirac 0)
rw₁ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (dirac 0)) (dirac 0)
rw₂ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (dirac (toLp 2 0)) (dirac 0)
rw₃ rw₄ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (dirac 0) (dirac 0)
⊢ Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) volume (dirac 0)

Tactic:
rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]

Premises used: PiLp.volume_preserving_toLp, WithLp.toLp_zero, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.volume_pi_eq_dirac, MeasureTheory.Measure.map_dirac, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ MeasurePreserving.{u_2, u_3} (α := E) (β := F) (⇑f : (a : E) → F) (volume : Measure E) (volume : Measure F)

Tactic:
⟨f.continuous.measurable, ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk, Continuous.measurable, LinearIsometryEquiv.continuous
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
refine :
  Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)
⊢ MeasurePreserving.{u_2, u_3} (α := E) (β := F) (⇑f : (a : E) → F) (volume : Measure E) (volume : Measure F)

Tactic:
refine ⟨f.continuous.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
rcases :
  ∀ (w : Finset E) (b : OrthonormalBasis ↥w ℝ E)
    (_hw : Eq (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))),
    Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
      (volume : Measure F)
⊢ Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)

Tactic:
rcases exists_orthonormalBasis ℝ E with ⟨w, b, _hw⟩

Premises used: Real, exists_orthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : Eq (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))
erw : Eq (α := Measure F) (b.toBasis.map (↑(↑f : E ≃L[ℝ] F) : E ≃ₗ[ℝ] F)).addHaar (b.map f).toBasis.addHaar
⊢ Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)

Tactic:
erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f),
    Basis.map_addHaar _ f.toContinuousLinearEquiv]

Premises used: OrthonormalBasis.map, LinearIsometryEquiv.toContinuousLinearEquiv, Module.Basis.map_addHaar, OrthonormalBasis.addHaar_eq_volume
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : Eq (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))
⊢ Eq (α := Measure F) (b.toBasis.map (↑(↑f : E ≃L[ℝ] F) : E ≃ₗ[ℝ] F)).addHaar (b.map f).toBasis.addHaar

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
this :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
this
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
this :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
h :
  Eq (α := WithLp 2 (U × V) ≃ᵐ U × V) (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)))
    (volumePreservingSymmMeasurableEquivToLpProdAux U V)
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V))) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
convert! this
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
this :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
h :
  ∀ (uv : WithLp 2 (U × V)),
    Eq.{u_4 + 1} (α := U)
      ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).1
      ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).1
h₁ :
  ∀ (uv : WithLp 2 (U × V)),
    Eq.{u_5 + 1} (α := V)
      ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).2
      ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).2
⊢ Eq (α := WithLp 2 (U × V) ≃ᵐ U × V) (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)))
    (volumePreservingSymmMeasurableEquivToLpProdAux U V)

Tactic:
ext uv
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
this :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
uv : WithLp 2 (U × V)
⊢ Eq.{u_4 + 1} (α := U) ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).1
    ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).1

Tactic:
simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      LinearEquiv.prodCongr_symm, MeasurableEquiv.prodCongr]

Premises used: _private.0.volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi, MeasurableEquiv.prodCongr, LinearEquiv.prodCongr_symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
this :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
uv : WithLp 2 (U × V)
⊢ Eq.{u_5 + 1} (α := V) ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).2
    ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).2

Tactic:
simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      LinearEquiv.prodCongr_symm, MeasurableEquiv.prodCongr]

Premises used: _private.0.volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi, MeasurableEquiv.prodCongr, LinearEquiv.prodCongr_symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
suffices :
  MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V))) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
suffices MeasurePreserving (volumePreservingSymmMeasurableEquivToLpProdAux U V) by
    convert! this
    ext uv
    <;> simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      LinearEquiv.prodCongr_symm, MeasurableEquiv.prodCongr]
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
(LinearIsometryEquiv.measurePreserving _).trans ?_

Premises used: MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine :
  MeasurePreserving (α := WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.trans
          (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)))
          (MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
            (MeasurableEquiv.prodCongr
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))))) :
      (a : WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) → U × V)
    volume (volume : Measure (U × V))
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
refine (LinearIsometryEquiv.measurePreserving _).trans ?_

Premises used: MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.trans
          (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)))
          (MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
            (MeasurableEquiv.prodCongr
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))))) :
      (a : WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) → U × V)
    volume (volume : Measure (U × V))

Tactic:
(EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).trans ?_

Premises used: EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine :
  MeasurePreserving (α := Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) (β := U × V)
    (⇑(MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
          (MeasurableEquiv.prodCongr
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))))))) :
      (a : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) → U × V)
    volume (volume : Measure (U × V))
⊢ MeasurePreserving (α := WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.trans
          (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)))
          (MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
            (MeasurableEquiv.prodCongr
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
              (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
                (LinearIsometryEquiv.toMeasurableEquiv
                  (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))))) :
      (a : WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) → U × V)
    volume (volume : Measure (U × V))

Tactic:
refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).trans ?_

Premises used: EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) (β := U × V)
    (⇑(MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
          (MeasurableEquiv.prodCongr
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))))))) :
      (a : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) → U × V)
    volume (volume : Measure (U × V))

Tactic:
(measurePreserving_sumPiEquivProdPi _).trans ?_

Premises used: MeasureTheory.measurePreserving_sumPiEquivProdPi, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine :
  MeasurePreserving (α := ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.prodCongr
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) → U × V)
    (Measure.prod (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume)
      (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume))
    (volume : Measure (U × V))
⊢ MeasurePreserving (α := Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) (β := U × V)
    (⇑(MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) ↦ ℝ)
          (MeasurableEquiv.prodCongr
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
            (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
              (LinearIsometryEquiv.toMeasurableEquiv
                (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V))))))) :
      (a : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) → U × V)
    volume (volume : Measure (U × V))

Tactic:
refine (measurePreserving_sumPiEquivProdPi _).trans ?_

Premises used: MeasureTheory.measurePreserving_sumPiEquivProdPi, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.prodCongr
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) → U × V)
    (Measure.prod (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume)
      (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume))
    (volume : Measure (U × V))

Tactic:
MeasurePreserving.prod ?_ ?_

Premises used: MeasureTheory.MeasurePreserving.prod, Prod.map