awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Convolution
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')
rw :
  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') ν)))
⊢ Eq.{u_3 + 1} (α := Measure M') (map (α := M) (⇑L : (a : M) → M') (map (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') ν)))

Tactic:
rw [map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Convolution
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')
h :
  ∀ (x : M × M),
    Eq.{u_3 + 1} (α := M') (Function.comp (β := M) (⇑L : (a : M) → M') (fun (p : M × M) ↦ p.1 * p.2) x)
      (((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) x)
⊢ 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'))

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Group.Convolution
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')
x : M × M
⊢ Eq.{u_3 + 1} (α := M') (Function.comp (β := M) (⇑L : (a : M) → M') (fun (p : M × M) ↦ p.1 * p.2) x)
    (((fun (p : M' × M') ↦ p.1 * p.2) ∘ Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M')) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.Convolution
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')
⊢ 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'))

Tactic:
have : (L ∘ fun p : M × M ↦ p.1 * p.2) = (fun p : M' × M' ↦ p.1 * p.2) ∘ (Prod.map L L) := by
    ext; simp
-- Module: Mathlib.MeasureTheory.Group.Convolution
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'))
⊢ Measurable (β := M') fun (p : M' × M') ↦ p.1 * p.2

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
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'))
⊢ Measurable.{u_2, u_3} (α := M × M) (β := M' × M') (Prod.map (⇑L : (a : M) → M') (⇑L : (a : M) → M'))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
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'))
⊢ Measurable.{u_2, u_3} (α := M) (β := M') (⇑L : (a : M) → M')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Convolution
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') ν)))
rw₂ 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') ν)))
⊢ 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') ν)))

Tactic:
rw [this, ← map_map (by fun_prop) (by fun_prop), ← map_prod_map _ _ (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_prod_map, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.Convolution
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
this :
  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) ν)
⊢ Eq.{u_3 + 1} (α := Measure F) (map (⇑L : (a : E) → F) (μ ∗ ν)) (map (⇑L : (a : E) → F) μ ∗ map (⇑L : (a : E) → F) ν)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Group.Convolution
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
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) ν)
⊢ Eq.{u_3 + 1} (α := Measure F) (map (⇑L : (a : E) → F) (μ ∗ ν)) (map (⇑L : (a : E) → F) μ ∗ map (⇑L : (a : E) → F) ν)

Tactic:
suffices (μ ∗ ν).map (L : E →+ F) = (μ.map (L : E →+ F)) ∗ (ν.map (L : E →+ F)) by simpa
-- Module: Mathlib.MeasureTheory.Group.Convolution
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
hL : Measurable.{u_2, u_3} (α := E) (β := F) (⇑(↑L : E →+ F) : (a : E) → 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) ν)

Tactic:
rw [map_conv_addMonoidHom]

Premises used: MeasureTheory.Measure.map_conv_addMonoidHom
-- Module: Mathlib.MeasureTheory.Group.Convolution
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
hL : Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑(↑L : E →+ F) : (a : E) → F)

Tactic:
rw [AddMonoidHom.coe_coe]

Premises used: AddMonoidHom.coe_coe
-- Module: Mathlib.MeasureTheory.Group.Convolution
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
funProp₁ : MeasurableEmbedding.{u_2, u_3} (β := F) fun (a : E) ↦ (L : (a : E) → F) a
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Defs
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Mul G
inst_2 : μ.IsMulLeftInvariant
⊢ SMulInvariantMeasure G G μ

Tactic:
⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _) hs.nullMeasurableSet⟩

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.SMulInvariantMeasure.mk, MeasureTheory.Measure.measure_preimage_of_map_eq_self, MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self
-- Module: Mathlib.MeasureTheory.Group.Defs
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Monoid G
s : Submonoid G
inst_2 : μ.IsMulLeftInvariant
⊢ SMulInvariantMeasure (↥s) G μ

