awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
h : x = ((c ^ n - c ^ m)⁻¹ * (c ^ n - c ^ m)) • x
h₁ : x = HSMul.hSMul (α := ℝ) 1 x
⊢ x = (c ^ n - c ^ m)⁻¹ • (c ^ n - c ^ m) • x
have h₂ : x = x
Tactic: rw [smul_smul, inv_mul_cancel₀ H, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A_1 : Bornology.IsBounded.{u_1} (α := E) (range fun (n : ℕ) ↦ c ^ n • x)
m n : ℕ
hmn : m ≠ n
y : E
hym : -(c ^ m • x) + y ∈ s
hyn : -(c ^ n • x) + y ∈ s
A : (c ^ n - c ^ m) • x ∈ s
H : c ^ n - c ^ m ≠ 0
⊢ False
have this : x ∈ s
Tactic: have : x ∈ s := by
    convert! s.smul_mem (c ^ n - c ^ m)⁻¹ A
    rw [smul_smul, inv_mul_cancel₀ H, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 ≠ ⊤
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : ∀ (hs : Ne.{u_1 + 1} (α := AffineSubspace ℝ E) ⊥ ⊤),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑⊥ : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases s.eq_bot_or_nonempty with (rfl | hne)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (hne : (↑s : Set E).Nonempty), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases s.eq_bot_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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) ⊥ ⊤
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑⊥ : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [AffineSubspace.bot_coe, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑⊥ : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [AffineSubspace.bot_coe, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have hs₁ : ¬s.direction = ⊤
Tactic: rw [Ne, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs
Cleared hypotheses: hs, hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (x : E) (hx : x ∈ s), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (↑s : Set E) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases hne with ⟨x, hx : x ∈ s⟩
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_1
inst : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
μ : Measure (ι → ℝ)
inst_1 : μ.IsAddHaarMeasure
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have intro : ∀ (val : Fintype ι),
  map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f : ℝ) (0 : ℝ)
μ : Measure (ι → ℝ)
inst_1 : μ.IsAddHaarMeasure
val : Fintype ι
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have this : μ =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure (ι → ℝ)) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑(piIcc01 ι) : Set (ι → ℝ)) : ℝ≥0∞)
    (addHaarMeasure (piIcc01 ι))
Tactic: have := addHaarMeasure_unique μ (piIcc01 ι)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 ι))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have 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 ι))
Tactic: rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 ι))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have 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 (ι → ℝ))
Tactic: rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 (ι → ℝ))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have 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 (ι → ℝ))
Tactic: rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 (ι → ℝ))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have 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 (ι → ℝ))
Tactic: rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 (ι → ℝ))
⊢ map (⇑f : (a : ι → ℝ) → ι → ℝ) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) f)⁻¹| • μ
have 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 (ι → ℝ))
Tactic: rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
    Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have this : FiniteDimensional ℝ (ι → ℝ)
Tactic: haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 ℝ (ι → ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have this₁ : finrank ℝ E = finrank ℝ (ι → ℝ)
Tactic: have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [ι]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 ℝ (ι → ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have have : ∀ (e : E ≃ₗ[ℝ] ι → ℝ), map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
Tactic: have e : E ≃ₗ[ℝ] ι → ℝ := LinearEquiv.ofFinrankEq E (ι → ℝ) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 ≃ₗ[ℝ] ι → ℝ
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have obtain : ∀ (g : (ι → ℝ) →ₗ[ℝ] ι → ℝ) (hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)),
  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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : ℝ)
have rw : Eq (α := ℝ)
  ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) ((↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)) : ℝ)
  ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have gdet : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 : ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ
have 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)⁻¹| • μ
Tactic: rw [← gdet] at hf ⊢
Cleared hypotheses: hf, hg, gdet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 →ₗ[ℝ] ι → ℝ)
have h : ∀ (x : E),
  Eq (α := E) ((f : (a : E) → E) x : E) (((↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ) : (a : E) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have fg : 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]