awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ x * g) ⁻¹' s) : ℝ≥0∞)
    (((comap (⇑f : (a : G) → H) μ : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
repeat rw [hf.comap_apply]

Premises used: MeasurableEmbedding.comap_apply
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
h :
  ∀ (x : H),
    Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x ↔
      Membership.mem (γ := Set H)
        (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
⊢ Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
h :
  Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x →
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x
h₁ :
  Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x →
    Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x ↔
    Membership.mem (γ := Set H)
      (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s)) x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
y : G
hy : Membership.mem (γ := Set G) ((fun (x : G) ↦ x * g) ⁻¹' s) y
⊢ Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) (y * g) : H)
    ((fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((f : (a : G) → H) y) : H)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
y : G
hy : Membership.mem (γ := Set G) ((fun (x : G) ↦ x * g) ⁻¹' s) y
⊢ Membership.mem.{u_3, u_3} (α := H) (γ := Set H)
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
    ((f : (a : G) → H) y : H)

Tactic:
exact ⟨y * g, hy, by simp⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) x : H)
⊢ Membership.mem (γ := Set G) ((fun (x : G) ↦ x * g) ⁻¹' s) (y * g⁻¹)

Tactic:
simp [yins]
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) x : H)
⊢ (f : (a : G) → H) (y * g⁻¹) = x

Tactic:
simp [hy]
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
x : H
y : G
yins : y ∈ s
hy :
  Eq.{u_3 + 1} (α := H) ((f : (a : G) → H) y : H) ((fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) x : H)
⊢ Membership.mem (γ := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) x

Tactic:
exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))

Tactic:
have : f '' (· * g) ⁻¹' s = (· * f g) ⁻¹' f '' s := by
      ext
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact ⟨y * g, hy, by simp⟩
      · intro ⟨y, yins, hy⟩
        exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
⊢ Measurable (β := H) fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
h : MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set H) → ℝ≥0∞) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set H) → ℝ≥0∞) ((⇑f : (a : G) → H) '' s) : ℝ≥0∞)

Tactic:
rw [this, ← map_apply (by fun_prop), IsMulRightInvariant.map_mul_right_eq_self]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
⊢ MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)

