mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤[i] v

Tactic:
restrict_zero,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ 0 ≤ v.restrict i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ v ≤[i] 0

Tactic:
restrict_zero,

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v : VectorMeasure α M
i : Set α
hi : ¬MeasurableSet i
⊢ v.restrict i ≤ 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
⊢ UnifIntegrable (fun x ↦ g) p μ

Tactic:
by
  intro ε hε
  obtain ⟨δ, hδ_pos, hgδ⟩ := hg.eLpNorm_indicator_le hp hp_ne_top hε
  exact ⟨δ, hδ_pos, fun _ => hgδ⟩

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v : VectorMeasure α M
w : VectorMeasure α N
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
s : Set α
hs : s ⊆ u
⊢ v s = 0

Tactic:
exact hu₁ s hs

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
by
  by_cases hf : Integrable f μ
  · refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_
    rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
    rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
  · rw [withDensityᵥ, dif_neg hf]
    exact VectorMeasure.AbsolutelyContinuous.zero _

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν

Tactic:
rw [Measure.le_iff, VectorMeasure.le_iff]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (∀ (i : Set α), MeasurableSet i → μ.toSignedMeasure i ≤ ν.toSignedMeasure i) ↔
    ∀ (s : Set α), MeasurableSet s → μ s ≤ ν s
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable (s.rnDeriv μ)

Tactic:
rnDeriv_def

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable fun x ↦
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun μ ↦ (↑μ.1).prod ↑μ.2

Tactic:
by
  apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure generateFrom_prod.symm
    isPiSystem_prod _
  simp only [mem_image2, mem_ofPred_eq, forall_exists_index, and_imp]
  intro _ u Hu v Hv Heq
  simp_rw [← Heq, Measure.prod_prod]
  apply Measurable.mul
  · exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)
  · exact (Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : ProbabilityMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
⊢ (ν.map f_aemble) A = ν (f ⁻¹' A)

Tactic:
by
  exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <|
    ν.map_apply' f_aemble A_mble

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), μ {x | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact ⟨C, fun i => hδ i _ (measurableSet_le measurable_const (hf i).nnnorm.measurable) (hC i)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
⊢ ContinuousSMul ℝ≥0 (FiniteMeasure Ω)

Tactic:
by
  refine ⟨continuous_iff_continuousAt.2 (fun p ↦ ?_)⟩
  apply tendsto_iff_forall_integral_tendsto.2 (fun g ↦ ?_)
  have A : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ i.1) (𝓝 p) (𝓝 (p.1)) := by
    rw [nhds_prod_eq]
    exact tendsto_fst
  have B : Tendsto (fun (i : ℝ≥0 × FiniteMeasure Ω) ↦ ∫ x, g x ∂i.2) (𝓝 p)
      (𝓝 (∫ x, g x ∂p.2)) := by
    rw [nhds_prod_eq]
    exact (tendsto_iff_forall_integral_tendsto.1 tendsto_id g).comp tendsto_snd
  convert! A.smul B with q <;> simp

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω : (κ ω) (f ⁻¹' s ∩ g ⁻¹' t) = (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t)
hωu : ω ∉ u
⊢ ((κ.map fun ω ↦ (f ω, g ω)) ω) (if ω ∈ u then s ×ˢ t else ∅) = ((κ.map f ×ₖ κ.map g) ω) (if ω ∈ u then s ×ˢ t else ∅)

pp: case pos
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω : (κ ω) (f ⁻¹' s ∩ g ⁻¹' t) = (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t)
hωu : ω ∈ u
⊢ ((κ.map fun ω ↦ (f ω, g ω)) ω) (if ω ∈ u then s ×ˢ t else ∅) = ((κ.map f ×ₖ κ.map g) ω) (if ω ∈ u then s ×ˢ t else ∅)

Tactic:
· simp [hωu]

Goal state after:
case pos
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ (s : Set β) (t : Set γ),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
u : Set α
s : Set β
t : Set γ
hu : MeasurableSet u
hs : MeasurableSet s
ht : MeasurableSet t
h_set_eq : ∀ (ω : α), Prod.mk ω ⁻¹' u ×ˢ s ×ˢ t = if ω ∈ u then s ×ˢ t else ∅
ω : α
hω : (κ ω) (f ⁻¹' s ∩ g ⁻¹' t) = (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t)
hωu : ω ∈ u
⊢ ((κ.map fun ω ↦ (f ω, g ω)) ω) (if ω ∈ u then s ×ˢ t else ∅) = ((κ.map f ×ₖ κ.map g) ω) (if ω ∈ u then s ×ˢ t else ∅)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
⊢ HasPDF (g ∘ X) ℙ ν

Tactic:
have hgm : AEMeasurable g (map X ℙ) := hg.aemeasurable.mono_ac HasPDF.absolutelyContinuous
  rw [hasPDF_iff, ← AEMeasurable.map_map_of_aemeasurable hgm (HasPDF.aemeasurable X ℙ μ)]
  refine ⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩
  exact (HasPDF.absolutelyContinuous.map hg.1).trans hg.2

Goal state after:
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
hY : MemLp Y 2 μ
⊢ cov[fun ω ↦ ∑ i, X i ω, Y; μ] = ∑ i, cov[X i, Y; μ]

Tactic:
by
  convert! covariance_sum_left hX hY
  simp

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

Goal state before:
pp: case e'_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝⁶ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝⁴ : TopologicalSpace E
F : Type u_6
inst✝³ : OpensMeasurableSpace E
inst✝² : TopologicalSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
g : E → F
hg : Continuous[inst✝⁴, inst✝²] g
h : TendstoInDistribution X l Z μ μ'
x✝ : ι
⊢ ⟨Measure.map (g ∘ X x✝) (μ x✝), ⋯⟩ = ProbabilityMeasure.map ⟨Measure.map (X x✝) (μ x✝), ⋯⟩ ⋯

Tactic:
simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk, Subtype.mk.injEq]
      rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable (h.forall_aemeasurable _)]

Goal state after:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
⊢ ∫ (x : Ω), (∏ i, f i ∘ X i) x ∂μ = ∏ i, ∫ (x : Ω), (f i ∘ X i) x ∂μ

Tactic:
convert! hX.integral_fun_prod_comp mX hf
  simp

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕₊ v
hnv : (𝓝[>] v).NeBot
⊢ ↑𝓕₊ v ≤ ↑𝓕 u

pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕₊ v
hnv : ¬(𝓝[>] v).NeBot
⊢ ↑𝓕₊ v ≤ ↑𝓕 u

Tactic:
· simpa [rightCont_eq_of_neBot_nhdsGT] using iInf₂_le_of_le u hv.2 le_rfl

Goal state after:
case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : (𝓝[>] i).NeBot
u : ι
hu : u > i
hiou : Set.Ioo i u ∈ 𝓝[>] i
v : ι
hv : v ∈ Set.Ioo i u
hle₁ : ⨅ j, ⨅ (_ : j > i), ↑𝓕₊ j ≤ ↑𝓕₊ v
hnv : ¬(𝓝[>] v).NeBot
⊢ ↑𝓕₊ v ≤ ↑𝓕 u
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ |sinc x| ≤ 1

Tactic:
exact abs_sinc_le_one x

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✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
by_cases Fi : Finite ι
  · refine ⟨fun n => simpleFunc_piecewise hs hm (fun i => (hf i).approx n), fun x => ?_⟩
    simp [simpleFunc_piecewise, piecewise_apply, StronglyMeasurable.tendsto_approx]
  simp only [not_finite_iff_infinite] at Fi
  obtain ⟨e, -⟩ := exists_true_iff_nonempty.mpr (nonempty_equiv_of_countable (α := ℕ) (β := ι))
  classical
  let g (n : ℕ) (i : ι) : Fin (n + 1) :=
    if hi : ∃ m < n, i = e m then ⟨hi.choose, by grind⟩ else Fin.last n
  have sg (n : ℕ) : (g n).Surjective := by
    intro b
    unfold g
    refine ⟨e b, ?_⟩
    by_cases hb : b < n
    · have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using! e.injective this.choose_spec.2.symm
    · simp [hb]
      grind
  have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
  refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
  · exact .biUnion (to_countable _) fun _ _ ↦ hm _
  simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]
  have : ∀ᶠ n in atTop, e ((G n).index x) = hs.index x := by
    obtain ⟨y, hy⟩ := e.bijective.2 (hs.index x)
    refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩
    have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
    rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]
    have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
    simpa [g, hs.mem_iff_index_eq, this] using! e.injective (hy.trans this.choose_spec.2).symm
  have : ∀ᶠ n in atTop, (hf (hs.index x)).approx n x = (hf (e ((G n).index x))).approx n x := by
    filter_upwards [this] with n hn using by rw [hn]
  exact (Filter.tendsto_congr' this).mp (by simp [StronglyMeasurable.tendsto_approx])

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
rcases hf (pos_iff_ne_zero.2 (toNNReal_ne_zero.mpr ⟨hε,hε_top⟩)) with ⟨s, hμs, hfs⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ¬ε = ∞
s : Set α
hμs : μ s ≠ ∞
hfs : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε.toNNReal
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (f + g) p μ < ↑ε
hη_top : η = ∞
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε

Tactic:
replace hη := hη_top ▸ hη
    refine ⟨∅, (by simp), fun i ↦ ?_⟩
    simp only [compl_empty, indicator_univ, Pi.add_apply]
    exact (hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le

Goal state after:
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✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h : μ F * 2 ^ finrank ℝ E < μ s
⊢ μ F < μ (2⁻¹ • s)

Tactic:
rw [addHaar_smul_of_nonneg μ (by simp : 0 ≤ (2 : ℝ)⁻¹) s,
      ← ENNReal.mul_lt_mul_iff_left (pow_ne_zero (finrank ℝ E) (two_ne_zero' _)) (by finiteness),
      mul_right_comm, ofReal_pow (by simp : 0 ≤ (2 : ℝ)⁻¹), ofReal_inv_of_pos zero_lt_two]

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✝¹ : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝ : Countable ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h : μ F * 2 ^ finrank ℝ E < μ s
⊢ μ F * 2 ^ finrank ℝ E < (ENNReal.ofReal 2)⁻¹ ^ finrank ℝ E * 2 ^ finrank ℝ E * μ s
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ circleMap 0 R i.2 * I) (closedBall z r ×ˢ univ)

Tactic:
apply_rules [ContinuousOn.mul, (continuous_circleMap 0 R).comp_continuousOn continuousOn_snd,
        continuousOn_const]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ AEStronglyMeasurable (Eᶜ.indicator (f n)) μ

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ AEStronglyMeasurable (Eᶜ.indicator g) μ

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ

Tactic:
by assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ AEStronglyMeasurable (E.indicator (f n - g)) μ

Tactic:
by assumption

Goal state after: