mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ (n + 1) • r ≤ ∑ x ∈ Finset.range (n + 1), μ (s x)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
n : ℕ
⊢ (↑n + 1) * r ≤ ∑ x ∈ Finset.range (n + 1), μ (s x)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
inst✝ : l.IsCountablyGenerated
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
⊢ TendstoInMeasure μ' (X - fun x ↦ Z) l 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
inst✝ : l.IsCountablyGenerated
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
⊢ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ' {x | ε ≤ ‖X i x - Z x‖}) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case refine_2
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁸ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁷ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ TendstoInMeasure μ'' (fun n ω ↦ (0, Y n ω - c)) l 0

Tactic:
simpa using

Goal state after:
case refine_2
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁸ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁷ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
⊢ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i ↦ μ'' {x | ε ≤ ‖Y i x - c‖}) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: case refine_2
α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ eLpNorm (fun x ↦ Finset.univ.sup fun x ↦ ‖f x‖ₑ) p count < ∞

Tactic:
exact (memLp_const_enorm <| by simp [h, LT.lt.ne]).eLpNorm_lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: case refine_3.refine_1.refine_1
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : r / μ univ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
hxs : {n | x ∈ s n}.Finite
⊢ Tendsto (fun n ↦ (↑n.succ)⁻¹ * ↑hxs.toFinset.card) atTop (nhds ⊥)

Tactic:
simpa using

Goal state after:
case refine_3.refine_1.refine_1
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : r / μ univ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
hxs : {n | x ∈ s n}.Finite
⊢ Tendsto (fun n ↦ (↑n + 1)⁻¹ * ↑hxs.toFinset.card) atTop (nhds 0)
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: case refine_3
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : r / μ univ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
⊢ ∃ t, t.Infinite ∧ ∀ ⦃u : Set ℕ⦄, u ⊆ t → u.Finite → 0 < μ (⋂ n ∈ u, s n)

Tactic:
refine ⟨{n | x ∈ s n}, fun hxs ↦ ?_, fun u hux hu ↦ ?_⟩
    -- This next block proves that a set of strictly positive natural density is infinite, mixed
    -- with the fact that `{n | x ∈ s n}` has strictly positive natural density.
    -- TODO: Separate it out to a lemma once we have a natural density API.
    · refine ENNReal.div_ne_zero.2 ⟨hr₀, by finiteness⟩ <| eq_bot_mono hx <|
        Tendsto.limsup_eq <| tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
        (h := fun n ↦ (n.succ : ℝ≥0∞)⁻¹ * hxs.toFinset.card) ?_ bot_le fun n ↦ mul_le_mul_right ?_ _
      · simpa using ENNReal.Tendsto.mul_const (ENNReal.tendsto_inv_nat_nhds_zero.comp <|
          tendsto_add_atTop_nat 1) (.inr <| ENNReal.natCast_ne_top _)
      · classical
        simpa only [Finset.sum_apply, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_le]
          using! Finset.card_le_card fun m hm ↦ hxs.mem_toFinset.2 (Finset.mem_filter.1 hm).2
    · simp_rw [← hu.mem_toFinset]
      exact hN₁ _ ⟨x, mem_iInter₂.2 fun n hn ↦ hux <| hu.mem_toFinset.1 hn, hxN⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : MeasurableSpace β
