awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u : Filter ι) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
⊢ mean μ u F (s ∪ t) = mean μ u F s + mean μ u F t

Tactic:
tendsto_nhds_unique_of_eventuallyEq
    (hfoel.tendsto_nhds_mean _) (hfoel.tendsto_nhds_mean _ |>.add <| hfoel.tendsto_nhds_mean _) ?_

Premises used: tendsto_nhds_unique_of_eventuallyEq, Filter.Tendsto.add, IsFoelner.tendsto_nhds_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u : Filter ι) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
refine :
  (↑u : Filter ι).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((s ∪ t) ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞)
⊢ mean μ u F (s ∪ t) = mean μ u F s + mean μ u F t

Tactic:
refine tendsto_nhds_unique_of_eventuallyEq
    (hfoel.tendsto_nhds_mean _) (hfoel.tendsto_nhds_mean _ |>.add <| hfoel.tendsto_nhds_mean _) ?_

Premises used: tendsto_nhds_unique_of_eventuallyEq, Filter.Tendsto.add, IsFoelner.tendsto_nhds_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u : Filter ι) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
h :
  ∀ (i : ι) (hi : MeasurableSet (F i)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((s ∪ t) ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
⊢ (↑u : Filter ι).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((s ∪ t) ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞)

Tactic:
filter_upwards [hfoel.eventually_measurableSet] with i hi

Premises used: IsFoelner.eventually_measurableSet
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u : Filter ι) F
s t : Set X
ht : MeasurableSet t
hdisj : Disjoint s t
i : ι
hi : MeasurableSet (F i)
h :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i ∪ t ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
h₁ :
  HDiv.hDiv (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
h₂ h₃ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((s ∪ t) ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)

Tactic:
rw [union_inter_distrib_right,
    measure_union (hdisj.inter_left _ |>.inter_right _) (ht.inter hi), ENNReal.add_div]

Premises used: Disjoint.inter_right, ENNReal.add_div, Disjoint.inter_left, MeasureTheory.measure_union, Set.union_inter_distrib_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g h : G
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g • F i) ∆ (h • F i)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    (↑u : Filter ι) (𝓝 0)

Tactic:
simpa [← smul_smul] using hfoel.tendsto_meas_smul_symmDiff (h⁻¹ * g)

Premises used: HMul.hMul, IsFoelner.tendsto_meas_smul_symmDiff, smul_smul, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g h : G
s : Set X
hle : ∀ (g h : G), mean μ u F (g • s) ≤ mean μ u F (h • s)
⊢ mean μ u F (g • s) = mean μ u F (h • s)

Tactic:
le_antisymm (hle g h) (hle h g)

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g h : G
s : Set X
hle : ∀ (g h : G), mean μ u F (g • s) ≤ mean μ u F (h • s)
⊢ mean μ u F (g • s) = mean μ u F (h • s)

Tactic:
exact le_antisymm (hle g h) (hle h g)

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g h : G
s : Set X
suffices : ∀ (g h : G), mean μ u F (g • s) ≤ mean μ u F (h • s)
⊢ mean μ u F (g • s) = mean μ u F (h • s)

Tactic:
suffices hle : ∀ g h, mean μ u F (g • s) ≤ mean μ u F (h • s) by
    exact le_antisymm (hle g h) (hle h g)
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
rw : mean μ u F (g • s) ≤ mean μ u F (h • s) + 0
⊢ mean μ u F (g • s) ≤ mean μ u F (h • s)

Tactic:
rw [← add_zero <| mean μ u F (h • s)]

Premises used: HSMul.hSMul, add_zero, IsFoelner.mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
⊢ mean μ u F (g • s) ≤ mean μ u F (h • s) + 0

Tactic:
le_of_tendsto_of_tendsto
    (hfoel.tendsto_nhds_mean (g • s))
    (hfoel.tendsto_nhds_mean (h • s) |>.add <| hfoel.tendsto_meas_smul_symmDiff_smul g⁻¹ h⁻¹) ?_

Premises used: IsFoelner.tendsto_meas_smul_symmDiff_smul, Inv.inv, Filter.Tendsto.add, HSMul.hSMul, le_of_tendsto_of_tendsto, IsFoelner.tendsto_nhds_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
refine :
  (↑u : Filter ι).EventuallyLE (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F x) ∆ (h⁻¹ • F x)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞)
⊢ mean μ u F (g • s) ≤ mean μ u F (h • s) + 0

Tactic:
refine le_of_tendsto_of_tendsto
    (hfoel.tendsto_nhds_mean (g • s))
    (hfoel.tendsto_nhds_mean (h • s) |>.add <| hfoel.tendsto_meas_smul_symmDiff_smul g⁻¹ h⁻¹) ?_

Premises used: IsFoelner.tendsto_meas_smul_symmDiff_smul, Inv.inv, Filter.Tendsto.add, HSMul.hSMul, le_of_tendsto_of_tendsto, IsFoelner.tendsto_nhds_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
h₁ :
  ∀ (i : ι) (hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
⊢ (↑u : Filter ι).EventuallyLE (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F x) ∆ (h⁻¹ • F x)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞)

Tactic:
filter_upwards [hfoel.eventually_meas_ne_zero] with i hi

Premises used: IsFoelner.eventually_meas_ne_zero
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ :
  HDiv.hDiv (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)

Tactic:
rw [← tsub_le_iff_left, ← ENNReal.sub_div <| fun _ _ ↦ hi]

Premises used: tsub_le_iff_left, ENNReal.sub_div
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)

Tactic:
ENNReal.div_le_div_right (le_trans ?_ (measure_mono <| @inter_subset_right _ s _)) _

Premises used: ENNReal.div_le_div_right, MeasureTheory.measure_mono, Set.inter_subset_right, le_trans
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) (s ∩ (g⁻¹ • F i) ∆ (h⁻¹ • F i))
⊢ HDiv.hDiv (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)

Tactic:
refine ENNReal.div_le_div_right (le_trans ?_ (measure_mono <| @inter_subset_right _ s _)) _

Premises used: ENNReal.div_le_div_right, MeasureTheory.measure_mono, Set.inter_subset_right, le_trans
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞) ≤
    (μ : (a : Set X) → ℝ≥0∞) (s ∩ (g⁻¹ • F i) ∆ (h⁻¹ • F i))

Tactic:
simpa [inter_symmDiff_distrib_left, ← measure_inter_inv_smul] using le_measure_symmDiff

Premises used: Set.inter_symmDiff_distrib_left, MeasureTheory.le_measure_symmDiff, MeasureTheory.measure_inter_inv_smul
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g : G
s : Set X
⊢ mean μ u F (g • s) = mean μ u F s

Tactic:
simpa using hfoel.mean_smul_eq_mean_smul g 1 s

Premises used: IsFoelner.mean_smul_eq_mean_smul, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
h :
  mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
⊢ ∃ (m : Set X → ℝ≥0∞),
    m univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s

Tactic:
use mean μ (Ultrafilter.of l) F

Premises used: Ultrafilter.of, IsFoelner.mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
h : mean μ (Ultrafilter.of l) F univ = 1
h₁ :
  ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t
h₂ : ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
⊢ mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s

Tactic:
refine ⟨?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ mean μ (Ultrafilter.of l) F univ = 1

Tactic:
(hfoel.mono <| Ultrafilter.of_le l).mean_univ_eq_one

Premises used: IsFoelner.mean_univ_eq_one, Ultrafilter.of_le, IsFoelner.mono
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ mean μ (Ultrafilter.of l) F univ = 1

Tactic:
exact (hfoel.mono <| Ultrafilter.of_le l).mean_univ_eq_one

Premises used: IsFoelner.mean_univ_eq_one, Ultrafilter.of_le, IsFoelner.mono
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t

Tactic:
(hfoel.mono <| Ultrafilter.of_le l).mean_union_eq_add_of_disjoint

Premises used: Ultrafilter.of_le, IsFoelner.mono, IsFoelner.mean_union_eq_add_of_disjoint
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t

Tactic:
exact (hfoel.mono <| Ultrafilter.of_le l).mean_union_eq_add_of_disjoint

Premises used: Ultrafilter.of_le, IsFoelner.mono, IsFoelner.mean_union_eq_add_of_disjoint
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s

Tactic:
(hfoel.mono <| Ultrafilter.of_le l).mean_smul_eq_mean

Premises used: Ultrafilter.of_le, IsFoelner.mono, IsFoelner.mean_smul_eq_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s

Tactic:
exact (hfoel.mono <| Ultrafilter.of_le l).mean_smul_eq_mean

Premises used: Ultrafilter.of_le, IsFoelner.mono, IsFoelner.mean_smul_eq_mean
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
⊢ IsFoelner G μ l F ↔ Tendsto F l (maxFoelner G μ)

Tactic:
simp [maxFoelner, tendsto_inf, tendsto_iInf, isFoelner_iff, Function.comp_def, and_assoc]

Premises used: Filter.tendsto_inf, isFoelner_iff, Function.comp_def, and_assoc, Filter.tendsto_iInf, maxFoelner
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
⊢ IsFoelner G μ (maxFoelner G μ) id

Tactic:
isFoelner_iff_tendsto _ _ |>.2 <| @tendsto_id _ (maxFoelner G μ)

Premises used: Iff.mpr, isFoelner_iff_tendsto, Filter.tendsto_id
-- Module: Mathlib.MeasureTheory.Group.FoelnerFilter
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : (maxFoelner G μ).NeBot
⊢ ∃ (m : Set X → ℝ≥0∞),
    m univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s

Tactic:
IsFoelner.amenable <| isFoelner_maxFoelner G μ

Premises used: IsFoelner.amenable, isFoelner_maxFoelner
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g : G, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) a) x
hxb : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) b) x
⊢ a⁻¹ • x ∈ s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g : G, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) a) x
hxb : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) b) x
hxa₁ : a⁻¹ • x ∈ s
⊢ b⁻¹ • x ∈ s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb

Premises used: Set.mem_smul_set_iff_inv_smul_mem