awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
hG : LocallyCompactSpace G
⊢ μ.haarScalarFactor μ = 1
have pos : ∀ (g : C(G, ℝ))
  (hg :
    HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
      LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  μ.haarScalarFactor μ = 1
Tactic: obtain ⟨g, hg⟩ := exists_continuous_nonneg_pos (1 : G)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ μ.haarScalarFactor μ = 1
have int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
Tactic: have int_g_ne_zero : ∫ x, g x ∂μ ≠ 0 :=
    ne_of_gt (g.2.integral_pos_of_hasCompactSupport_nonneg_nonzero hg.1 hg.2.1 hg.2.2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ : Measure G
inst_5 : μ.IsHaarMeasure
hG : LocallyCompactSpace G
g : C(G, ℝ)
hg :
  HasCompactSupport (α := G) (β := ℝ) (⇑g : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑g : (a : G) → ℝ) ∧ Ne (α := ℝ) ((g : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_g_ne_zero : Ne (α := ℝ) (∫ (x : G), (g : (a : G) → ℝ) x ∂μ) 0
⊢ μ.haarScalarFactor μ = 1
have pos : (↑(μ.haarScalarFactor μ) : ℝ) = (↑1 : ℝ)
Tactic: apply NNReal.coe_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have pos : ∀ (hG : LocallyCompactSpace G), μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
Tactic: by_cases hG : LocallyCompactSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
pos : ∀ (hG : LocallyCompactSpace G), μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have neg : ∀ (hG : ¬LocallyCompactSpace G), μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
Tactic: by_cases hG : LocallyCompactSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have pos : ∀ (g : G → ℝ) (g_cont : Continuous[inst, _] g)
  (g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ))
  (g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) })
  (g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
Tactic: obtain ⟨⟨g, g_cont⟩, g_comp, g_nonneg, g_one⟩ :
    ∃ (g : C(G, ℝ)), HasCompactSupport g ∧ 0 ≤ g ∧ g 1 ≠ 0 := exists_continuous_nonneg_pos 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have Z : Eq (α := ℝ) (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ'.haarScalarFactor μ • μ)
Tactic: have Z := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ g_cont g_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Z : Eq (α := ℝ) (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ'.haarScalarFactor μ • μ)
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have Z₁ : HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
Tactic: simp only [integral_smul_nnreal_measure, smul_smul,
    integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' ν g_cont g_comp,
    integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ ν g_cont g_comp] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)
have apply : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞)
      (support (M := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont })) :
    ℝ≥0∞)
Tactic: apply (integral_pos_iff_support_of_nonneg g_nonneg _).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
apply :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞)
        (support (M := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont })) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)
have apply₁ : Integrable (ε := ℝ) ((fun (f : C(G, ℝ)) ↦ f.toFun) { toFun := g, continuous_toFun := g_cont }) ν
Tactic: apply (integral_pos_iff_support_of_nonneg g_nonneg _).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)
Tactic: have int_g_pos : 0 < ∫ x, g x ∂ν := by
    apply (integral_pos_iff_support_of_nonneg g_nonneg _).2
    · exact IsOpen.measure_pos ν g_cont.isOpen_support ⟨1, g_one⟩
    · exact g_cont.integrable_of_hasCompactSupport g_comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ ν : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : ν.IsHaarMeasure
