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

Goal state before:
pp: case inr.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
p r : ℝ≥0∞
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hpqr✝ : p.HolderTriple 0 r
hpqr : 1 / r = 1 / p + 1 / 0
⊢ eLpNorm (fun x ↦ b (f x) (g x)) r μ ≤ ↑c * eLpNorm f p μ * eLpNorm g 0 μ

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
induction s using cons_induction with

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

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

pp: case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ¬ε = ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
· have h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0) := h 1 (by simp) (by simp)
    refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le) ?_
    intro n
    simp only [hε_top]
    gcongr
    simp

Goal state after:
case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ¬ε = ∞
⊢ Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∈ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst✝¹ : PseudoEMetricSpace F
inst✝ : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : x ∈ {x | ε ≤ edist ((fun i ↦ s.indicator (f i)) n x) (s.indicator g x)}
h✝ : x ∉ s
⊢ x ∈ {x | ε ≤ edist (f n x) (g x)}

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : ↥(Lp E p μ)
⊢ dist f g = (eLpNorm (↑↑f - ↑↑g) p μ).toReal

Tactic:
rw [dist_eq_eLpNorm_neg_add, ← eLpNorm_neg, neg_add, neg_neg, sub_eq_add_neg]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ∑' (i : ℕ), B1 i < ∞

Tactic:
rw [hB1_has.tsum_eq]

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : Fact (1 ≤ p)
H :
  ∀ (f : ℕ → α → E),
    (∀ (n : ℕ), MemLp (f n) p μ) →
      ∀ (B : ℕ → ℝ≥0∞),
        ∑' (i : ℕ), B i < ∞ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) →
            ∃ f_lim, MemLp f_lim p μ ∧ Tendsto (fun n ↦ eLpNorm (f n - f_lim) p μ) atTop (𝓝 0)
B : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
hB_pos : ∀ (n : ℕ), 0 < B n
f : ℕ → ↥(Lp E p μ)
hf : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → dist (f n) (f m_1) < B N
M : ℝ
hB : HasSum B M
B1 : ℕ → ℝ≥0∞ := fun n ↦ ENNReal.ofReal (B n)
hB1_has : HasSum B1 (ENNReal.ofReal M)
⊢ ENNReal.ofReal M < ∞
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ∞
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
rcases H' with H' | H' <;> simp [H', -one_div]

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
have :=
    ENNReal.coe_le_coe.2
      (@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _
        hp)

Goal state after:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ↑((∑ i ∈ s, ((f i).toNNReal + (g i).toNNReal) ^ p) ^ (1 / p)) ≤
    ↑((∑ i ∈ s, (f i).toNNReal ^ p) ^ (1 / p) + (∑ i ∈ s, (g i).toNNReal ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  (∑ i ∈ s, (↑(f i).toNNReal + ↑(g i).toNNReal) ^ p) ^ (1 / p) ≤
    (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ (1 / p) + (∑ x ∈ s, ↑(g x).toNNReal ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ max (↑↑(-f) a✝) 0 = max (-↑↑f a✝) 0

Tactic:
h₂,

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ max ((-↑↑f) a✝) 0 = max (-↑↑f a✝) 0
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f ↦ negPart f

Tactic:
unfold negPart

Goal state after:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
⊢ Continuous fun f ↦ posPart (-f)
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: case refine_2
𝕜 : 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
a : R
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : E), ‖((lsmul 𝕜 R) a) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ ‖a‖ * ‖y‖ ≤ N * ‖y‖

Tactic:
simpa [norm_smul] using h y

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝⁴ : Fintype ι
this✝³ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝² : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝¹ : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this✝ : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
this : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) = n
⊢ IsUniformEmbedding ⇑b.equivFun.symm.toEquiv

Tactic:
have : Continuous b.equivFun := IH b inferInstance this

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝⁵ : Fintype ι
this✝⁴ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝³ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this✝² : FiniteDimensional 𝕜 E
s : Submodule 𝕜 E
s_dim : finrank 𝕜 ↥s = n
this✝¹ : IsUniformAddGroup ↥s := AddSubgroup.isUniformAddGroup s.toAddSubgroup
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 ↥s)) 𝕜 ↥s := Basis.ofVectorSpace 𝕜 ↥s
this✝ : Fintype.card ↑(Basis.ofVectorSpaceIndex 𝕜 ↥s) = n
this : Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace] ⇑b.equivFun
⊢ IsUniformEmbedding ⇑b.equivFun.symm.toEquiv
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
h' : ∀ s ∈ l, μ s = ∞
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ∞
⊢ μ v < ∞

