mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ∞
⊢ ∞ ^ p ≤ ∞ * ∞ ^ (p - 1)

Tactic:
ENNReal.top_rpow_of_pos hpq.sub_one_pos,

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ∞
⊢ ∞ ^ p ≤ ∞ * ∞
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ∞
⊢ ∞ ^ p ≤ ∞ * ∞

Tactic:
ENNReal.top_mul_top

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ∞
⊢ ∞ ^ p ≤ ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ ENNReal.ofReal ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ =
    ENNReal.ofReal (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖)

Tactic:
rw [Real.norm_of_nonneg _]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
p : ℝ
hp1 : 1 ≤ p
B : ℕ → ℝ≥0∞
n : ℕ
hp_pos : 0 < p
hn : (∫⁻ (a : α), ‖∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖‖ₑ ^ p ∂μ) ^ p⁻¹ ≤ ∑' (i : ℕ), B i
a : α
⊢ 0 ≤ ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
⊢ ↑↑0 a✝ = 0 a✝ → (g ∘ ↑↑0) a✝ = 0 a✝

Tactic:
ha

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
a✝ : α
ha : ↑↑0 a✝ = 0 a✝
⊢ (g ∘ ↑↑0) a✝ = 0 a✝
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_3.a.inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
hw : w i ≠ 0
⊢ w i * f i = w i * ↑(f i).toNNReal

Tactic:
coe_toNNReal

Goal state after:
case e'_3.a.inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
hw : w i ≠ 0
⊢ w i * f i = w i * f i

case e'_3.a.inr
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x).toNNReal * ↑(f x).toNNReal ≤ (∑ i ∈ s, ↑(w i).toNNReal) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
i : ι
hi : i ∈ s
hw : w i ≠ 0
⊢ f i ≠ ∞
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ ‖x‖

Tactic:
apply opNorm_lsmul_apply_le

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 fun x ↦ x.2

Tactic:
refine (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_
  rw [one_mul]
  exact le_max_right _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = ‖x‖ ∧ 1 ≤ ‖x‖
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

pp: case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖

Tactic:
· grw [hx.1]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E
C : ℝ
hC_pos : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
y : F
hx : max ‖x‖ 1 = 1 ∧ ‖x‖ < 1
⊢ C * ‖x‖ * ‖y‖ ≤ C * max ‖x‖ 1 * ‖y‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: case hf.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
⊢ Prod.snd =O[𝓝 x] fun _x ↦ 1

Tactic:
exact (continuous_snd.tendsto _).isBigO_one ℝ

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = T ∘SL f

Tactic:
by
  simpa [← toLinearMap_comp] using
    LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap

Goal state after:
Module: Mathlib.Topology.Homeomorph.Quotient

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
r : X → X → Prop
e : X ≃ₜ Y
x✝¹ x✝ : X
⊢ r x✝¹ x✝ ↔ r (e.symm (e x✝¹)) (e.symm (e x✝))

Tactic:
simp only [e.symm_apply_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
⊢ (↑(f a) ≠ 0 → g a = g' a) → f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a

Tactic:
ha

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
⊢ f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ.real sᶜ = 1 - μ.real s

Tactic:
rw [measureReal_compl₀ h, probReal_univ]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable (s.piecewise f g) μ

Tactic:
rw [IntegrableOn] at hf hg

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : Integrable f (μ.restrict s)
hg : Integrable g (μ.restrict sᶜ)
⊢ Integrable (s.piecewise f g) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
a✝ : α
⊢ a✝ ∈ {x} → f a✝ = f x

Tactic:
ha

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
a✝ : α
ha : a✝ ∈ {x}
⊢ f a✝ = f x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f - g) μ

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
n : ℕ
⊢ μ (v n ∩ s) ≠ ∞

Tactic:
← Measure.restrict_apply (measurableSet_toMeasurable _ _),

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
n : ℕ
⊢ (μ.restrict s) (toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}) ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
    intro n
    rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]
    exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ∞
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
⊢ ‖f₀ a - f₁ a‖ ≤ g a → ‖f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₁ a‖ ≤ ‖f₀ a‖ + g a
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
A : IntegrableOn f v μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
h'x : x ∈ s
H : ¬0 = f x
⊢ False

Tactic:
exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : α → E
c : 𝕜
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (c • f) l μ

Tactic:
exact ⟨s, sl, hs.smul c⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
a : α
⊢ a ∈ t → f a ∈ f '' s

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
f : α → β
s t : Set α
μ : Measure α
hf : ContinuousOn f s
hs : IsCompact s
ht : MeasurableSet t
hts : t ⊆ s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
a : α
ha : a ∈ t
⊢ f a ∈ f '' s
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
⊢ ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝ → ‖↑↑(f - g) a✝‖ₑ = ‖↑↑f a✝ - ↑↑g a✝‖ₑ

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ ‖↑↑(f - g) a✝‖ₑ = ‖↑↑f a✝ - ↑↑g a✝‖ₑ
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
⊢ ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝ → edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
a✝ : α
ha : ↑↑(f - g) a✝ = (↑↑f - ↑↑g) a✝
⊢ edist (↑↑(f - g) a✝) 0 = edist (↑↑f a✝ - ↑↑g a✝) 0
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ∑ e, ‖(f.iteratedFDerivComponent e.toEquivRange) fun i ↦ x ↑i‖ ≤ ∑ x_1, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
gcongr with e _

Goal state after:
case h
𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
e : Fin k ↪ ι
a✝ : e ∈ univ
⊢ ‖(f.iteratedFDerivComponent e.toEquivRange) fun i ↦ x ↑i‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace ε
inst✝³ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝² : PseudoMetrizableSpace ε
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Iic a) μ

Tactic:
refine (integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace ε
inst✝³ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝² : PseudoMetrizableSpace ε
a : X
inst✝¹ : LinearOrder X
inst✝ : CompactIccSpace X
x✝ : IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ
s : Set X
hsl : s ∈ atBot
hs : IntegrableOn f s μ
h : LocallyIntegrableOn f (Iic a) μ
this : Nonempty X
a' : X
ha' : ∀ b ≤ a', b ∈ s
⊢ IntegrableOn f (Icc a' a) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : μ s ≠ ∞
this : Fact (μ s < ∞)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
a : X
⊢ a ∈ s → ‖f a‖ ≤ C

Tactic:
ha

Goal state after:
X : Type u_1
E : Type u_6
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : μ s ≠ ∞
this : Fact (μ s < ∞)
C : ℝ
hC : ∀ x ∈ f '' K, ‖x‖ ≤ C
a : X
ha : a ∈ s
⊢ ‖f a‖ ≤ C
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] fun x ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
⊢ f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
    Tendsto (fun x ↦ ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)

Tactic:
ha

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
hF_meas : ∀ (n : ℕ), Measurable fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal
h_bound : ∀ (n : ℕ), (fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] fun x ↦ ‖f x - y₀‖ₑ ^ p.toReal
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
a : β
ha : f a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun x ↦ ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
⊢ (∀ i ∈ insert a s, μ (S i) ≠ ∞) →
    (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)) →
      T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)

Tactic:
hps

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
⊢ (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)) →
    T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ) atTop (𝓝 0)

Tactic:
apply tendsto_approxOn_L1_enorm fmeas

Goal state after:
case hμ
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range f ∪ {0})

case hi
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
μ : Measure β
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
fmeas : Measurable f
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ f x - 0) μ