awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      ((μ : (a : Set G) → ℝ≥0∞) (preimage (β := G) (⇑φ : (a : G) → G) univ) : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      ((μ : (a : Set G) → ℝ≥0∞) (preimage (β := G) (⇑φ : (a : G) → G) univ) : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₂ : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
Tactic: rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
| (μ : (a : Set G) → ℝ≥0∞) univ
have rw : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
  (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have conv_rhs : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
  (μ : (a : Set G) → ℝ≥0∞) univ
Tactic: conv_rhs => rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
conv_rhs :
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
⊢ HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
    (μ : (a : Set G) → ℝ≥0∞) univ
have conv_rhs₁ : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: conv_rhs => rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
have _ : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
Tactic: calc
    _ = μ.haarScalarFactor (map φ μ) • (1 : ℝ≥0∞) := by rw [ENNReal.smul_def, smul_eq_mul, mul_one]
    _ = μ.haarScalarFactor (map φ μ) • (map φ μ univ) := by
          rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]
    _ = μ univ := by
          conv_rhs => rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
    _ = 1 := hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
_ :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
have _₁ : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: calc
    _ = μ.haarScalarFactor (map φ μ) • (1 : ℝ≥0∞) := by rw [ENNReal.smul_def, smul_eq_mul, mul_one]
    _ = μ.haarScalarFactor (map φ μ) • (map φ μ univ) := by
          rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]
    _ = μ univ := by
          conv_rhs => rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
    _ = 1 := hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : CompactSpace G
φ : G ≃ₜ* G
μ : Measure G := haarMeasure { carrier := univ, isCompact' := ⋯, interior_nonempty' := ⋯ }
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
_ :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1
_₁ :
  HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
have _₂ : HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) =
  (μ : (a : Set G) → ℝ≥0∞) univ
Tactic: calc
    _ = μ.haarScalarFactor (map φ μ) • (1 : ℝ≥0∞) := by rw [ENNReal.smul_def, smul_eq_mul, mul_one]
    _ = μ.haarScalarFactor (map φ μ) • (map φ μ univ) := by
          rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]
    _ = μ univ := by
          conv_rhs => rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]
    _ = 1 := hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
⊢ ∃ (n : ℕ),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
      (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
        ℝ≥0∞)
have by_contra! : ∀
  (this :
    ∀ (n : ℕ),
      LE.le (α := ℝ≥0∞)
        (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
            (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
this :
  ∀ (n : ℕ),
    LE.le (α := ℝ≥0∞)
      (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ False
have this₁ : Eq (α := ℝ≥0∞) (((haar : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [nonpos_iff_eq_zero, ← measure_iUnion_null_iff, ← inter_iUnion, ← preimage_iUnion,
      iUnion_ball_nat, preimage_univ, inter_univ] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
have obtain : ∀ (n : ℕ)
  (hn :
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
      (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
        ℝ≥0∞)),
  ∃ s ∈ 𝓝 x, Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, 0 < haar (interior K ∩ f ⁻¹' ball 1 n) := by
    by_contra!
    simp_rw [nonpos_iff_eq_zero, ← measure_iUnion_null_iff, ← inter_iUnion, ← preimage_iUnion,
      iUnion_ball_nat, preimage_univ, inter_univ] at this
    exact this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
have rw : ∃ s ∈ 𝓝 (HSMul.hSMul (β := G) x 1), Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
Tactic: rw [← mul_one x, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
⊢ ∃ s ∈ 𝓝 (HSMul.hSMul (β := G) x 1), Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
have refine : Bornology.IsBounded.{u_2} (α := H)
  ((⇑f : (a : G) → H) ''
    (x •
      (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ)) /
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))
Tactic: refine ⟨_, smul_mem_nhds_smul _ <| div_mem_nhds_one_of_haar_pos_ne_top haar _
    (isOpen_interior.measurableSet.inter <| hf measurableSet_ball) hn <|
      mt (measure_mono_top <| inter_subset_left.trans interior_subset) K.isCompact.measure_ne_top,
    ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
⊢ Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) ''
      (x •
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ)) /
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))
have this : Bornology.IsBounded.{u_2} (α := H)
  ((⇑f : (a : G) → H) '' (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
Tactic: have : Bornology.IsBounded (f '' (interior K ∩ f ⁻¹' ball 1 n)) :=
    isBounded_ball.subset <| (image_mono inter_subset_right).trans <| image_preimage_subset _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : IsTopologicalGroup G
inst_4 : BorelSpace G
inst_5 : LocallyCompactSpace G
inst_6 : MeasurableSpace H
inst_7 : SeminormedGroup H
inst_8 : OpensMeasurableSpace H
f : G →* H
hf : Measurable.{u_1, u_2} (α := G) (β := H) (⇑f : (a : G) → H)
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    (((haar : Measure G) : (a : Set G) → ℝ≥0∞)
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))) :
      ℝ≥0∞)
this :
  Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) '' (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
⊢ Bornology.IsBounded.{u_2} (α := H)
    ((⇑f : (a : G) → H) ''
      (x •
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ)) /
          (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))
have rw : Bornology.IsBounded
  (HSMul.hSMul (α := H) ((f : (a : G) → H) x : H)
    (HDiv.hDiv (α := Set H)
      ((⇑f : (a : G) → H) ''
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))
      ((⇑f : (a : G) → H) ''
        (interior (↑K : Set G) ∩ preimage.{u_1, u_2} (β := H) (⇑f : (a : G) → H) (ball 1 (↑n : ℝ))))))
Tactic: rw [image_smul_distrib, image_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
have pos : ∀ (hF : CompleteSpace F), ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
pos : ∀ (hF : CompleteSpace F), ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
have neg : ∀ (hF : ¬CompleteSpace F), ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
Tactic: by_cases hF : CompleteSpace F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hF : CompleteSpace F
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
have pos : ∫ (x : E), f (HSMul.hSMul (α := ℝ) 0 x) ∂μ =
  HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
R : ℝ
hF : CompleteSpace F
pos :
  ∫ (x : E), f (HSMul.hSMul (α := ℝ) 0 x) ∂μ =
    HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
⊢ ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
have pos₁ : ∀ (hR : R ≠ 0), ∫ (x : E), f (R • x) ∂μ = HSMul.hSMul (β := F) |(R ^ finrank ℝ E)⁻¹| (∫ (x : E), f x ∂μ)
Tactic: rcases eq_or_ne R 0 with (rfl | hR)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
⊢ ∫ (x : E), f (HSMul.hSMul (α := ℝ) 0 x) ∂μ =
    HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have pos : μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
Tactic: simp only [zero_smul, integral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have pos : ∀ (hE : finrank ℝ E = 0),
  μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
Tactic: rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
pos :
  ∀ (hE : finrank ℝ E = 0),
    μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have pos₁ : ∀ (hE : finrank ℝ E > 0),
  μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
Tactic: rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
⊢ μ.real univ • f 0 = HSMul.hSMul (β := F) |(HPow.hPow (α := ℝ) 0 (finrank ℝ E))⁻¹| (∫ (x : E), f x ∂μ)
have this : Subsingleton E
Tactic: have : Subsingleton E := finrank_zero_iff.1 hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
this : Subsingleton E
⊢ f = fun (x : E) ↦ f 0
have h : ∀ (x : E), f x = f 0
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (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 : Type u_2
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
f : E → F
hF : CompleteSpace F
hE : finrank ℝ E = 0
this : Subsingleton E
x : E
⊢ f x = f 0
have h : f 0 = f 0
Tactic: rw [Subsingleton.elim x 0]