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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
| ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
Real.norm_of_nonneg (by positivity)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
| ‖g₁ x‖ + ‖g₂ x‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
h1s : support f ⊆ s
⊢ IntegrableOn f s μ ↔ Integrable f μ

Tactic:
refine ⟨fun h => ?_, fun h => h.integrableOn⟩
  refine h.integrable_of_forall_notMem_eq_zero fun x hx => ?_
  contrapose! hx
  exact h1s (mem_support.2 hx)

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

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable f μ

pp: case refine_2
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ

Tactic:
· rw [← indicator_add_eq_left h]; exact hfg.indicator hf.measurableSet_support

Goal state after:
case refine_2
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ ∧ HasFiniteIntegral (fun x ↦ f x • c) μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ

Tactic:
and_congr_right_iff,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ AEStronglyMeasurable f μ → (HasFiniteIntegral (fun x ↦ f x • c) μ ↔ HasFiniteIntegral f μ)
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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι

Tactic:
have := (norm_nonneg x).trans hx

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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
ε : ℝ
hε : ∀ x ∈ (s, r).1, ‖x‖ ≤ ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ε ^ Fintype.card ι * δ < (s, r).2
f : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
hf : ‖f‖ ≤ δ
hx : ‖x‖ ≤ ε
this : 0 ≤ ε
⊢ ‖f‖ * ε ^ Fintype.card ι ≤ δ * ε ^ Fintype.card ι
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case succ
𝕜 : 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
⊢ Continuous[inst✝⁴, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
have : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite
    -- first step: thanks to the induction hypothesis, any n-dimensional subspace is equivalent
    -- to a standard space of dimension n, hence it is complete and therefore closed.
    have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by
      intro s s_dim
      let : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup
      let b := Basis.ofVectorSpace 𝕜 s
      have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by
        have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by
          rw [← s_dim]
          exact (finrank_eq_card_basis b).symm
        have : Continuous b.equivFun := IH b inferInstance this
        exact
          b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this
      have : IsComplete (s : Set E) :=
        completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)
      exact this.isClosed
    -- second step: any linear form is continuous, as its kernel is closed by the first step
    have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by
      intro f
      by_cases H : finrank 𝕜 (LinearMap.range f) = 0
      · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H
        rw [H]
        exact continuous_zero
      · have : finrank 𝕜 (LinearMap.ker f) = n := by
          have Z := f.finrank_range_add_finrank_ker
          rw [finrank_eq_card_basis ξ, hn] at Z
          have : finrank 𝕜 (LinearMap.range f) = 1 :=
            le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)
          rw [this, add_comm, Nat.add_one] at Z
          exact Nat.succ.inj Z
        have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this
        exact LinearMap.continuous_of_isClosed_ker f this
    rw [continuous_pi_iff]
    intro i
    change Continuous (ξ.coord i)
    exact H₂ (ξ.coord i)

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
exact ⟨t, t_mem, ht.mono_enorm hg.restrict (ae_restrict_of_ae h)⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 (E ⧸ s)
s_closed : IsClosed[inst✝⁴] ↑s
s_le_t : s ≤ t
⊢ IsClosed[inst✝⁴] ↑(comap s.mkQ (map s.mkQ t))

Tactic:
exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
s t : Submodule 𝕜 E
hs : IsClosed[inst✝³] ↑s
ht : FiniteDimensional 𝕜 ↥t
⊢ IsClosed[inst✝³] ↑(comap s.mkQ (map s.mkQ t))

Tactic:
exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
x y : G
⊢ f.smulRight (x + y) = f.smulRight x + f.smulRight y

Tactic:
by ext; simp

Goal state after:
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 ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Tactic:
rw [nhdsWithin_inter_of_mem (nhdsWithin_le_nhds <| hU.mem_nhds hx.1)]

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 ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[Z] x) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f g : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (f + g).flipMultilinear = f.flipMultilinear + g.flipMultilinear

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
c : 𝕜
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ (c • f).flipMultilinear = (RingHom.id 𝕜) c • f.flipMultilinear

Tactic:
by ext; simp

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrable f μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrable g μ

Tactic:
← locallyIntegrableOn_univ

Goal state after:
X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g univ μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
F : Type u_7
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrable f μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrable g μ

Tactic:
← locallyIntegrableOn_univ

Goal state after:
X : Type u_1
E : Type u_6
F : Type u_7
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure X
f : X → E
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case neg
β : 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
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Tactic:
have h_bound n :
    (fun x ↦ ‖approxOn f hf s y₀ h₀ n x - f x‖ₑ ^ p.toReal) ≤ᵐ[μ] (‖f · - y₀‖ₑ ^ p.toReal) :=
    .of_forall fun x => rpow_le_rpow (coe_mono (nnnorm_approxOn_le hf h₀ x n)) toReal_nonneg

Goal state after:
case neg
β : 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
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
h_fin : (map (fun x ↦ ‖x‖ₑ ^ p.toReal) f).FinMeasSupp μ
hf_fin : f.FinMeasSupp μ
⊢ μ (⇑f ⁻¹' {y}) < ∞

Tactic:
exact hf_fin.meas_preimage_singleton_ne_zero hy_ne

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x

Tactic:
by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]

Goal state after:
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 α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun x ↦ ‖∫ (x : α) in s x, f x ∂μ‖) l (𝓝 0)

Tactic:
← coe_nnnorm,

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun x ↦ ↑‖∫ (x : α) in s x, f x ∂μ‖₊) l (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = L1.SimpleFunc.integral (f.toLp ⋯)

Tactic:
L1.SimpleFunc.integral_eq_integral

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (f.toLp ⋯))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case lhs
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun x ↦ f x (p • a + q • b)) μ

pp: case rhs
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun x ↦ p • f x a + q • f x b) μ

pp: case ae_le
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun x ↦ f x (p • a + q • b)) ≤ᵐ[μ] fun x ↦ p • f x a + q • f x b

Tactic:
case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq

Goal state after:
case rhs
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun x ↦ p • f x a + q • f x b) μ

case ae_le
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun x ↦ f x (p • a + q • b)) ≤ᵐ[μ] fun x ↦ p • f x a + q • f x b
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
c : ℝ
f : ↥(α →₁ₛ[μ] E)
⊢ ⇑(toSimpleFunc (c • f)) =ᵐ[μ] ⇑(c • toSimpleFunc f)

Tactic:
exact smul_toSimpleFunc c f

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(α →₁ₛ[μ] E)
⊢ ⇑(toSimpleFunc (c • f)) =ᵐ[μ] ⇑(c • toSimpleFunc f)

Tactic:
exact smul_toSimpleFunc c f

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖

Tactic:
rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