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

Goal state before:
pp: X : Type u_1
ε'' : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
μ : Measure X
f : X → ε''
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (s.indicator f) μ

Tactic:
intro x

Goal state after:
X : Type u_1
ε'' : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace ε''
inst✝ : ESeminormedAddMonoid ε''
μ : Measure X
f : X → ε''
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (s.indicator f) (𝓝 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 ι
α : 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

Goal state after:
𝕜 : 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), ‖((f.iteratedFDerivComponent e) x) m₂‖ ≤ (‖f‖ * ∏ i, ‖x i‖) * ∏ i, ‖m₂ i‖
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
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
⊢ ∀ x ∉ K, g x • f x = 0

Tactic:
intro x

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
⊢ x ∉ K → g x • f x = 0
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
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := ⋯
hK : IsCompact K
⊢ ∀ x ∉ K, f x • g x = 0

Tactic:
intro x

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
⊢ x ∉ K → f x • g x = 0
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
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
⊢ LocallyIntegrable f μ

Tactic:
intro x

Goal state after:
X : Type u_1
E : Type u_6
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
f : X → E
inst✝ : IsLocallyFiniteMeasure μ
hmono : Monotone f
x : X
⊢ IntegrableAtFilter f (𝓝 x) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
R : Type u_8
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
μ : Measure X
inst✝² : OpensMeasurableSpace X
A K : Set X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
g g' : X → R
hg : IntegrableOn g A μ
hg' : ContinuousOn g' K
hA : MeasurableSet A
hK : IsCompact K
hAK : A ⊆ K
C : ℝ
hC : ∀ x ∈ K, ‖g' x‖ ≤ C
⊢ IntegrableOn (fun x ↦ g x * g' x) A μ

Tactic:
exact hg.mul_bdd ((hg'.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

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
inst✝⁴ : OpensMeasurableSpace X
A K : Set X
𝕜 : Type u_9
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : SecondCountableTopologyEither X 𝕜
f : X → 𝕜
hf : ContinuousOn f K
g : X → E
hg : IntegrableOn g A μ
hK : IsCompact K
hA : MeasurableSet A
hAK : A ⊆ K
⊢ IntegrableOn (fun x ↦ f x • g x) A μ

Tactic:
by
  rcases IsCompact.exists_bound_of_continuousOn hK hf with ⟨C, hC⟩
  exact hg.bdd_smul C ((hf.mono hAK).aestronglyMeasurable hA)
    (ae_restrict_of_forall_mem hA fun x hx => hC x (hAK hx))

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
⊢ ∀ (a₁ a₂ : E), ⋯.extend (⇑f) (e a₁ + e a₂) = ⋯.extend (⇑f) (e a₁) + ⋯.extend (⇑f) (e a₂)

Tactic:
intro x

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
x : E
⊢ ∀ (a₂ : E), ⋯.extend (⇑f) (e x + e a₂) = ⋯.extend (⇑f) (e x) + ⋯.extend (⇑f) (e a₂)
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
⊢ ∀ (a : E), ⋯.extend (⇑f) (k • e a) = σ₁₂ k • ⋯.extend (⇑f) (e a)

Tactic:
intro x

Goal state after:
case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
k : 𝕜
b : Eₗ
x : E
⊢ ⋯.extend (⇑f) (k • e x) = σ₁₂ k • ⋯.extend (⇑f) (e 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✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
⊢ f.extend e = g

Tactic:
simp only [extend, h_dense, h_e, and_self, ↓reduceDIte]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h_dense : DenseRange ⇑e
h_e : IsUniformInducing ⇑e
g : Eₗ →SL[σ₁₂] F
H : g ∘SL e = f
⊢ { toFun := ⋯.extend ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } = g
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 : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖
⊢ g.ker ≤ f.ker

Tactic:
intro x

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‖
x : E
⊢ x ∈ g.ker → x ∈ 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
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ₗ
⊢ ∀ x ∈ e.range, ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
intro x

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ₗ
⊢ x ∈ e.range → ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map norm (-f).posPart = (-f).posPart

Tactic:
exact posPart_map_norm _

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

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (s.piecewise (⇑f) 0 ⁻¹' {y}) • y = (μ.restrict s).real (⇑f ⁻¹' {y}) • y

Tactic:
rw [Set.piecewise_eq_indicator, indicator_preimage_of_notMem,
      measureReal_restrict_apply (f.measurableSet_preimage _)]

Goal state after:
case refine_2.ht
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ 0 ∉ {y}
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : 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 : α), μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x

Tactic:
intro x

Goal state after:
α : 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 : α
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x
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) μ
⊢ ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})

Tactic:
intro x

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 α
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) μ
x : E
⊢ x ∈ {x ∈ f.range | x ≠ 0} → T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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

Tactic:
intro x

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
x : E
⊢ x ∈ {x ∈ f.range | x ≠ 0} → T' (⇑f ⁻¹' {x}) = c • T (⇑f ⁻¹' {x})
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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
⊢ ∀ (y : E), y ≠ 0 → μ (⇑(-g) ⁻¹' {y}) < ∞

Tactic:
intro x

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 α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
⊢ x ≠ 0 → μ (⇑(-g) ⁻¹' {x}) < ∞
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α →ₛ G'
hfi : Integrable (⇑f) μ
hgi : Integrable (⇑g) μ
hfg : f ≤ g
⊢ 0 ≤ g - f

Tactic:
intro x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α →ₛ G'
hfi : Integrable (⇑f) μ
hgi : Integrable (⇑g) μ
hfg : f ≤ g
x : α
⊢ 0 x ≤ (g - f) x
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.const
α : 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
⊢ ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (δ : ℝ≥0∞),
    δ ≠ 0 →
      MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ →
        ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ δ ∧ P g

Tactic:
intro c s hs ε εpos Hs

Goal state after:
case inr.const
α : 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
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
Q : Type u_5
inst✝¹⁴ : Ring S
inst✝¹³ : Ring R
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module R V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module R W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : Module S W
inst✝⁴ : SMulCommClass R S W
inst✝³ : ContinuousConstSMul S W
inst✝² : AddTorsor W Q
inst✝¹ : TopologicalSpace Q
inst✝ : IsTopologicalAddTorsor Q
f : V →ᴬ[R] Q
⊢ (fun p ↦ p.2.toContinuousAffineMap +ᵥ const R V p.1) ((fun f ↦ (f 0, f.contLinear)) f) = f

Tactic:
by
    ext x
    simp_rw [vadd_apply, f.contLinear.coe_toContinuousAffineMap, coe_const, Function.const_apply,
      ← f.map_vadd, vadd_eq_add, add_zero]

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

Goal state before:
pp: α : 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‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞

Tactic:
intro x

Goal state after:
α : 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
⊢ x ∈ (toSimpleFunc f).range → ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x}) ≠ ∞
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Sub R
inst✝ : BoundedSub R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C
⊢ ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C

Tactic:
intro x

Goal state after:
case h
R : Type u_1
X : Type u_2
inst✝² : PseudoMetricSpace R
inst✝¹ : Sub R
inst✝ : BoundedSub R
f g : X → R
f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C
x : X
⊢ ∀ (y : X), dist ((f - g) x) ((f - g) y) ≤ C
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x ↦ x ^ n) '' s)
⊢ (fun x ↦ x ^ (n + 1)) '' s ⊆ (fun x ↦ x ^ n) '' s * s

Tactic:
intro x

Goal state after:
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded ((fun x ↦ x ^ n) '' s)
x : R
⊢ x ∈ (fun x ↦ x ^ (n + 1)) '' s → x ∈ (fun x ↦ x ^ n) '' s * s