awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
have this : LocallyCompactSpace G
Tactic: haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    1
have h0 : Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
h0 :
  Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞)
      ((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) =
    1
have ht : Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Regular (haarMeasure K₀)
have this : LocallyCompactSpace G
Tactic: haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Regular (haarMeasure K₀)
have hx : Ne (α := ℝ≥0∞) (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply Regular.smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ Ne (α := ℝ≥0∞) (((((haarContent K₀).measure : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G))⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
have hx : Ne (α := ℝ≥0∞) (((haarContent K₀).outerMeasure : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [K₀.isCompact.measure_closure, haarMeasure_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
rw : Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [K₀.isCompact.measure_closure, haarMeasure_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
⊢ SigmaFinite (m0 := inst_3) (haarMeasure K₀)
have this : LocallyCompactSpace G
Tactic: haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ IsHaarMeasure (haarMeasure K₀)
have h : Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply
    isHaarMeasure_of_isCompact_nonempty_interior (haarMeasure K₀) K₀ K₀.isCompact
      K₀.interior_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
h : Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsHaarMeasure (haarMeasure K₀)
have h' : Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply
    isHaarMeasure_of_isCompact_nonempty_interior (haarMeasure K₀) K₀ K₀.isCompact
      K₀.interior_nonempty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
K₀ : PositiveCompacts G
⊢ Ne (α := ℝ≥0∞) (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (0 : ℝ≥0∞)
have h : Ne (α := ℝ≥0∞) 1 0
Tactic: simp only [haarMeasure_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst_1] K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have obtain : ∀ (K : Set G) (hKE : K ⊆ E) (hK_comp : IsCompact K)
  (hK_meas : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
  ∃ K ⊆ E, IsCompact K ∧ IsClosed[inst_1] K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
Cleared hypotheses: hEapprox
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)
have obtain : ∀ (K : Set G) (hKE : K ⊆ E) (hK : IsCompact K) (K_closed : IsClosed[inst_1] K)
  (hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
  Membership.mem (γ := Filter G) (𝓝 1) (E / E)
Tactic: obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Membership.mem (γ := Filter G) (𝓝 1) (E / E)
have h : ∀ (g : G) (hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)),
  g ∈ E / E
Tactic: filter_upwards [eventually_nhds_one_measure_smul_diff_lt hK K_closed hKpos.ne' (μ := μ)] with g hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ.InnerRegularCompactLTTop
inst_7 : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst_1] K
hKpos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
g : G
hg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • K \ K) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
⊢ g ∈ E / E
have h : ∀ (x : G) (hxK : x ∈ K) (hgxK : (fun (x : G) ↦ g • x) x ∈ K), g ∈ E / E
Tactic: obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
have A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
Tactic: have A : Set.Nonempty (interior (closure (K₀ : Set G))) :=
    K₀.interior_nonempty.mono (interior_mono subset_closure)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
have this : μ =
  HSMul.hSMul (β := Measure G)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
      (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
    (haarMeasure K₀)
Tactic: have := measure_eq_div_smul μ (haarMeasure K₀)
    (measure_pos_of_nonempty_interior _ A).ne' K₀.isCompact.closure.measure_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
this :
  μ =
    HSMul.hSMul (β := Measure G)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
      (haarMeasure K₀)
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
have rwa : ∀
  (this :
    μ =
      HSMul.hSMul (β := Measure G)
        (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞) (1 : ℝ≥0∞))
        (haarMeasure K₀)),
  μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
Tactic: rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
this :
  μ =
    HSMul.hSMul (β := Measure G)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
      (haarMeasure K₀)
rwa :
  ∀
    (this :
      μ =
        HSMul.hSMul (β := Measure G)
          (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
            (1 : ℝ≥0∞))
          (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
have rwa₁ : ∀
  (this :
    μ =
      HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (haarMeasure K₀)),
  μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
Tactic: rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K₀ : PositiveCompacts G
A : (interior (closure[inst_1] (↑K₀ : Set G))).Nonempty
this :
  μ =
    HSMul.hSMul (β := Measure G)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
        (((haarMeasure K₀ : Measure G) : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞))
      (haarMeasure K₀)
rwa :
  ∀
    (this :
      μ =
        HSMul.hSMul (β := Measure G)
          (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
            (1 : ℝ≥0∞))
          (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
rwa₁ :
  ∀
    (this :
      μ =
        HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (closure[inst_1] (↑K₀ : Set G)) : ℝ≥0∞)
          (haarMeasure K₀)),
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
⊢ μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
have rwa₂ : ∀
  (this :
    μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)),
  μ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
Tactic: rwa [haarMeasure_closure_self, div_one, K₀.isCompact.measure_closure] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ haarMeasure K₀ = μ
have rw : haarMeasure K₀ =
  HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
Tactic: rw [haarMeasure_unique μ K₀, h, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  haarMeasure K₀ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
⊢ haarMeasure K₀ = μ
have rw₁ : haarMeasure K₀ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) 1 (haarMeasure K₀)
Tactic: rw [haarMeasure_unique μ K₀, h, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
K₀ : PositiveCompacts G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (1 : ℝ≥0∞)
rw :
  haarMeasure K₀ =
    HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) ((μ : (a : Set G) → ℝ≥0∞) (↑K₀ : Set G) : ℝ≥0∞) (haarMeasure K₀)
rw₁ : haarMeasure K₀ = HSMul.hSMul (α := ℝ≥0∞) (β := Measure G) 1 (haarMeasure K₀)
⊢ haarMeasure K₀ = μ
have rw₂ : Eq (α := Measure G) (haarMeasure K₀) (haarMeasure K₀)
Tactic: rw [haarMeasure_unique μ K₀, h, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
inst_5 : SecondCountableTopology G
μ : Measure G
inst_6 : SigmaFinite μ
inst_7 : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h2K : (interior K).Nonempty
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.Regular
have rw : (HSMul.hSMul (α := ℝ≥0∞) (β := Measure G)
    ((μ : (a : Set G) → ℝ≥0∞)
        (↑{ carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G } : Set G) :
      ℝ≥0∞)
    (haarMeasure { carrier := K, isCompact' := hK, interior_nonempty' := h2K : PositiveCompacts G })).Regular
Tactic: rw [haarMeasure_unique μ ⟨⟨K, hK⟩, h2K⟩]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
⊢ ∃ (c : ℝ≥0∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this : FiniteDimensional 𝕜 E
⊢ ProperSpace F
have inl : ∀ (hE : Subsingleton E), ProperSpace F
Tactic: rcases subsingleton_or_nontrivial E with hE | hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this : FiniteDimensional 𝕜 E
inl : ∀ (hE : Subsingleton E), ProperSpace F
⊢ ProperSpace F
have inr : ∀ (hE : Nontrivial E), ProperSpace F
Tactic: rcases subsingleton_or_nontrivial E with hE | hE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this : FiniteDimensional 𝕜 E
hE : Subsingleton E
⊢ ProperSpace F
have this₁ : Subsingleton F
Tactic: have : Subsingleton F := Function.Surjective.subsingleton h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this : FiniteDimensional 𝕜 E
hE : Nontrivial E
⊢ ProperSpace F
have this₁ : ProperSpace 𝕜
Tactic: have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this_1 : FiniteDimensional 𝕜 E
hE : Nontrivial E
this : ProperSpace 𝕜
⊢ ProperSpace F
have this₁ : FiniteDimensional 𝕜 F
Tactic: have : FiniteDimensional 𝕜 F := Module.Finite.of_surjective L h