awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
φ ψ : G ≃ₜ* G
hφ : Measurable (α := G) (β := G) (⇑φ : (a : G) → G)
hψ : Measurable (α := G) (β := G) (⇑ψ : (a : G) → G)
h_reg : Regular (α := G) (map (α := G) (⇑ψ : (a : G) → G) haar)
rw :
  haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) *
      haarScalarFactor (G := G) (map (α := G) (⇑ψ : (a : G) → G) haar)
        (map (α := G) (⇑φ : (a : G) → G) (map (α := G) (⇑ψ : (a : G) → G) haar)) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
rw₁ rw₂ :
  haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) (map (α := G) (⇑ψ : (a : G) → G) haar)) =
    haarScalarFactor (G := G) haar (map (α := G) (⇑ψ : (a : G) → G) haar) * mulEquivHaarChar φ

Tactic:
rw [MeasureTheory.Measure.haarScalarFactor_eq_mul haar (haar.map ψ),
    ← mulEquivHaarChar_eq (haar.map ψ)]

Premises used: MeasureTheory.mulEquivHaarChar_eq, MeasureTheory.Measure.haar, MeasureTheory.Measure.map, MeasureTheory.Measure.haarScalarFactor_eq_mul, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
φ : G ≃ₜ* G
symm : (mulEquivHaarChar φ)⁻¹ = mulEquivHaarChar φ.symm
⊢ mulEquivHaarChar φ.symm = (mulEquivHaarChar φ)⁻¹

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
φ : G ≃ₜ* G
a : mulEquivHaarChar φ * mulEquivHaarChar φ.symm = 1
⊢ (mulEquivHaarChar φ)⁻¹ = mulEquivHaarChar φ.symm

Tactic:
apply inv_eq_of_mul_eq_one_right

Premises used: inv_eq_of_mul_eq_one_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ * mulEquivHaarChar φ.symm = 1

Tactic:
simp [← mulEquivHaarChar_trans]

Premises used: MeasureTheory.mulEquivHaarChar_trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
⊢ Set.Nonempty.{u_1} (α := G) (interior (Compacts.carrier { carrier := univ, isCompact' := ⋯ }))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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' := ⋯ }
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
have hμ : μ univ = 1 := haarMeasure_self
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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 : μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ) = 1
⊢ mulEquivHaarChar φ = 1

Tactic:
rw [mulEquivHaarChar_eq μ]

Premises used: MeasureTheory.mulEquivHaarChar_eq
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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∞)
this : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
⊢ μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ) = 1

Tactic:
exact_mod_cast this
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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∞)
suffices : (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 1
⊢ μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ) = 1

Tactic:
suffices (μ.haarScalarFactor (map φ μ) : ℝ≥0∞) = 1 by exact_mod_cast this
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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 :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) 1
rw₁ :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) * 1
rw₂ rw₃ :
  (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞)
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) 1

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, mul_one]

Premises used: ENNReal.smul_def, smul_eq_mul, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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∞)
rw₂ rw₃ :
  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) μ)) 1 =
    HSMul.hSMul (β := ℝ≥0∞) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ))
      (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [map_apply (map_continuous φ).measurable .univ, Set.preimage_univ, hμ]

Premises used: MeasureTheory.Measure.map_apply, Continuous.measurable, Set.preimage_univ, ContinuousMapClass.map_continuous, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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) μ))
    (((map (⇑φ : (a : G) → G) μ : Measure G) : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞)
| (μ : (a : Set G) → ℝ≥0∞) univ

Tactic:
rw [isMulInvariant_eq_smul_of_compactSpace μ (map φ μ), Measure.smul_apply]

Premises used: MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.map, MeasureTheory.Measure.smul_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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
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∞)
⊢ 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]

Premises used: MeasureTheory.Measure.isMulInvariant_eq_smul_of_compactSpace, MeasureTheory.Measure.map, MeasureTheory.Measure.smul_apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
hμ
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
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∞)
_₂ :
  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
⊢ (↑(μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) : ℝ≥0∞) = 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μ

Premises used: Set.univ, MeasureTheory.Measure.map, OfNat.ofNat, DFunLike.coe, MeasureTheory.Measure.haarScalarFactor
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
inst_3 : FiniteDimensional ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
⊢ NoAtoms μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
Goal:
𝕜 : Type u_1
G : Type u_2
H : Type u_3
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : NontriviallyNormedField 𝕜
inst_3 : TopologicalSpace G
inst_4 : TopologicalSpace H
inst_5 : AddCommGroup G
inst_6 : AddCommGroup H
inst_7 : IsTopologicalAddGroup G
inst_8 : IsTopologicalAddGroup H
inst_9 : Module 𝕜 G
inst_10 : Module 𝕜 H
μ : Measure G
inst_11 : μ.IsAddHaarMeasure
inst_12 : BorelSpace G
inst_13 : BorelSpace H
inst_14 : CompleteSpace 𝕜
inst_15 : T2Space G
inst_16 : FiniteDimensional 𝕜 G
inst_17 : ContinuousSMul 𝕜 G
inst_18 : ContinuousSMul 𝕜 H
inst_19 : T2Space H
e : G ≃ₗ[𝕜] H
⊢ IsAddHaarMeasure.{u_3} (G := H) (map (⇑e : (a : G) → H) μ)

Tactic:
e.toContinuousLinearEquiv.isAddHaarMeasure_map _

Premises used: ContinuousLinearEquiv.isAddHaarMeasure_map, LinearEquiv.toContinuousLinearEquiv
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)
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
⊢ ∃ (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∞)

Tactic:
by_contra!
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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∞)
⊢ 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

Premises used: Set.inter_univ, MeasureTheory.measure_iUnion_null_iff, Metric.iUnion_ball_nat, Set.inter_iUnion, Set.preimage_univ, Set.preimage_iUnion, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 : Eq (α := ℝ≥0∞) (((haar : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty

Premises used: Eq.not_gt, isOpen_interior, TopologicalSpace.PositiveCompacts.interior_nonempty, IsOpen.measure_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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 : Eq (α := ℝ≥0∞) (((haar : Measure G) : (a : Set G) → ℝ≥0∞) (interior (↑K : Set G)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
exact this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty

Premises used: Eq.not_gt, isOpen_interior, TopologicalSpace.PositiveCompacts.interior_nonempty, IsOpen.measure_pos
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)
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)
⊢ ∃ 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
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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∞)
rw : ∃ s ∈ 𝓝 (HSMul.hSMul (β := G) x 1), Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)

Tactic:
rw [← mul_one x, ← smul_eq_mul]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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)

Tactic:
⟨_, 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,
    ?_⟩

Premises used: interior_subset, MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top, isOpen_interior, mt, HasSubset.Subset.trans, IsOpen.measurableSet, Set.inter_subset_left, smul_mem_nhds_smul, MeasureTheory.measure_mono_top, MeasureTheory.Measure.haar, measurableSet_ball, And.intro, Exists.intro, TopologicalSpace.PositiveCompacts.isCompact, IsCompact.measure_ne_top, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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∞)
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 : ℝ))))))
⊢ ∃ s ∈ 𝓝 (HSMul.hSMul (β := G) x 1), Bornology.IsBounded.{u_2} (α := H) ((⇑f : (a : G) → H) '' s)

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,
    ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace
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) '' (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 _ _