inst✝ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
hf : ∀ (i : ι), Measurable (f i)
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (hs.piecewise f ⁻¹' t)

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : MeasurableSpace β
inst✝ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
hf : ∀ (i : ι), Measurable (f i)
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (⋃ i, s i ∩ f i ⁻¹' t)
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ μ ∅ ≠ ∞

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ 0 ≠ ∞
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
hi : μ (F i) ≠ 0
hi' : μ (F i) ≠ ∞
⊢ μ (s ∩ F i) / μ (F i) ∈ Icc 0 1

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : Group G
inst✝ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
hfoel : IsFoelner G μ (↑u) F
s : Set X
i : ι
hi : μ (F i) ≠ 0
hi' : μ (F i) ≠ ∞
⊢ μ (s ∩ F i) ≤ μ (F i)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g h : G
⊢ Tendsto (fun i ↦ μ ((g • F i) ∆ (h • F i)) / μ (F i)) (↑u) (𝓝 0)

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g h : G
⊢ Tendsto (fun i ↦ μ ((g • F i) ∆ (h • F i)) / μ (F i)) (↑u) (𝓝 0)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h✝ : G
s : Set X
g h : G
i : ι
hi : μ (F i) ≠ 0
⊢ μ (g • s ∩ F i) - μ (h • s ∩ F i) ≤ μ (s ∩ (g⁻¹ • F i) ∆ (h⁻¹ • F i))

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g✝ h✝ : G
s : Set X
g h : G
i : ι
hi : μ (F i) ≠ 0
⊢ μ (s ∩ g⁻¹ • F i) ≤ μ ((s ∩ g⁻¹ • F i) ∆ (s ∩ h⁻¹ • F i)) + μ (s ∩ h⁻¹ • F i)
Module: Mathlib.MeasureTheory.Group.FoelnerFilter

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g : G
s : Set X
⊢ mean μ u F (g • s) = mean μ u F s

Tactic:
simpa using

Goal state after:
G : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : Group G
inst✝¹ : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst✝ : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u) F
g : G
s : Set X
⊢ mean μ u F (g • s) = mean μ u F s
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty (ι ≃ Fin n)
g : Fin n → α → β := f ∘ ⇑hn.some.symm
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : μ s ≠ ∞
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε
i : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Finite ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
n : ℕ
hn : Nonempty (ι ≃ Fin n)
g : Fin n → α → β := f ∘ ⇑hn.some.symm
hg : ∀ (i : Fin n), MemLp (g i) p μ
s : Set α
hμs : μ s ≠ ∞
hfε : ∀ (i : Fin n), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε
i : ι
⊢ eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
hμ : μ s = 0
⊢ μ F = 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
hμ : μ s = 0
⊢ μ F = 0
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ ((circleMap z R i.2 - i.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)

Tactic:
simpa using

Goal state after:
case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ ((circleMap z R i.2 - i.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
simpa using

Goal state after:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
this :
  ∃ x ∈ closedBall z r ×ˢ [[0, 2 * π]],
    IsMaxOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ [[0, 2 * π]]) x
⊢ ∃ a b,
    (dist a z ≤ r ∧ b ∈ [[0, 2 * π]]) ∧
      ∀ (a_1 : ℂ) (b_1 : ℝ),
        dist a_1 z ≤ r →
          b_1 ∈ [[0, 2 * π]] →
            ‖circleTransformBoundingFunction R z (a_1, b_1)‖ ≤ ‖circleTransformBoundingFunction R z (a, b)‖
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
V : ℝ → ℂ → ℂ := fun θ w ↦ circleTransformDeriv R z w (fun x ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩‖ * ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖ * ‖f X‖
⊢ ‖circleTransformDeriv R z v f y1‖ ≤ ‖V b a‖ * ‖f X‖

Tactic:
simpa using

Goal state after:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
    ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖
V : ℝ → ℂ → ℂ := fun θ w ↦ circleTransformDeriv R z w (fun x ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩‖ * ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩‖ * ‖f X‖
⊢ |R| * ((‖circleMap z R y1 - v‖ ^ 2)⁻¹ * ‖f (circleMap z R y1)‖) ≤ |R| * ((‖circleMap z R b - a‖ ^ 2)⁻¹ * ‖f X‖)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : g 0 = 0
⊢ HasCompactSupport (g.comp ↑f).toFun

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)

Tactic:
· exact f.hasCompactSupport'.comp_left hg

Goal state after:
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g f : α →C_c β
⊢ HasCompactSupport (-⇑f.toContinuousMap)

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g f : α →C_c β
⊢ IsCompact (closure (Function.support ⇑f))
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g✝ f g : α →C_c β
⊢ HasCompactSupport (⇑f.toContinuousMap - ⇑g.toContinuousMap)

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
x : α
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
f✝ g✝ f g : α →C_c β
⊢ HasCompactSupport (⇑f + -⇑g)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ ↑((f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ }) x) = ↑(f₂ x)

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ f₁ x + (f₂ x - f₁ x) = f₂ x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
x : α
⊢ ↑((-f).nnrealPart x) = ↑(0 x)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
hf : 0 ≤ f
x : α
⊢ 0 ≤ f x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
x : α
⊢ (f + g).nnrealPart x ≤ (f.nnrealPart + g.nnrealPart) x

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
x : α
⊢ (f x + g x).toNNReal ≤ (f x).toNNReal + (g x).toNNReal
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : R1Space α
inst✝⁵ : Group α
inst✝⁴ : TopologicalSpace β
inst✝³ : R1Space β
inst✝² : Group β
inst✝¹ : ContinuousMul β
inst✝ : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding ⇑φ
f : β →C_c γ
b : β
K : Set β
hK : IsCompact K
hf : ∀ x ∉ K, f x = 0
x : α
hx : x ∉ ⇑φ ⁻¹' (b⁻¹ • K)
⊢ b * φ x ∉ K

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁷ : TopologicalSpace α
inst✝⁶ : R1Space α
inst✝⁵ : Group α
inst✝⁴ : TopologicalSpace β
inst✝³ : R1Space β
inst✝² : Group β
inst✝¹ : ContinuousMul β
inst✝ : NormedAddCommGroup γ
φ : α →* β
hφ : Topology.IsClosedEmbedding ⇑φ
f : β →C_c γ
b : β
K : Set β
hK : IsCompact K
hf : ∀ x ∉ K, f x = 0
x : α
hx : x ∉ ⇑φ ⁻¹' (b⁻¹ • K)
⊢ b * φ x ∉ K
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = Gamma (1 / p + 1)

Tactic:
by
  convert! (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1
  · simp_rw [rpow_zero, one_mul]
  · rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ (x : ι), Measurable ((As x).indicator 1)

Tactic:
exact fun i ↦ Measurable.indicator measurable_const (As_mble i)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
simpa using

Goal state after:
case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A