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 : Set E
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : E),
      (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
          ((μ : (a : Set E) → ℝ≥0∞) (closedBall x ε) : ℝ≥0∞)
have h : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioi 0) r) (x : E),
  (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin] with r hr x
-- 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 : Set E
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
x : E
⊢ (μ : (a : Set E) → ℝ≥0∞) (closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h : HMul.hMul (β := ℝ≥0∞) (↑(Real.toNNReal 2 ^ finrank ℝ E) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑(HPow.hPow (α := ℝ≥0) 2 (finrank ℝ E)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 r) : ℝ≥0∞)
Tactic: rw [addHaar_closedBall_mul μ x zero_le_two (le_of_lt hr), addHaar_closedBall_center μ x,
    ENNReal.ofReal, Real.toNNReal_pow zero_le_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have this : FiniteDimensional ℝ G
Tactic: have : FiniteDimensional ℝ G := b.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
have rw : parallelepiped v =
  parallelepiped.{u_2, u_3} (ι := ι)
    (Function.comp (β := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G) (⇑b : (a : ι) → G))
Tactic: rw [image_parallelepiped]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have A : parallelepiped v =
  image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
    (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
Tactic: have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by
    rw [image_parallelepiped]
    exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw : ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
    (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
  ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₁ : HMul.hMul (β := ℝ≥0∞)
    (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
    (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
  ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₂ : ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
  ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₂ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₃ : ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| =
  ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₂ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₃ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₄ : ENNReal.ofReal
    |Matrix.det.{0, u_2} (n := ι)
        ((LinearMap.toMatrix b b : (a : G →ₗ[ℝ] G) → Matrix ι ι ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v))| =
  ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₂ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₃ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₄ :
  ENNReal.ofReal
      |Matrix.det.{0, u_2} (n := ι)
          ((LinearMap.toMatrix b b : (a : G →ₗ[ℝ] G) → Matrix ι ι ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v))| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₅ : ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
ι : Type u_2
G : Type u_3
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A :
  parallelepiped v =
    image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
      (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))
rw :
  ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞)
      (image (α := G) (⇑((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G) : (a : G) → G)
        (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G))) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₁ :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)|)
      (((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped.{u_2, u_3} (ι := ι) (⇑b : (a : ι) → G)) : ℝ≥0∞) =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₂ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| * 1 =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₃ :
  ENNReal.ofReal |(LinearMap.det : (a : G →ₗ[ℝ] G) → ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v : G →ₗ[ℝ] G)| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₄ :
  ENNReal.ofReal
      |Matrix.det.{0, u_2} (n := ι)
          ((LinearMap.toMatrix b b : (a : G →ₗ[ℝ] G) → Matrix ι ι ℝ) ((b.constr ℕ : (a : ι → G) → G →ₗ[ℝ] G) v))| =
    ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
rw₅ : ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
⊢ ((b.addHaar : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(b.det : (a : ι → G) → ℝ) v|
have rw₆ : ENNReal.ofReal |(b.toMatrix v).det| = ENNReal.ofReal |(b.toMatrix v).det|
Tactic: rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
    ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
| ENNReal.ofReal |(ω : (a : Fin n → G) → ℝ) v|
have rw : ENNReal.ofReal
  |(HSMul.hSMul (α := ℝ) (β := G [⋀^Fin n]→ₗ[ℝ] ℝ)
          ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G sorry) : (a : Fin n) → G) : ℝ)
          (Basis.det (finBasisOfFinrankEq ℝ G sorry)) :
        (a : Fin n → G) → ℝ)
      v|
Tactic: rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
Goal:
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
v : Fin n → G
⊢ ((ω.measure : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) = ENNReal.ofReal |(ω : (a : Fin n → G) → ℝ) v|
have conv_rhs : ((ω.measure : Measure G) : (a : Set G) → ℝ≥0∞) (parallelepiped v) =
  ENNReal.ofReal
    |(HSMul.hSMul (α := ℝ) (β := G [⋀^Fin n]→ₗ[ℝ] ℝ)
            ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G sorry) : (a : Fin n) → G) : ℝ)
            (Basis.det (finBasisOfFinrankEq ℝ G sorry)) :
          (a : Fin n → G) → ℝ)
        v|
Tactic: conv_rhs => rw [ω.eq_smul_basis_det (finBasisOfFinrankEq ℝ G _i.out)]
-- 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 : Set E
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ IsAddLeftInvariant ω.measure
have rw : (HSMul.hSMul (β := Measure G)
    (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G sorry) : (a : Fin n) → G) : ℝ))
    (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G sorry))).IsAddLeftInvariant
Tactic: rw [AlternatingMap.measure]
-- 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 : Set E
ι : Type u_2
G : Type u_3
inst_6 : Fintype ι
inst_7 : DecidableEq ι
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : MeasurableSpace G
inst_11 : BorelSpace G
inst_12 : FiniteDimensional ℝ G
n : ℕ
_i : Fact (finrank ℝ G = n)
ω : G [⋀^Fin n]→ₗ[ℝ] ℝ
⊢ IsLocallyFiniteMeasure (m0 := inst_10) ω.measure
have rw : IsLocallyFiniteMeasure
  (HSMul.hSMul (β := Measure G)
    (nnnorm (E := ℝ) ((ω : (a : Fin n → G) → ℝ) (⇑(finBasisOfFinrankEq ℝ G sorry) : (a : Fin n) → G) : ℝ))
    (Basis.addHaar (ι := Fin n) (finBasisOfFinrankEq ℝ G sorry)))
Tactic: rw [AlternatingMap.measure]
-- 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 : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
have tendsto_of_tendsto_of_tendsto_of_le_of_le' : ∀ᶠ (b : ℝ) in 𝓝[>] 0,
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x b) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞)
Tactic: apply
      tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds h
        (Eventually.of_forall fun b => zero_le)
-- 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 : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + b • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞) ≤
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x b) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x b) : ℝ≥0∞)
have h₁ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) a →
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + a • t)) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞) ≤
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x a) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x a) : ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin]
-- 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 : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
r : ℝ
rpos : 0 < r
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + r • t)) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: grw [t_bound]
-- 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 : Set E
x : E
h :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
t_bound : t ⊆ closedBall 0 1
r : ℝ
rpos : 0 < r
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (s ∩ ({x} + HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have h₁ : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (s ∩ HVAdd.hVAdd (α := Set E) {x} (HSMul.hSMul (β := Set E) r (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞) ≤
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: rw [← vadd_eq_add, singleton_vadd, affinity_unitClosedBall rpos.le]