Tactic:
simpa only [Measure.restrict_apply_self]

Goal state after:
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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
⊢ ‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖

Tactic:
have : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1 := by
    simp [zero_le_one, norm_le_of_mem_closedBall (le_of_lt h')]

Goal state after:
𝕜 : 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 : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ ‖f m' - f m‖ ≤ D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
⊢ AEMeasurable f (μ.restrict s)

Tactic:
← Measure.restrict_congr_set t_eq_s

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
t : Set α
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
⊢ AEMeasurable f (μ.restrict t)
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case inl
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
f : ι → X → E
inst✝¹ : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ MeasurableSet {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) ⊥ (𝓝 c)}

Tactic:
simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
x : Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 x
hU_tb : TotallyBounded U
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
by
  replace hU_nhds : x +ᵥ (-x) +ᵥ U ∈ 𝓝 x := by simpa
  rw [vadd_mem_nhds_self] at hU_nhds
  refine .of_totallyBounded_nhds_zero _ hU_nhds ?_
  have : -x +ᵥ U = (· - x) '' U := by simp [← Set.image_vadd, neg_add_eq_sub]
  exact this ▸ hU_tb.image (uniformContinuous_id.sub uniformContinuous_const)

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

Goal state before:
pp: case singleton
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
ι : Type u_8
s : Finset ι
μ : ι → Measure α
T : ι → Set α → β
C : ι → ℝ
hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
⊢ DominatedFinMeasAdditive (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) ({i}.sup' ⋯ C)

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : DecidablePred fun x ↦ x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ integral μ f = ∑ x ∈ f.range with x ≠ 0, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : μ s + ν s ≠ ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
ENNReal.add_ne_top

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : μ s ≠ ∞ ∧ ν s ≠ ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : 0 ≤ f x
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x

Tactic:
obtain (hx | hx) := hx.eq_or_lt

Goal state after:
case pos.inl
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx✝ : 0 ≤ f x
hx : 0 = f x
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x

case pos.inr
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx✝ : 0 ≤ f x
hx : 0 < f x
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
y : α
hy : y ∈ ⇑f ⁻¹' {f x}
⊢ y ∈ {a | ¬0 a ≤ f a}

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous ⇑integralCLM

Tactic:
exact (integralCLM (E := E)).continuous

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous fun x ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] ℝ)), integral ↑a = ‖Lp.posPart ↑a‖ - ‖Lp.negPart ↑a‖

Tactic:
· refine Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
      (continuous_norm.comp Lp.continuous_negPart)

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] ℝ)), integral ↑a = ‖Lp.posPart ↑a‖ - ‖Lp.negPart ↑a‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ edist (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ≤ ∫⁻ (a : α), edist (f a) (g a) ∂μ

Tactic:
by
  rw [edist_dist]
  exact ENNReal.ofReal_le_of_le_toReal (dist_integral_le_lintegral_edist hf hg)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ‖max (↑↑f₁ a✝) 0‖ₑ

Tactic:
h₂,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (f a✝) = ‖max (f a✝) 0‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖-min (↑↑f₁ a✝) 0‖ₑ

Tactic:
h₂,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖-min (f a✝) 0‖ₑ
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : ¬s = ∅
⊢ Bornology.IsBounded ((fun x ↦ x ^ 0) '' s)

Tactic:
simp_rw [← nonempty_iff_ne_empty] at s_empty

Goal state after:
case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s.Nonempty
⊢ Bornology.IsBounded ((fun x ↦ x ^ 0) '' s)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = ENNReal.ofReal ((∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)

Tactic:
integral_eq_lintegral_of_nonneg_ae

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ 0 ≤ᵐ[μ] fun a ↦ ‖f a‖ ^ p.toReal

case hfm
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖ ^ p.toReal) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
⊢ ∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ

Tactic:
by
  -- First we consider the “degenerate” case `c = ∞`
  rcases eq_or_ne c ∞ with (rfl | hc)
  · rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
  -- Main case: `c ≠ ∞`
  simp_rw [integral_eq_setToFun, ← setToFun_smul_left]
  have hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ) : Set α → G →L[ℝ] G) c.toReal :=
    mul_one c.toReal ▸ (dominatedFinMeasAdditive_weightedSMul (c • μ)).of_smul_measure hc
  have hdfma_smul := dominatedFinMeasAdditive_weightedSMul (F := G) (c • μ)
  rw [← setToFun_congr_smul_measure c hc hdfma hdfma_smul f]
  exact setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : ¬Integrable f (Measure.map φ μ)
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
rw [integral_undef hfi, integral_undef]
    exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)

Goal state after: