mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa using

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✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ AEStronglyMeasurable f μ
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✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst✝³] (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ

Tactic:
simpa using

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✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen[inst✝³] (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
ε''' : Type u_9
inst✝² : TopologicalSpace ε'''
inst✝¹ : ESeminormedAddCommMonoid ε'''
inst✝ : ContinuousAdd ε'''
ι : Type u_10
s : Finset ι
f : ι → X → ε'''
hf : ∀ i ∈ s, LocallyIntegrable (f i) μ
⊢ LocallyIntegrable (fun a ↦ ∑ i ∈ s, f i a) μ

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
ε''' : Type u_9
inst✝² : TopologicalSpace ε'''
inst✝¹ : ESeminormedAddCommMonoid ε'''
inst✝ : ContinuousAdd ε'''
ι : Type u_10
s : Finset ι
f : ι → X → ε'''
hf : ∀ i ∈ s, LocallyIntegrable (f i) μ
⊢ LocallyIntegrable (fun a ↦ (∑ c ∈ s, f c) a) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case pos
β : 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
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
case pos
β : 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
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
i : Subtype (Membership.mem s)
a✝ : i ∈ univ
⊢ ‖if h : ↑i ∈ s then m (e.symm ⟨↑i, ⋯⟩) ↑i else x ⟨↑i, ⋯⟩‖ ≤ ‖m (e.symm i)‖

Tactic:
simpa using

Goal state after:
case h1
𝕜 : 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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : (i : { a // a ∉ s }) → E₁ ↑i
m : α → (i : ι) → E₁ i
i : Subtype (Membership.mem s)
a✝ : i ∈ univ
⊢ ‖m (e.symm i) ↑i‖ ≤ ‖m (e.symm i)‖
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 ι
α : Type u_1
inst✝¹ : Fintype α
f : ContinuousMultilinearMap 𝕜 E₁ G
s : Set ι
e : α ≃ ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∀ (m₁ : (i : { a // a ∉ s }) → E₁ ↑i) (m₂ : α → (i : ι) → E₁ i),
    ‖((f.iteratedFDerivComponent e) m₁) m₂‖ ≤ (‖f‖ * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖

Tactic:
intro x m
    simp only [MultilinearMap.iteratedFDerivComponent, MultilinearMap.domDomRestrictₗ,
      MultilinearMap.coe_mk, MultilinearMap.domDomRestrict_apply, coe_coe]
    apply (f.le_opNorm _).trans _
    classical
    rw [← prod_compl_mul_prod s.toFinset, mul_assoc]
    gcongr
    · apply le_of_eq
      have : ∀ x, x ∈ s.toFinsetᶜ ↔ (fun x ↦ x ∉ s) x := by simp
      rw [prod_subtype _ this]
      congr with i
      simp [i.2]
    · rw [prod_subtype _ (fun _ ↦ s.mem_toFinset), ← Equiv.prod_comp e.symm]
      gcongr with i
      simpa only [i.2, ↓reduceDIte, Subtype.coe_eta] using norm_le_pi_norm (m (e.symm i)) ↑i

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

Goal state before:
pp: 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)

Tactic:
simpa using

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.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
n : ℕ
⊢ Measurable fun x ↦ ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal

Tactic:
simpa using

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
n : ℕ
⊢ Measurable fun x ↦ edist ((approxOn f hf s y₀ h₀ n) x) (f x) ^ p.toReal
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case mpr
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
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ

Tactic:
exact integrableOn_Iic_iff_integrableAtFilter_atBot.mpr
      ⟨hbot, hlocal.mono_set (Iic_subset_Iio.mpr hs'_mono)⟩

Goal state after:
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✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : μ s ≠ ∞
h's : MeasurableSet s
⊢ (μ.restrict s) univ ≠ ∞

Tactic:
simpa using

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✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
hs : μ s ≠ ∞
h's : MeasurableSet s
⊢ ¬μ s = ∞
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
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 ∂μ ≠ ∞
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun x ↦ ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)

Tactic:
simpa using

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
h_fin : ∫⁻ (a : β), ‖f a - y₀‖ₑ ^ p.toReal ∂μ ≠ ∞
h_lim : ∀ᵐ (a : β) ∂μ, Tendsto (fun x ↦ ‖(approxOn f hf s y₀ h₀ x) a - f a‖ₑ ^ p.toReal) atTop (𝓝 0)
⊢ 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: case refine_2
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ∞
⊢ eLpNorm (fun x ↦ f x - 0) p μ < ∞

Tactic:
simpa using

Goal state after:
case refine_2
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ∞
⊢ eLpNorm (fun x ↦ f x) p μ < ∞
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✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
⊢ Tendsto (fun n ↦ MemLp.toLp ⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) atTop (𝓝 (MemLp.toLp f hf))

Tactic:
simpa using

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - ⇑g) p μ < ε
g_mem : MemLp (⇑g) p μ
x : β
hx : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ (f - ⇑g) x = (f' - ⇑g) x

Tactic:
simpa using

Goal state after:
β : Type u_2
inst✝¹ : MeasurableSpace β
p : ℝ≥0∞
E : Type u_7
inst✝ : NormedAddCommGroup E
f : β → E
μ : Measure β
hf : MemLp f p μ
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
f' : β → E := AEStronglyMeasurable.mk f ⋯
g : β →ₛ E
hg : eLpNorm (f' - ⇑g) p μ < ε
g_mem : MemLp (⇑g) p μ
x : β
hx : f x = AEStronglyMeasurable.mk f ⋯ x
⊢ f x = f' x
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: 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) μ

Tactic:
simpa using

Goal state after:
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) μ
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
f : α →ₛ E
g : α →ₛ F
⊢ Integrable (⇑f) μ → Integrable (⇑g) μ → Integrable (⇑(f.pair g)) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
μ : Measure α
f : α →ₛ E
g : α →ₛ F
⊢ f.FinMeasSupp μ → g.FinMeasSupp μ → (f.pair g).FinMeasSupp μ
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 ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
this : support ⇑(const α c) = Set.univ
⊢ μ s < ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
c : E
hc : c ≠ 0
s : Set α
hs : MeasurableSet s
hcs : MemLp (⇑(piecewise s hs (const α c) (const α 0))) p μ
this : support ⇑(const α c) = Set.univ
⊢ μ s < ∞
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
k : 𝕜
f : ↥(simpleFunc E p μ)
⊢ k • ↑f ∈ simpleFunc E p μ

Tactic:
rcases f with ⟨f, ⟨s, hs⟩⟩

Goal state after:
α : 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
k : 𝕜
f : ↥(Lp E p μ)
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hs : AEEqFun.mk ⇑s ⋯ = ↑f
⊢ k • ↑⟨f, ⋯⟩ ∈ simpleFunc E p μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖(-T) s‖ ≤ C * μ.real s

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖T s‖ ≤ C * μ.real s
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case cons
α : 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 : ι
s : Finset ι
his : i ∉ s
hs' : s.Nonempty
ih : DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs' C)
⊢ DominatedFinMeasAdditive (∑ i ∈ cons i s his, μ i) (∑ i ∈ cons i s his, T i) ((cons i s his).sup' ⋯ C)

Tactic:
simpa using

Goal state after:
case cons
α : 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 : ι
s : Finset ι
his : i ∉ s
hs' : s.Nonempty
ih : DominatedFinMeasAdditive (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs' C)
⊢ DominatedFinMeasAdditive (μ i + ∑ i ∈ s, μ i) (T i + ∑ i ∈ s, T i) (max (C i) (s.sup' hs' C))
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ₗ
C : ℝ
x : E
h : ‖f x‖ ≤ C * ‖0‖
hx : x ∈ g.ker
⊢ x ∈ f.ker

Tactic:
simpa using

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 : ℝ
x : E
h : ‖f x‖ ≤ C * ‖0‖
hx : x ∈ g.ker
⊢ f x = 0
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:
by
    obtain ⟨C, h⟩ := h
    intro x hx
    specialize h x
    rw [hx] at h
    simpa using h

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

Goal state before:
pp: case h
𝕜 : 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‖
x : Eₗ
y : E
hxy : g y = x
⊢ ‖(g.ker.liftQ f ⋯ ∘ₛₗ ↑g.quotKerEquivRange.symm) ⟨x, ⋯⟩‖ ≤ C * ‖⟨x, ⋯⟩‖

Tactic:
simpa using

Goal state after:
case h
𝕜 : 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‖
x : Eₗ
y : E
hxy : g y = x
⊢ ‖f y‖ ≤ C * ‖g y‖
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✝ x : Eₗ
y : E
hxy : e y = x
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
simpa using

Goal state after:
𝕜 : 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✝ x : Eₗ
y : E
hxy : e y = x
⊢ ‖f y‖ ≤ C * ‖e y‖