awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
⟨C, fun ⟨f, s, hs⟩ => Lp.eLpNorm_le_of_ae_tendsto
      (Eventually.of_forall fun n => hC (s n)) (fun n => hUI.1 (s n)) hs⟩

Premises used: ENNReal.ofNNReal, Filter.Eventually.of_forall, LE.le, And.left, Exists.intro, _private.0.MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto.match_1, MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto, Subtype.val, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UniformIntegrable fn p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (fn i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2))),
      eLpNorm.{u_1, u_2} (ε := β)
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            i)
          p μ ≤
        (↑C : ℝ≥0∞)

Tactic:
exact ⟨C, fun ⟨f, s, hs⟩ => Lp.eLpNorm_le_of_ae_tendsto
      (Eventually.of_forall fun n => hC (s n)) (fun n => hUI.1 (s n)) hs⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ f n x) u (𝓝 (g x))
⊢ MemLp g p μ

Tactic:
simpa using (hUI.uniformIntegrable_of_ae_tendsto u).memLp ⟨g, ⟨fun n => n, htends⟩⟩

Premises used: MeasureTheory.UniformIntegrable.uniformIntegrable_of_ae_tendsto, Subtype.mk, MeasureTheory.UniformIntegrable.memLp, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f 1 μ
htends : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ f n x) u (𝓝 (g x))
⊢ Integrable g μ

Tactic:
memLp_one_iff_integrable.mp (hUI.memLp_of_ae_tendsto htends)

Premises used: MeasureTheory.UniformIntegrable.memLp_of_ae_tendsto, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
g₁ g₂ : G
h₁ : Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} g₁
h₂ : Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} g₂
⊢ Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} (g₁ * g₂)

Tactic:
simpa only [smul_smul] using ((smul_set_ae_eq g₁).2 h₂).trans h₁

Premises used: Iff.mpr, Filter.EventuallyEq.trans, smul_smul, MeasureTheory.smul_set_ae_eq
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
⊢ Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
g : G
h : Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} g
⊢ Membership.mem (γ := Set G) {g : G | g • s =ᶠ[ae μ] s} g⁻¹

Tactic:
simpa using (smul_set_ae_eq g⁻¹).2 h.out.symm

Premises used: Iff.mpr, Membership.mem.out, Inv.inv, MeasureTheory.smul_set_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
g : G
s : Set α
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ g • s =ᶠ[ae μ] s

Tactic:
.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
g : G
hg : Membership.mem (γ := Subgroup G) (stabilizer G s) g
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x_1 : G
h : Membership.mem (γ := Subgroup G) ⊤ x_1
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ ∅) x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x_1 : G
h : Membership.mem (γ := Subgroup G) ⊤ x_1
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ univ) x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
h₁ :
  ∀ (g : G),
    Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
⊢ Eq (α := Subgroup G) (aestabilizer G μ s) (aestabilizer G μ t)

Tactic:
ext g
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
h₁ : g • s =ᶠ[ae μ] s ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
h₂ : g • s =ᶠ[ae μ] s ↔ g • t =ᶠ[ae μ] t
h₃ : g • s =ᶠ[ae μ] t ↔ g • t =ᶠ[ae μ] t
h₄ h₅ : g • t =ᶠ[ae μ] t ↔ g • t =ᶠ[ae μ] t
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g

Tactic:
rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]

Premises used: Iff.mpr, MulAction.mem_aestabilizer, Filter.EventuallyEq.congr_right, MeasureTheory.smul_set_ae_eq, Filter.EventuallyEq.congr_left
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
⊢ Eq (α := Subgroup G) (aestabilizer G μ s) ⊤

Tactic:
top_unique fun g _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
refine : ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g
⊢ Eq (α := Subgroup G) (aestabilizer G μ s) ⊤

Tactic:
refine top_unique fun g _ ↦ ?_

Premises used: top_unique
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ g
h : s =ᶠ[ae μ] ∅
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g

Tactic:
simp [aestabilizer_congr h]

Premises used: MulAction.aestabilizer_congr
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ g
h : s =ᶠ[ae μ] univ
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g

Tactic:
simp [aestabilizer_congr h]

Premises used: MulAction.aestabilizer_congr
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
cases eventuallyConst_set'.mp hs with
  | inl h => simp [aestabilizer_congr h]
  | inr h => simp [aestabilizer_congr h]

Premises used: Filter.eventuallyConst_set', Iff.mp
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x • s =ᶠ[ae μ] s
hy : Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y
⊢ LE.le (α := Subgroup G) (Subgroup.zpowers x) (MulAction.aestabilizer G μ s)

Tactic:
rw [← MulAction.mem_aestabilizer, ← Subgroup.zpowers_le] at hs

Premises used: MulAction.mem_aestabilizer, Subgroup.zpowers_le
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x • s =ᶠ[ae μ] s
hy : Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y
hs₁ : LE.le (α := Subgroup G) (Subgroup.zpowers x) (MulAction.aestabilizer G μ s)
⊢ Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y

Tactic:
rw [← MulAction.mem_aestabilizer, ← Subgroup.zpowers_le] at hs

Premises used: MulAction.mem_aestabilizer, Subgroup.zpowers_le
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : LE.le (α := Subgroup G) (Subgroup.zpowers x) (MulAction.aestabilizer G μ s)
hy : Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y
⊢ y • s =ᶠ[ae μ] s

Tactic:
hs hy

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : LE.le (α := Subgroup G) (Subgroup.zpowers x) (MulAction.aestabilizer G μ s)
hy : Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y
⊢ y • s =ᶠ[ae μ] s

