awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
inl :
  ∀ (hs : Ne.{u_1 + 1} (α := AffineSubspace ℝ E) ⊥ ⊤),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑⊥ : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
inr : ∀ (hne : (↑s : Set E).Nonempty), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases s.eq_bot_or_nonempty with (rfl | hne)

Premises used: AffineSubspace.eq_bot_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : Ne.{u_1 + 1} (α := AffineSubspace ℝ E) ⊥ ⊤
inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
inl₁ inl₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑⊥ : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [AffineSubspace.bot_coe, measure_empty]

Premises used: AffineSubspace.bot_coe, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : (↑s : Set E).Nonempty
⊢ ¬s.direction = ⊤

Tactic:
rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs

Premises used: AffineSubspace.direction_eq_top_iff_of_nonempty, Ne
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : (↑s : Set E).Nonempty
hs₁ : ¬s.direction = ⊤
⊢ (↑s : Set E).Nonempty

Tactic:
rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs

Premises used: AffineSubspace.direction_eq_top_iff_of_nonempty, Ne
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
hne : (↑s : Set E).Nonempty
inr : ∀ (x : E) (hx : x ∈ s), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases hne with ⟨x, hx : x ∈ s⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : AffineSubspace ℝ E
hs : ¬s.direction = ⊤
x : E
hx : x ∈ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg,
    image_add_right, neg_neg, measure_preimage_add_right] using addHaar_submodule μ s.direction hs

Premises used: sub_eq_add_neg, neg_neg, Set.image_add_right, MeasureTheory.Measure.addHaar_submodule, MeasureTheory.measure_preimage_add_right, vsub_eq_sub, AffineSubspace.direction, AffineSubspace.coe_direction_eq_vsub_set_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
μ : Measure (ι → ℝ)
inst_1 : μ.IsAddHaarMeasure
intro :
  ∀ (val : Fintype ι),
    map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
μ : Measure (ι → ℝ)
inst_1 : μ.IsAddHaarMeasure
val : Fintype ι
⊢ μ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (addHaarMeasure (piIcc01 ι))

Tactic:
have := addHaarMeasure_unique μ (piIcc01 ι)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
ι : Type u_1
inst : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
μ : Measure (ι → ℝ)
inst_1 : μ.IsAddHaarMeasure
val : Fintype ι
this :
  μ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (addHaarMeasure (piIcc01 ι))
intro :
  map (⇑f : (a : ι → ℝ) → ι → ℝ)
      (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (addHaarMeasure (piIcc01 ι))) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (addHaarMeasure (piIcc01 ι))
intro₁ :
  map (⇑f : (a : ι → ℝ) → ι → ℝ)
      (HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ))) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ))
intro₂ :
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (map (α := ι → ℝ) (⇑f : (a : ι → ℝ) → ι → ℝ) (volume : Measure (ι → ℝ))) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ))
intro₃ :
  HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
      (HSMul.hSMul (β := Measure (ι → ℝ)) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹|)
        volume) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ))
intro₄ intro₅ :
  ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| •
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ))
        ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞) (volume : Measure (ι → ℝ))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ

Tactic:
rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]

Premises used: MeasureTheory.addHaarMeasure_eq_volume_pi, Real.map_linearMap_volume_pi_eq_smul_volume_pi, MeasureTheory.Measure.map_smul, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
⊢ FiniteDimensional ℝ (ι → ℝ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
⊢ FiniteDimensional ℝ (ι → ℝ)

Tactic:
haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
simp [ι]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)

Tactic:
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [ι]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
have :
  ∀ (e : E ≃ₗ[ℝ] ι → ℝ), map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ

Tactic:
have e : E ≃ₗ[ℝ] ι → ℝ := LinearEquiv.ofFinrankEq E (ι → ℝ) this
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
⊢ ∃ (g : (ι → ℝ) →ₗ[ℝ] ι → ℝ), g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
obtain :
  ∀ (g : (ι → ℝ) →ₗ[ℝ] ι → ℝ) (hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)),
    map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ

Tactic:
obtain ⟨g, hg⟩ : ∃ g, g = (e : E →ₗ[ℝ] ι → ℝ).comp (f.comp (e.symm : (ι → ℝ) →ₗ[ℝ] E)) := ⟨_, rfl⟩

Premises used: LinearEquiv.symm, LinearMap.comp, LinearEquiv.toLinearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
rw :
  Eq (α := ℝ)
    ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) ((↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)) : ℝ)
    ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
⊢ Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)

Tactic:
rw [hg]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
⊢ Eq (α := ℝ)
    ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) ((↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)) : ℝ)
    ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)

Tactic:
LinearMap.det_conj f e

Premises used: LinearMap.det_conj
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
⊢ Eq (α := ℝ)
    ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) ((↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)) : ℝ)
    ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)

Tactic:
exact LinearMap.det_conj f e

Premises used: LinearMap.det_conj
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
⊢ Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)

Tactic:
have gdet : LinearMap.det g = LinearMap.det f := by rw [hg]; exact LinearMap.det_conj f e
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
rw :
  ∀ (hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ))
    (hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E))
    (gdet :
      Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ)
        ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)),
    map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ

Tactic:
rw [← gdet] at hf ⊢
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
h :
  ∀ (x : E),
    Eq (α := E) ((f : (a : E) → E) x : E)
      (((↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ) : (a : E) → E) x : E)
⊢ f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
x : E
⊢ Eq (α := E) ((f : (a : E) → E) x : E) (((↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ) : (a : E) → E) x : E)

Tactic:
simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
      LinearEquiv.symm_apply_apply, hg]

Premises used: LinearEquiv.symm_apply_apply, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
⊢ f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)

Tactic:
have fg : f = (e.symm : (ι → ℝ) →ₗ[ℝ] E).comp (g.comp (e : E →ₗ[ℝ] ι → ℝ)) := by
    ext x
    simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
      LinearEquiv.symm_apply_apply, hg]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
simp :
  map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ

Tactic:
simp only [fg, LinearEquiv.coe_coe, LinearMap.coe_comp]

Premises used: LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)

Tactic:
have Ce : Continuous e := (e : E →ₗ[ℝ] ι → ℝ).continuous_of_finiteDimensional
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
⊢ Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)

Tactic:
have Cg : Continuous g := LinearMap.continuous_of_finiteDimensional g
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)

Tactic:
have Cesymm : Continuous e.symm := (e.symm : (ι → ℝ) →ₗ[ℝ] E).continuous_of_finiteDimensional