Tactic:
hf.measurableSet_image.mpr hs

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableMul G
H : Type u_3
inst_3 : Group H
mH : MeasurableSpace H
inst_4 : MeasurableMul H
μ : Measure H
inst_5 : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding.{u_1, u_3} (α := G) (β := H) (⇑f : (a : G) → H)
g : G
s : Set G
hs : MeasurableSet s
this :
  Eq.{u_3 + 1} (α := Set H) (image (α := G) (⇑f : (a : G) → H) ((fun (x : G) ↦ x * g) ⁻¹' s))
    (preimage (β := H) (fun (x : H) ↦ HMul.hMul (β := H) x ((f : (a : G) → H) g : H)) ((⇑f : (a : G) → H) '' s))
⊢ MeasurableSet.{u_3} (α := H) ((⇑f : (a : G) → H) '' s)

Tactic:
exact hf.measurableSet_image.mpr hs

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableInv G
h :
  ∀ (s : Set G) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
      (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure G) (Measure.inv count) count

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : Group G
μ : Measure G
inst_3 : MeasurableInv G
s : Set G
hs : MeasurableSet s
h : ((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)
h₁ : ((count : Measure G) : (a : Set G) → ℝ≥0∞) s⁻¹ = (↑s.encard : ℝ≥0∞)
h₂ : (↑s⁻¹.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
h₃ h₄ : (↑s.encard : ℝ≥0∞) = (↑s.encard : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.inv count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure G) : (a : Set G) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [count_apply hs, inv_apply, count_apply hs.inv, encard_inv]

Premises used: MeasureTheory.Measure.count_apply, MeasureTheory.Measure.inv_apply, MeasurableSet.inv, Set.encard_inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : Group G
inst_2 : MeasurableInv G
inst_3 : MeasurableMul G
μ : Measure G
inst_4 : μ.IsMulLeftInvariant
inst_5 : μ.IsInvInvariant
x : G
⊢ Filter.map (fun (t : G) ↦ x / t) (ae μ) = ae μ

Tactic:
((MeasurableEquiv.divLeft x).map_ae μ).trans <| congr_arg ae <| map_div_left_eq_self μ x

Premises used: MeasureTheory.ae, congr_arg, MeasurableEquiv.divLeft, MeasureTheory.Measure.map_div_left_eq_self, MeasurableEquiv.map_ae, Eq.trans
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : ContinuousInv G
inst_6 : IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasureOnCompacts μ.inv

Tactic:
IsFiniteMeasureOnCompacts.map μ (Homeomorph.inv G)

Premises used: Homeomorph.inv, MeasureTheory.Measure.IsFiniteMeasureOnCompacts.map, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : ContinuousInv G
inst_6 : μ.IsOpenPosMeasure
⊢ μ.inv.IsOpenPosMeasure

Tactic:
(Homeomorph.inv G).continuous.isOpenPosMeasure_map (Homeomorph.inv G).surjective

Premises used: Homeomorph.continuous, Continuous.isOpenPosMeasure_map, Homeomorph.inv, MeasureTheory.Measure.inv, Homeomorph.surjective
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : ContinuousInv G
inst_6 : μ.Regular
⊢ μ.inv.Regular

Tactic:
Regular.map (Homeomorph.inv G)

Premises used: Homeomorph.inv, MeasureTheory.Measure.Regular.map, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : ContinuousInv G
inst_6 : μ.InnerRegular
⊢ μ.inv.InnerRegular

Tactic:
InnerRegular.map (Homeomorph.inv G)

Premises used: MeasureTheory.Measure.InnerRegular.map, Homeomorph.inv, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
α : Type u_3
inst_5 : Monoid α
inst_6 : MulAction α G
inst_7 : ContinuousConstSMul α G
inst_8 : μ.InnerRegular
a : α
⊢ InnerRegular (α := G) (Measure.map (fun (x : G) ↦ a • x) μ)

Tactic:
InnerRegular.map_of_continuous (continuous_const_smul a)

Premises used: ContinuousConstSMul.continuous_const_smul, MeasureTheory.Measure.InnerRegular.map_of_continuous
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : IsTopologicalGroup G
inst_6 : μ.InnerRegular
g : G
⊢ InnerRegular (α := G) (Measure.map (fun (x : G) ↦ g * x) μ)

Tactic:
InnerRegular.map_of_continuous (continuous_const_mul g)

Premises used: MeasureTheory.Measure.InnerRegular.map_of_continuous, continuous_const_mul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
H : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace H
inst_2 : TopologicalSpace G
inst_3 : BorelSpace G
μ : Measure G
inst_4 : Group G
inst_5 : IsTopologicalGroup G
inst_6 : μ.InnerRegular
g : G
⊢ InnerRegular (α := G) (Measure.map (fun (x : G) ↦ x * g) μ)

Tactic:
InnerRegular.map_of_continuous (continuous_mul_const g)

Premises used: MeasureTheory.Measure.InnerRegular.map_of_continuous, continuous_mul_const
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
⊢ μ.inv.Regular ↔ μ.Regular

Tactic:
Regular.map_iff (Homeomorph.inv G)

Premises used: Homeomorph.inv, MeasureTheory.Measure.inv, MeasureTheory.Measure.Regular.map_iff
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
⊢ μ.inv.InnerRegular ↔ μ.InnerRegular

Tactic:
InnerRegular.map_iff (Homeomorph.inv G)

Premises used: MeasureTheory.Measure.InnerRegular.map_iff, Homeomorph.inv, MeasureTheory.Measure.inv
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (U : Set G),
    k ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε

Tactic:
hk.exists_isOpen_lt_add hε

Premises used: IsCompact.exists_isOpen_lt_add
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
obtain :
  ∀ (U : Set G) (hUk : k ⊆ U) (hU : IsOpen[inst_1] U)
    (hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε),
    ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε

Tactic:
obtain ⟨U, hUk, hU, hμUk⟩ : ∃ (U : Set G), k ⊆ U ∧ IsOpen U ∧ μ U < μ k + ε :=
    hk.exists_isOpen_lt_add hε

Premises used: DFunLike.coe, IsCompact.exists_isOpen_lt_add, Set
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ V * k ⊆ U

Tactic:
compact_open_separated_mul_left hk hU hUk

Premises used: Set.Mem, compact_open_separated_mul_left
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
obtain :
  ∀ (V : Set G) (hV1 : Membership.mem (γ := Filter G) (𝓝 1) V) (hVkU : V * k ⊆ U),
    ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε

Tactic:
obtain ⟨V, hV1, hVkU⟩ : ∃ V ∈ 𝓝 (1 : G), V * k ⊆ U := compact_open_separated_mul_left hk hU hUk

Premises used: nhds, compact_open_separated_mul_left, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
h : ∀ (g : G) (hg : g ∈ V), (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε
⊢ ∀ᶠ (g : G) in 𝓝 1, (μ : (a : Set G) → ℝ≥0∞) (g • k \ k) < ε

Tactic:
filter_upwards [hV1] with g hg
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
h : g • k ⊆ U
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (g • k \ k) : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) (U \ k) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ g • k ⊆ U

Tactic:
(smul_set_subset_smul hg).trans hVkU

Premises used: HasSubset.Subset.trans, Set.smul_set_subset_smul
-- Module: Mathlib.MeasureTheory.Group.Measure
Goal:
G : Type u_1
inst : MeasurableSpace G
inst_1 : TopologicalSpace G
inst_2 : BorelSpace G
μ : Measure G
inst_3 : Group G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
inst_6 : IsFiniteMeasureOnCompacts μ
inst_7 : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst_1] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst_1] U
hμUk : (μ : (a : Set G) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) k : ℝ≥0∞) ε
V : Set G
hV1 : Membership.mem (γ := Filter G) (𝓝 1) V
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ g • k ⊆ U

Tactic:
exact (smul_set_subset_smul hg).trans hVkU

Premises used: HasSubset.Subset.trans, Set.smul_set_subset_smul