Tactic:
exact hs hy
-- Module: Mathlib.MeasureTheory.Group.AEStabilizer
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x : G
s : Set α
hs : x • s =ᶠ[ae μ] s
⊢ x⁻¹ • s =ᶠ[ae μ] s

Tactic:
inv_mem (s := MulAction.aestabilizer G μ s) hs

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, InvMemClass.inv_mem
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
M : Type v
α : Type w
inst : MeasurableSpace α
inst_1 : SMul M α
⊢ @SMulInvariantMeasure M α _ inst 0

Tactic:
⟨fun _ _ _ => rfl⟩

Premises used: MeasureTheory.SMulInvariantMeasure.mk, rfl
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
M : Type v
α : Type w
inst : SMul M α
m : MeasurableSpace α
μ ν : Measure α
inst_1 : SMulInvariantMeasure M α μ
inst_2 : SMulInvariantMeasure M α ν
⊢ SMulInvariantMeasure M α (μ + ν)

Tactic:
⟨fun c _s hs =>
    show _ + _ = _ + _ from
      congr_arg₂ (· + ·) (measure_preimage_smul c hs) (measure_preimage_smul c hs)⟩

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, MeasureTheory.SMulInvariantMeasure.mk, HAdd.hAdd, congr_arg₂
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
M : Type v
α : Type w
inst : SMul M α
m : MeasurableSpace α
μ ν : Measure α
inst_1 : SMulInvariantMeasure M α μ
c : ℝ≥0∞
⊢ SMulInvariantMeasure M α (c • μ)

Tactic:
⟨fun a _s hs => show c • _ = c • _ from congr_arg (c • ·) (measure_preimage_smul a hs)⟩

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, MeasureTheory.SMulInvariantMeasure.mk, congr_arg, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
M : Type v
α : Type w
inst : SMul M α
m : MeasurableSpace α
μ ν : Measure α
inst_1 : SMulInvariantMeasure M α μ
c : ℝ≥0
⊢ SMulInvariantMeasure M α (c • μ)

Tactic:
SMulInvariantMeasure.smul c

Premises used: MeasureTheory.SMulInvariantMeasure.smul, ENNReal.ofNNReal
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(outerMeasure_le_iff (m := .map (c • ·) μ.1)).2
    (fun _s hs ↦ (SMulInvariantMeasure.measure_preimage_smul _ hs).le) _

Premises used: Iff.mpr, MeasureTheory.Measure.outerMeasure_le_iff, Eq.le, MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
c : G
⊢ Tendsto (fun (x : α) ↦ c • x) (ae μ) (ae μ)

Tactic:
fun _s hs ↦
  eq_bot_mono (measure_preimage_smul_le μ c _) hs

Premises used: Set.Mem, setOf, Set.preimage, Filter.Tendsto, eq_bot_mono
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
eq_bot_mono (measure_preimage_smul_le μ c _) h

Premises used: MeasureTheory.measure_preimage_smul_le, eq_bot_mono
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' toMeasurable μ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← measure_toMeasurable s,
    ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ s)]

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' toMeasurable μ s) : ℝ≥0∞)

Tactic:
measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

Premises used: MeasureTheory.measure_congr, Set.Mem, setOf, MeasureTheory.tendsto_smul_ae, Set.preimage, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' toMeasurable μ s) : ℝ≥0∞)

Tactic:
exact measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

Premises used: MeasureTheory.measure_congr, MeasureTheory.tendsto_smul_ae, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)

Tactic:
simpa [preimage_preimage] using measure_preimage_smul_le μ c⁻¹ ((c • ·) ⁻¹' s)

Premises used: Set.preimage_preimage, Inv.inv, Set.preimage, MeasureTheory.measure_preimage_smul_le, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s

Premises used: Set.preimage_smul_inv, Inv.inv, MeasureTheory.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)

Tactic:
rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]

Premises used: Set.smul_set_inter, smul_smul, one_smul, MeasureTheory.measure_smul, mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c⁻¹ • s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c • t) : ℝ≥0∞)

Tactic:
simpa [inv_inv] using (measure_inter_inv_smul _ c⁻¹ _ _).symm

Premises used: MeasureTheory.measure_inter_inv_smul, Inv.inv, inv_inv, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)

Tactic:
rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]

Premises used: smul_smul, one_smul, Set.smul_set_union, MeasureTheory.measure_smul, mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c⁻¹ • s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c • t) : ℝ≥0∞)

Tactic:
simpa [inv_inv] using (measure_union_inv_smul _ c⁻¹ _ _).symm

Premises used: Inv.inv, inv_inv, Eq.symm, MeasureTheory.measure_union_inv_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)

Tactic:
rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]

Premises used: smul_smul, one_smul, Set.smul_set_sdiff, MeasureTheory.measure_smul, mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c⁻¹ • s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c • t) : ℝ≥0∞)

Tactic:
simpa [inv_inv] using (measure_sdiff_inv_smul _ c⁻¹ _ _).symm

Premises used: MeasureTheory.measure_sdiff_inv_smul, Inv.inv, inv_inv, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ (c • c⁻¹ • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ ((c * c⁻¹) • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)

Tactic:
rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]

Premises used: Set.smul_set_symmDiff, smul_smul, one_smul, MeasureTheory.measure_smul, mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c⁻¹ • s) ∆ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c • t)) : ℝ≥0∞)

Tactic:
simpa [inv_inv] using (measure_symmDiff_inv_smul _ c⁻¹ _ _).symm

Premises used: MeasureTheory.measure_symmDiff_inv_smul, Inv.inv, inv_inv, Eq.symm