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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp (⇑f) p μ

Tactic:
hp_top

Goal state after:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ∞
hp0 : ¬p = 0
hp_top : p = ∞
⊢ MemLp ⇑f ∞ μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
x : 𝕜
⊢ x • 0 = 0

Tactic:
ext1; exact smul_zero _

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝⁷ : DivisionRing 𝕜
inst✝⁶ : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup Eₗ
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜₂ F
inst✝ : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
⊢ g.ker ≤ f.ker

Tactic:
obtain ⟨C, h⟩ := h

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝⁷ : DivisionRing 𝕜
inst✝⁶ : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup Eₗ
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜₂ F
inst✝ : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
⊢ g.ker ≤ f.ker
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝⁷ : DivisionRing 𝕜
inst✝⁶ : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup Eₗ
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜₂ F
inst✝ : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
h : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
⊢ ∃ C, ∀ (x : ↥g.range), ‖(g.ker.liftQ f ⋯ ∘ₛₗ ↑g.quotKerEquivRange.symm) x‖ ≤ C * ‖x‖

Tactic:
obtain ⟨C, h⟩ := h

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝⁷ : DivisionRing 𝕜
inst✝⁶ : DivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup Eₗ
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜₂ F
inst✝ : Module 𝕜 Eₗ
f : E →ₛₗ[σ₁₂] F
g : E →ₗ[𝕜] Eₗ
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
⊢ ∃ C_1, ∀ (x : ↥g.range), ‖(g.ker.liftQ f ⋯ ∘ₛₗ ↑g.quotKerEquivRange.symm) x‖ ≤ C_1 * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : Eₗ
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
have h_mem : ∀ (x : Eₗ) (hy : x ∈ (LinearMap.range e)), ‖extendOfNorm f e x‖ ≤ C * ‖x‖ := by
    intro x ⟨y, hxy⟩
    simpa only [← hxy, extendOfNorm_eq h_dense ⟨C, h_norm⟩ y] using h_norm y
  exact h_dense.induction h_mem (isClosed_le (by fun_prop) (by fun_prop)) x

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ setToSimpleFunc T f = ∑ x ∈ s, (T (⇑f ⁻¹' {x})) x

Tactic:
setToSimpleFunc_eq_sum_filter,

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
⊢ ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x = ∑ x ∈ s, (T (⇑f ⁻¹' {x})) x
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 α
⊢ setToSimpleFunc (weightedSMul μ) f = ∑ x ∈ f.range with x ≠ 0, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
setToSimpleFunc_eq_sum_filter,

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
hx_nonneg : ∀ (n : ℕ), 0 ≤ x n
hx_memLp : ∀ (n : ℕ), MemLp (⇑(x n)) p μ
h_toLp : ∀ (n : ℕ), ↑↑(MemLp.toLp ⇑(x n) ⋯) =ᵐ[μ] ⇑(x n)
n : ℕ
a : α
ha0 : ↑↑↑0 a = 0 a
ha_toLp : ↑↑(MemLp.toLp ⇑(x n) ⋯) a = (x n) a
⊢ 0 a ≤ (x n) a

Tactic:
exact hx_nonneg n a

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

Goal state before:
pp: case neg.hSp
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ {b ∈ f.range | g b = g (f a)}, μ (⇑f ⁻¹' {i}) ≠ ∞

pp: case neg.h_disj
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ {b ∈ f.range | g b = g (f a)}, ∀ j ∈ {b ∈ f.range | g b = g (f a)}, i ≠ j → Disjoint (⇑f ⁻¹' {i}) (⇑f ⁻¹' {j})

Tactic:
· grind

Goal state after:
case neg.h_disj
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ {b ∈ f.range | g b = g (f a)}, ∀ j ∈ {b ∈ f.range | g b = g (f a)}, i ≠ j → Disjoint (⇑f ⁻¹' {i}) (⇑f ⁻¹' {j})
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
⊢ (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹ → (toSimpleFunc (posPart f)) a✝¹ = max ((toSimpleFunc f) a✝¹) 0

Tactic:
h₃

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ (toSimpleFunc (posPart f)) a✝¹ = max ((toSimpleFunc f) a✝¹) 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ max ((toSimpleFunc f) a✝¹) 0 = max (↑↑↑f a✝¹) 0

Tactic:
h₃

Goal state after:
case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
a✝¹ : α
a✝ : (toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : (toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ max (↑↑↑f a✝¹) 0 = max (↑↑↑f a✝¹) 0
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v

Tactic:
convert! h.fun_sub (EventuallyEq.refl l v); simp [sub_mul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ

Tactic:
rw [← integral_sub hf.real_toNNReal]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal - ↑(-f a).toNNReal ∂μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun a ↦ ↑(-f a).toNNReal) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : 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✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
x✝ : SeparableSpace ↑(range g ∪ {0})
h₁ : Tendsto (fun n ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂ν))
h₂ : Tendsto (fun n ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∫ (a : α), g a ∂μ ≤ ∫ (a : α), g a ∂ν

Tactic:
apply le_of_tendsto_of_tendsto' h₂ h₁

Goal state after:
case pos
α : 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✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
x✝ : SeparableSpace ↑(range g ∪ {0})
h₁ : Tendsto (fun n ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂ν))
h₂ : Tendsto (fun n ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∀ (x : ℕ),
    SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x) ≤
      SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hp_ne_top : 0 ≠ ∞
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) 0 μ ≤ ε ∧ P g
hf : MemLp f 0 μ
⊢ μ ∅ < ∞

Tactic:
by simp only [measure_empty, zero_lt_top]

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p μ
⊢ μ ∅ < ∞

Tactic:
by simp only [measure_empty, zero_lt_top]

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ∞

pp: case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : ¬x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ∞

Tactic:
· rw [hx0]; simp

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
a✝ : x ∈ (toSimpleFunc f).range
hx0 : ¬x = 0
⊢ ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ∞
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ / ↑r * (↑r * (↑‖z‖)⁻¹ * f z)

Tactic:
rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ ↑‖z‖ ≠ 0
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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
⊢ (setToL1 ⋯) f = (setToL1 hT) f + (setToL1 hT') f

Tactic:
apply setToL1_unique (hT.add hT') (A := setToL1 hT + setToL1 hT') _ f

Goal state after:
α : 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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ ⋯) f = (setToL1 hT + setToL1 hT') ↑f
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∫ (x : X) in s, f x ∂μ = ∑' (x : ↑s), μ.real {↑x} • f ↑x

Tactic:
← integral_subtype_comap hs.measurableSet,

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
hf' : Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∑' (x : ↑s), μ.real {↑x} • f ↑x
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
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
have le_ae : ∀ᵐ a ∂μ, 0 ≤ ‖f a‖ := Eventually.of_forall fun a => norm_nonneg _

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ ↑(Fintype.card ι) * ‖g‖

Tactic:
← nsmul_eq_mul

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : ι → E
⊢ ‖(↑LinearMap.toContinuousLinearMap ∘ₗ ↑(LinearEquiv.piRing 𝕜 E ι 𝕜).symm) g‖ ≤ Fintype.card ι • ‖g‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ ‖∑ x, (v x - u x) • (g x - f x)‖ ≤ ∑ i, ‖g i - f i‖ * ‖v - u‖

Tactic:
refine norm_sum_le_of_le _ fun i _ => ?_

Goal state after:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
⊢ (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ ↑C * M

Tactic:
H

Goal state after:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h : ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
H : ∀ (i : ι), ‖u (v i)‖ ≤ M
⊢ ‖u‖ ≤ ↑C * M
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
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
⊢ Tendsto (fun n ↦ setToFun μ T hT (fs n)) atTop (𝓝 (setToFun μ T hT f))

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  -- `f` is a.e.-measurable, since it is the a.e.-pointwise limit of a.e.-measurable functions.
  have f_measurable : AEStronglyMeasurable f μ :=
    aestronglyMeasurable_of_tendsto_ae _ fs_measurable h_lim
  -- all functions we consider are integrable
  have fs_int : ∀ n, Integrable (fs n) μ := fun n =>
    bound_integrable.mono' (fs_measurable n) (h_bound _)
  have f_int : Integrable f μ :=
    ⟨f_measurable,
      hasFiniteIntegral_of_dominated_convergence bound_integrable.hasFiniteIntegral h_bound
        h_lim⟩
  -- it suffices to prove the result for the corresponding L1 functions
  suffices
    Tendsto (fun n => L1.setToL1 hT ((fs_int n).toL1 (fs n))) atTop
      (𝓝 (L1.setToL1 hT (f_int.toL1 f))) by
    convert! this with n
    · exact setToFun_eq hT (fs_int n)
    · exact setToFun_eq hT f_int
  -- the convergence of setToL1 follows from the convergence of the L1 functions
  refine L1.tendsto_setToL1 hT _ _ ?_
  -- up to some rewriting, what we need to prove is `h_lim`
  rw [tendsto_iff_norm_sub_tendsto_zero]
  have lintegral_norm_tendsto_zero :
    Tendsto (fun n => ENNReal.toReal <| ∫⁻ a, ENNReal.ofReal ‖fs n a - f a‖ ∂μ) atTop (𝓝 0) :=
    (tendsto_toReal zero_ne_top).comp
      (tendsto_lintegral_norm_of_dominated_convergence fs_measurable
        bound_integrable.hasFiniteIntegral h_bound h_lim)
  convert! lintegral_norm_tendsto_zero with n
  rw [L1.norm_def]
  congr 1
  refine lintegral_congr_ae ?_
  rw [← Integrable.toL1_sub]
  refine ((fs_int n).sub f_int).coeFn_toL1.mono fun x hx => ?_
  dsimp only
  rw [hx, ofReal_norm, Pi.sub_apply]

Goal state after: