awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst : Monoid M
inst_1 : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst_2 : Monoid M'
inst_3 : MeasurableMul₂ M'
μ ν : Measure M
inst_4 : SFinite μ
inst_5 : SFinite ν
L : M →* M'
hL : Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')
this :
  Eq (α := M × M → M') (Function.comp (β := M) (⇑L : (a : M) → M') fun (p : M × M) ↦ p.1 * p.2)
    ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))
⊢ Eq.{u_3 + 1} (α := Measure M')
    (map (Function.comp (β := M) (⇑L : (a : M) → M') fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
have rw : Eq.{u_3 + 1} (α := Measure M')
  (map ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) (μ.prod ν))
  (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
Tactic: rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst : Monoid M
inst_1 : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst_2 : Monoid M'
inst_3 : MeasurableMul₂ M'
μ ν : Measure M
inst_4 : SFinite μ
inst_5 : SFinite ν
L : M →* M'
hL : Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')
this :
  Eq (α := M × M → M') (Function.comp (β := M) (⇑L : (a : M) → M') fun (p : M × M) ↦ p.1 * p.2)
    ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))
rw :
  Eq.{u_3 + 1} (α := Measure M')
    (map ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
⊢ Eq.{u_3 + 1} (α := Measure M')
    (map (Function.comp (β := M) (⇑L : (a : M) → M') fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
have rw₁ : Eq.{u_3 + 1} (α := Measure M')
  (map (fun (p : M' × M') ↦ p.1 * p.2) (map (Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) (μ.prod ν)))
  (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
Tactic: rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
M : Type u_2
M' : Type u_3
mM : MeasurableSpace M
inst : Monoid M
inst_1 : MeasurableMul₂ M
mM' : MeasurableSpace M'
inst_2 : Monoid M'
inst_3 : MeasurableMul₂ M'
μ ν : Measure M
inst_4 : SFinite μ
inst_5 : SFinite ν
L : M →* M'
hL : Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')
this :
  Eq (α := M × M → M') (Function.comp (β := M) (⇑L : (a : M) → M') fun (p : M × M) ↦ p.1 * p.2)
    ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))
rw :
  Eq.{u_3 + 1} (α := Measure M')
    (map ((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
rw₁ :
  Eq.{u_3 + 1} (α := Measure M')
    (map (fun (p : M' × M') ↦ p.1 * p.2) (map (Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) (μ.prod ν)))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
⊢ Eq.{u_3 + 1} (α := Measure M')
    (map (Function.comp (β := M) (⇑L : (a : M) → M') fun (x : M × M) ↦ x.1 * x.2) (μ.prod ν))
    (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
have rw₂ : Eq.{u_3 + 1} (α := Measure M')
  (map (fun (p : M' × M') ↦ p.1 * p.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
  (map (fun (x : M' × M') ↦ x.1 * x.2) (Measure.prod (map (⇑L : (a : M) → M') μ) (map (⇑L : (a : M) → M') ν)))
Tactic: rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : AddCommMonoid F
inst_2 : Module ℝ E
inst_3 : Module ℝ F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
mE : MeasurableSpace E
inst_6 : MeasurableAdd₂ E
mF : MeasurableSpace F
inst_7 : MeasurableAdd₂ F
inst_8 : OpensMeasurableSpace E
inst_9 : BorelSpace F
μ ν : Measure E
inst_10 : SFinite μ
inst_11 : SFinite ν
L : E →L[ℝ] F
⊢ Eq.{u_3 + 1} (α := Measure F) (map (⇑L : (a : E) → F) (μ ∗ ν)) (map (⇑L : (a : E) → F) μ ∗ map (⇑L : (a : E) → F) ν)
have suffices : Eq.{u_3 + 1} (α := Measure F) (map (⇑(↑L : E →+ F) : (a : E) → F) (μ ∗ ν))
  (map (⇑(↑L : E →+ F) : (a : E) → F) μ ∗ map (⇑(↑L : E →+ F) : (a : E) → F) ν)
Tactic: suffices (μ ∗ ν).map (L : E →+ F) = (μ.map (L : E →+ F)) ∗ (ν.map (L : E →+ F)) by simpa
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : AddCommMonoid F
inst_2 : Module ℝ E
inst_3 : Module ℝ F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
mE : MeasurableSpace E
inst_6 : MeasurableAdd₂ E
mF : MeasurableSpace F
inst_7 : MeasurableAdd₂ F
inst_8 : OpensMeasurableSpace E
inst_9 : BorelSpace F
μ ν : Measure E
inst_10 : SFinite μ
inst_11 : SFinite ν
L : E →L[ℝ] F
⊢ Eq.{u_3 + 1} (α := Measure F) (map (⇑(↑L : E →+ F) : (a : E) → F) (μ ∗ ν))
    (map (⇑(↑L : E →+ F) : (a : E) → F) μ ∗ map (⇑(↑L : E →+ F) : (a : E) → F) ν)
have hL : Measurable.{u_2, u_3} (α := E) (β := F) (⇑(↑L : E →+ F) : (a : E) → F)
Tactic: rw [map_conv_addMonoidHom]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : AddCommMonoid F
inst_2 : Module ℝ E
inst_3 : Module ℝ F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
mE : MeasurableSpace E
inst_6 : MeasurableAdd₂ E
mF : MeasurableSpace F
inst_7 : MeasurableAdd₂ F
inst_8 : OpensMeasurableSpace E
inst_9 : BorelSpace F
μ ν : Measure E
inst_10 : SFinite μ
inst_11 : SFinite ν
L : E →L[ℝ] F
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑(↑L : E →+ F) : (a : E) → F)
have hL : Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)
Tactic: rw [AddMonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : AddCommMonoid F
inst_2 : Module ℝ E
inst_3 : Module ℝ F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
mE : MeasurableSpace E
inst_6 : MeasurableAdd₂ E
mF : MeasurableSpace F
inst_7 : MeasurableAdd₂ F
inst_8 : OpensMeasurableSpace E
inst_9 : BorelSpace F
μ ν : Measure E
inst_10 : SFinite μ
inst_11 : SFinite ν
L : E →L[ℝ] F
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)
have funProp : mE ≤ mE
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Convolution (goal)
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : AddCommMonoid F
inst_2 : Module ℝ E
inst_3 : Module ℝ F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
mE : MeasurableSpace E
inst_6 : MeasurableAdd₂ E
mF : MeasurableSpace F
inst_7 : MeasurableAdd₂ F
inst_8 : OpensMeasurableSpace E
inst_9 : BorelSpace F
μ ν : Measure E
inst_10 : SFinite μ
inst_11 : SFinite ν
L : E →L[ℝ] F
funProp : mE ≤ mE
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)
have funProp₁ : MeasurableEmbedding.{u_2, u_3} (β := F) fun (a : E) ↦ (L : (a : E) → F) a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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 : Set X
⊢ ∀ᶠ (i : ι) in (↑u : Filter ι),
    Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
have h : ∀ (i : ι) (hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞))
  (hi' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
Tactic: filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (hypothesis)
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 : Set X
⊢ Tendsto
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    (↑u : Filter ι) (𝓝 (mean μ u F s))
have mem_Icc : ∀ᶠ (i : ι) in (↑u : Filter ι),
  Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1)
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
Tactic: have mem_Icc : ∀ᶠ i in u, μ (s ∩ F i) / μ (F i) ∈ Icc 0 1 := by
    filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'
    simpa [ENNReal.div_le_iff hi hi'] using μ.mono inter_subset_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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 : Set X
mem_Icc :
  ∀ᶠ (i : ι) in (↑u : Filter ι),
    Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
⊢ Tendsto
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    (↑u : Filter ι) (𝓝 (mean μ u F s))
have obtain : ∀ (x : ℝ≥0∞)
  (hx :
    Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1) x ∧
      (↑(Ultrafilter.map
              (fun (i : ι) ↦
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
                  ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
              u) :
          Filter ℝ≥0∞) ≤
        𝓝 x),
  Tendsto
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    (↑u : Filter ι) (𝓝 (mean μ u F s))
Tactic: obtain ⟨x, hx⟩ := isCompact_Icc.ultrafilter_le_nhds'
    (u.map (fun i ↦ μ (s ∩ F i) / μ (F i))) (mem_map.1 mem_Icc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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 : Set X
mem_Icc :
  ∀ᶠ (i : ι) in (↑u : Filter ι),
    Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1)
      (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
x : ℝ≥0∞
hx :
  Membership.mem (γ := Set ℝ≥0∞) (Icc 0 1) x ∧
    (↑(Ultrafilter.map
            (fun (i : ι) ↦
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
                ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
            u) :
        Filter ℝ≥0∞) ≤
      𝓝 x
⊢ ∃ (x : ℝ≥0∞),
    Tendsto
      (fun (i : ι) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
      (↑u : Filter ι) (𝓝 x)
have h : Tendsto
  (fun (i : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
  (↑u : Filter ι) (𝓝 x)
Tactic: use x
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
⊢ mean μ u F univ = 1
have refine : (↑u : Filter ι).EventuallyEq (β := ℝ≥0∞)
  (fun (i : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
  fun (x : ι) ↦ 1
Tactic: refine tendsto_nhds_unique_of_eventuallyEq (hfoel.tendsto_nhds_mean _) tendsto_const_nhds ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
⊢ (↑u : Filter ι).EventuallyEq (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦ 1
have h : ∀ (i : ι) (hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞))
  (hi' : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) =
    1
Tactic: filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
have 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∞)
Tactic: refine tendsto_nhds_unique_of_eventuallyEq
    (hfoel.tendsto_nhds_mean _) (hfoel.tendsto_nhds_mean _ |>.add <| hfoel.tendsto_nhds_mean _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
⊢ (↑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∞)
have 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∞)
Tactic: filter_upwards [hfoel.eventually_measurableSet] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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)
⊢ 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∞)
have 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∞)
Tactic: rw [union_inter_distrib_right,
    measure_union (hdisj.inter_left _ |>.inter_right _) (ht.inter hi), ENNReal.add_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [union_inter_distrib_right,
    measure_union (hdisj.inter_left _ |>.inter_right _) (ht.inter hi), ENNReal.add_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: rw [union_inter_distrib_right,
    measure_union (hdisj.inter_left _ |>.inter_right _) (ht.inter hi), ENNReal.add_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
⊢ mean μ u F (g • s) = mean μ u F (h • s)
have suffices : ∀ (g h : G), 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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)
have rw : mean μ u F (g • s) ≤ mean μ u F (h • s) + 0
Tactic: rw [← add_zero <| mean μ u F (h • s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
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
have 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∞)
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⁻¹) ?_