awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞) (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
have suffices : LT.lt (α := ℝ≥0∞)
  ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: suffices μH[finrank ℝ E] (e '' K) < ⊤ by
      rw [← e.symm_image_image K]
      apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)
      rw [ENNReal.rpow_natCast]
      exact ENNReal.mul_lt_top (ENNReal.pow_lt_top ENNReal.coe_lt_top) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)
have a : μH[(↑(finrank ℝ E) : ℝ)]
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[(↑(finrank ℝ E) : ℝ)]
have a : (↑(finrank ℝ E) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| (↑(finrank ℝ E) : ℝ)
have a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
Tactic: rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)
have a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
Tactic: congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have conv_lhs : LT.lt (α := ℝ≥0∞)
  ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
      ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: conv_lhs => congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞)
  ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [hausdorffMeasure_pi_real]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ Ne (α := ℝ≥0∞) (((μH[(↑(finrank ℝ E) : ℝ)] : Measure E) : (a : Set E) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have suffices : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)
Tactic: suffices 0 < μH[finrank ℝ E] (e '' U) from
      (ENNReal.mul_pos_iff.mp (lt_of_lt_of_le this <|
        e.lipschitz.hausdorffMeasure_image_le (by simp) _)).2.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)
have a : μH[(↑(finrank ℝ E) : ℝ)]
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[(↑(finrank ℝ E) : ℝ)]
have a : (↑(finrank ℝ E) : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| (↑(finrank ℝ E) : ℝ)
have a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
Tactic: rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)
have a : (↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)
Tactic: congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(finrank ℝ E) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)
have conv_rhs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
      ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
    ℝ≥0∞)
Tactic: conv_rhs => congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μH[(↑(Fintype.card (Fin (finrank ℝ E))) : ℝ)] : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞)
        ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) :
      ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) : ℝ≥0∞)
Tactic: rw [hausdorffMeasure_pi_real]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst : EMetricSpace X
inst_1 : EMetricSpace Y
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : MeasurableSpace Y
inst_5 : BorelSpace Y
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℝ E
inst_8 : FiniteDimensional ℝ E
inst_9 : MeasurableSpace E
inst_10 : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((volume : (a : Set (Fin (finrank ℝ E) → ℝ)) → ℝ≥0∞) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U) : ℝ≥0∞)
have apply : Set.Nonempty (α := Fin (finrank ℝ E) → ℝ) ((⇑e : (a : E) → Fin (finrank ℝ E) → ℝ) '' U)
Tactic: apply (e.isOpenMap U hU).measure_pos (μ := volume)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
⊢ Eq (α := Measure ℝ) μH[1] volume
have rw : Eq (α := Measure ℝ) μH[1]
  (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
Tactic: rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure ℝ) μH[1]
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
⊢ Eq (α := Measure ℝ) μH[1] volume
have rw₁ : Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
  (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
Tactic: rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure ℝ) μH[1]
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₁ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
⊢ Eq (α := Measure ℝ) μH[1] volume
have rw₂ : Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
  (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ)
    μH[(↑(Fintype.card Unit) : ℝ)])
Tactic: rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure ℝ) μH[1]
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₁ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₂ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ)
      μH[(↑(Fintype.card Unit) : ℝ)])
⊢ Eq (α := Measure ℝ) μH[1] volume
have rw₃ : Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
  (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[(↑1 : ℝ)])
Tactic: rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure ℝ) μH[1]
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₁ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) volume)
rw₂ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ)
      μH[(↑(Fintype.card Unit) : ℝ)])
rw₃ :
  Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
    (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[(↑1 : ℝ)])
⊢ Eq (α := Measure ℝ) μH[1] volume
have rw₄ : Eq (α := Measure ℝ) (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
  (Measure.map (α := Unit → ℝ) (⇑(MeasurableEquiv.funUnique Unit ℝ) : (a : Unit → ℝ) → ℝ) μH[1])
Tactic: rw [← (volume_preserving_funUnique Unit ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_funUnique Unit ℝ 1).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_unit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume
have rw : Eq (α := Measure (ℝ × ℝ)) μH[2]
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    volume)
Tactic: rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure (ℝ × ℝ)) μH[2]
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume
have rw₁ : Eq (α := Measure (ℝ × ℝ))
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[2])
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    volume)
Tactic: rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure (ℝ × ℝ)) μH[2]
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₁ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume
have rw₂ : Eq (α := Measure (ℝ × ℝ))
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[2])
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[(↑(Fintype.card (Fin 2)) : ℝ)])
Tactic: rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure (ℝ × ℝ)) μH[2]
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₁ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₂ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
      μH[(↑(Fintype.card (Fin 2)) : ℝ)])
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume
have rw₃ : Eq (α := Measure (ℝ × ℝ))
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[2])
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[(↑2 : ℝ)])
Tactic: rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
rw :
  Eq (α := Measure (ℝ × ℝ)) μH[2]
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₁ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) volume)
rw₂ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
      μH[(↑(Fintype.card (Fin 2)) : ℝ)])
rw₃ :
  Eq (α := Measure (ℝ × ℝ))
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[2])
    (Measure.map (α := (i : Fin 2) → ℝ)
      (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ) μH[(↑2 : ℝ)])
⊢ Eq (α := Measure (ℝ × ℝ)) μH[2] volume
have rw₄ : Eq (α := Measure (ℝ × ℝ))
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[2])
  (Measure.map (α := (i : Fin 2) → ℝ) (⇑(MeasurableEquiv.piFinTwo fun (x : Fin 2) ↦ ℝ) : (a : (i : Fin 2) → ℝ) → ℝ × ℝ)
    μH[2])
Tactic: rw [← (volume_preserving_piFinTwo fun _ => ℝ).map_eq,
    ← (hausdorffMeasure_measurePreserving_piFinTwo (fun _ => ℝ) _).map_eq,
    ← hausdorffMeasure_pi_real, Fintype.card_fin, Nat.cast_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inl : ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
  HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: obtain rfl | hv := eq_or_ne v 0
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
v : E
s : Set ℝ
inl :
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∀ (hv : v ≠ 0),
  ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ r • v) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) ‖v‖₊ ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: obtain rfl | hv := eq_or_ne v 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Hausdorff (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
s : Set ℝ
⊢ ((μH[1] : Measure E) : (a : Set E) → ℝ≥0∞) ((fun (r : ℝ) ↦ HSMul.hSMul (β := E) r 0) '' s) =
    HSMul.hSMul (β := ℝ≥0∞) (nnnorm.{u_5} (E := E) 0) ((μH[1] : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have this : NoAtoms.{u_5} (α := E) (m0 := inst_2) μH[1]
Tactic: haveI := noAtoms_hausdorff E one_pos