inst_7 : IsFiniteMeasureOnCompacts μ'
inst_8 : μ'.IsMulLeftInvariant
hG : LocallyCompactSpace G
g : G → ℝ
g_cont : Continuous[inst, _] g
g_comp : HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ)
g_nonneg : 0 ≤ { toFun := g, continuous_toFun := g_cont : C(G, ℝ) }
g_one : Ne (α := ℝ) (({ toFun := g, continuous_toFun := g_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
Z :
  HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor ν) (∫ (x : G), g x ∂ν) =
    HSMul.hSMul (β := ℝ) (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) (∫ (x : G), g x ∂ν)
int_g_pos : LT.lt (α := ℝ) 0 (∫ (x : G), g x ∂ν)
⊢ μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
have Z₁ : (↑(μ'.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν =
  (↑(μ'.haarScalarFactor μ * μ.haarScalarFactor ν) : ℝ) * ∫ (x : G), g x ∂ν
Tactic: change (haarScalarFactor μ' ν : ℝ) * ∫ (x : G), g x ∂ν =
    (haarScalarFactor μ' μ * haarScalarFactor μ ν : ℝ≥0) * ∫ (x : G), g x ∂ν at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have pos : ∀ (hG : LocallyCompactSpace G),
  haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
Tactic: by_cases hG : LocallyCompactSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
pos :
  ∀ (hG : LocallyCompactSpace G),
    haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have neg : ∀ (hG : ¬LocallyCompactSpace G),
  haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
Tactic: by_cases hG : LocallyCompactSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have pos : ∀ (f : G → ℝ) (f_cont : Continuous[inst, _] f)
  (hf :
    HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
        Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)),
  haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
Tactic: obtain ⟨⟨f, f_cont⟩, hf⟩ := exists_continuous_nonneg_pos (1 : G)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
Tactic: have int_f_ne_zero : ∫ (x : G), f x ∂(map φ μ) ≠ 0 :=
    ne_of_gt (f_cont.integral_pos_of_hasCompactSupport_nonneg_nonzero hf.1 hf.2.1 hf.2.2)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have pos : HDiv.hDiv (α := ℝ)
    (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ')
    (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ) =
  HDiv.hDiv (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ')
    (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ)
Tactic: rw [← NNReal.coe_inj, haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hf,
    haarScalarFactor_eq_integral_div μ' μ (f_cont.comp φ.continuous),
    integral_map (by fun_prop) (by fun_prop),
    integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
pos :
  HDiv.hDiv (α := ℝ)
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ')
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ')
      (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ)
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have pos₁ : HasCompactSupport (α := G) (f ∘ (⇑φ.toHomeomorph : (a : G) → G))
Tactic: rw [← NNReal.coe_inj, haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hf,
    haarScalarFactor_eq_integral_div μ' μ (f_cont.comp φ.continuous),
    integral_map (by fun_prop) (by fun_prop),
    integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
pos :
  HDiv.hDiv (α := ℝ)
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ')
      (∫ (x : G), ({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ((φ : (a : G) → G) x : G) ∂μ) =
    HDiv.hDiv (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ')
      (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ)
pos₁ : HasCompactSupport (α := G) (f ∘ (⇑φ.toHomeomorph : (a : G) → G))
⊢ haarScalarFactor (G := G) (map (⇑φ : (a : G) → G) μ') (map (⇑φ : (a : G) → G) μ) = μ'.haarScalarFactor μ
have pos₂ : Ne (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ) 0
Tactic: rw [← NNReal.coe_inj, haarScalarFactor_eq_integral_div_of_continuous_nonneg_pos _ _ hf,
    haarScalarFactor_eq_integral_div μ' μ (f_cont.comp φ.continuous),
    integral_map (by fun_prop) (by fun_prop),
    integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst, _] f
hf :
  HasCompactSupport (α := G) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
    LE.le (α := (a : G) → ℝ) 0 (⇑{ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) ∧
      Ne (α := ℝ) (({ toFun := f, continuous_toFun := f_cont : C(G, ℝ) } : (a : G) → ℝ) 1 : ℝ) (0 : ℝ)
int_f_ne_zero : Ne (α := ℝ) (@integral _ _ _ _ inst_3 (map (⇑φ : (a : G) → G) μ) fun (x : G) ↦ f x) 0
⊢ Ne (α := ℝ) (∫ (x : G), (f ∘ (⇑φ.toHomeomorph : (a : G) → G)) x ∂μ) 0
have pos : Ne (α := ℝ) (∫ (x : G), f ((φ : (a : G) → G) x) ∂μ) 0
Tactic: change ∫ x, f (φ x) ∂μ ≠ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have obtain : ∀ (u : ℕ → ℝ) (u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)) (u_lim : Tendsto u atTop (𝓝 0)),
  (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
Tactic: obtain ⟨u, -, u_mem, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo 0 1)
    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ) < 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
n : ℕ
⊢ Continuous[inst, _] (v n ∘ f)
have apply : Continuous[_, induced Subtype.val PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (⇑(thickenedIndicator sorry {1}) : (a : ℝ) → ℝ≥0)
Tactic: apply Continuous.comp (continuous_induced_dom.comp ?_) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : BorelSpace G
μ' μ : Measure G
inst_5 : μ.IsHaarMeasure
inst_6 : IsFiniteMeasureOnCompacts μ'
inst_7 : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioo 0 1) (u n)
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun (n : ℕ) (x : ℝ) ↦ (↑((thickenedIndicator ⋯ {1} : (a : ℝ) → ℝ≥0) x) : ℝ)
⊢ (μ' : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) =
    HSMul.hSMul (β := ℝ≥0∞) (μ'.haarScalarFactor μ) ((μ : (a : Set G) → ℝ≥0∞) (f ⁻¹' {1}) : ℝ≥0∞)
have vf_cont : ∀ (n : ℕ), Continuous[inst, _] (v n ∘ f)
Tactic: have vf_cont n : Continuous ((v n) ∘ f) := by
    apply Continuous.comp (continuous_induced_dom.comp ?_) hf
    exact BoundedContinuousFunction.continuous (thickenedIndicator (u_mem n).left {1})