Tactic:
⟨fun ⟨x, _⟩ _ h ↦ IsMulLeftInvariant.smulInvariantMeasure.1 x h⟩

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, MeasureTheory.SMulInvariantMeasure.mk, Set.preimage, HSMul.hSMul, Eq, DFunLike.coe, _private.0.MeasureTheory.Measure.instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant.match_1
-- Module: Mathlib.MeasureTheory.Group.Defs
Goal:
G : Type u_1
inst : MeasurableSpace G
μ : Measure G
inst_1 : Mul G
inst_2 : μ.IsMulRightInvariant
⊢ SMulInvariantMeasure Gᵐᵒᵖ G μ

Tactic:
⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _) hs.nullMeasurableSet⟩

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self, MeasureTheory.SMulInvariantMeasure.mk, MeasureTheory.Measure.measure_preimage_of_map_eq_self, MulOpposite.unop
-- 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 ι
inst_3 : NeZero μ
inst_4 : IsFiniteMeasure μ
⊢ ∀ᶠ (i : ι) in l, MeasurableSet.{u_2} (α := X) univ

Tactic:
simp
-- 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 ι
inst_3 : NeZero μ
inst_4 : IsFiniteMeasure μ
⊢ ∀ᶠ (i : ι) in l, Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [NeZero.ne]

Premises used: NeZero.ne
-- 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 ι
inst_3 : NeZero μ
inst_4 : IsFiniteMeasure μ
⊢ ∀ᶠ (i : ι) in l, Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- 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 ι
inst_3 : NeZero μ
inst_4 : IsFiniteMeasure μ
⊢ ∀ (g : G),
    Tendsto (β := ℝ≥0∞)
      (fun (i : ι) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (HSMul.hSMul (β := Set X) g univ ∆ univ) : ℝ≥0∞)
          ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞))
      l (𝓝 0)

Tactic:
simp [tendsto_const_nhds]

Premises used: tendsto_const_nhds
-- 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 : Set X
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∞))
⊢ ∀ᶠ (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:
filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'

Premises used: IsFoelner.eventually_meas_ne_zero, IsFoelner.eventually_meas_ne_top
-- 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 : Set X
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:
simpa [ENNReal.div_le_iff hi hi'] using μ.mono inter_subset_right

Premises used: MeasureTheory.OuterMeasure.mono, ENNReal.div_le_iff, MeasureTheory.Measure.toOuterMeasure, Set.inter_subset_right
-- 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 : 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∞))

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
-- 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 : 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∞))
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))
⊢ 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)

Premises used: HDiv.hDiv, IsCompact.ultrafilter_le_nhds', CompactIccSpace.isCompact_Icc, Inter.inter, Iff.mp, Ultrafilter.map, DFunLike.coe, Filter.mem_map
-- 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 : 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
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)
⊢ ∃ (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)

Tactic:
use x
-- 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 : 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
⊢ 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:
hx.2

Premises used: Set.Mem, And.right, Filter.Tendsto
-- 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 : 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
⊢ 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:
exact hx.2

Premises used: And.right
-- 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 : 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
⊢ 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:
exact tendsto_nhds_limUnder (by use x; exact hx.2)

Premises used: tendsto_nhds_limUnder
-- 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
⊢ mean μ u F univ = 1

Tactic:
tendsto_nhds_unique_of_eventuallyEq (hfoel.tendsto_nhds_mean _) tendsto_const_nhds ?_

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, 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
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
⊢ mean μ u F univ = 1

Tactic:
refine tendsto_nhds_unique_of_eventuallyEq (hfoel.tendsto_nhds_mean _) tendsto_const_nhds ?_

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq, 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
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
⊢ (↑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:
filter_upwards [hfoel.eventually_meas_ne_zero, hfoel.eventually_meas_ne_top] with i hi hi'

Premises used: IsFoelner.eventually_meas_ne_zero, IsFoelner.eventually_meas_ne_top
-- 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
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:
simp [ENNReal.div_self hi hi']

Premises used: ENNReal.div_self