mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ 1 * ‖y‖ ≤ N * ‖y‖

Tactic:
simpa using

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : R), ‖(lsmul 𝕜 R) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ ‖y‖ ≤ N * ‖y‖
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
a : R
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : E), ‖((lsmul 𝕜 R) a) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ ‖a‖ * ‖y‖ ≤ N * ‖y‖

Tactic:
simpa using

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
a : R
N : ℝ
x✝ : N ≥ 0
h : ∀ (x : E), ‖((lsmul 𝕜 R) a) x‖ ≤ N * ‖x‖
y : E
hy : y ≠ 0
⊢ ‖a‖ * ‖y‖ ≤ N * ‖y‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ ∃ M, 0 < M ∧ ∀ (x : E), ‖-f x‖ ≤ M * ‖x‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f : E → F
hf : IsBoundedLinearMap 𝕜 f
⊢ ∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap 𝕜 fun e ↦ f e - g e

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
⊢ IsBoundedLinearMap 𝕜 fun e ↦ f e + -g e
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
left✝ : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ C * ‖‖(x, y).1‖ * ‖(x, y).2‖‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
left✝ : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ C * (‖x‖ * ‖y‖)
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
this : Tendsto (fun y ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0))
⊢ Tendsto (fun x_1 ↦ f x_1 - f x) (𝓝 x) (𝓝 0)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
x : E × F
this : Tendsto (fun y ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0))
⊢ Tendsto (fun x_1 ↦ f x_1 - f x) (𝓝 x) (𝓝 0)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : M →L[R] M
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ (↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : M →L[R] M
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ (↑p).range = (↑q).range ∧ (↑p).ker = (↑q).ker
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = T ∘SL f

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).range ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = T ∘SL f
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f).ker ∈ Module.End.invtSubmodule ↑T ↔ f ∘SL T ∘SL f = f ∘SL T
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
H : IsEmbedding (g ∘ kerLift f ∘ ⇑Φ)
⊢ IsEmbedding (g ∘ kerLift f)

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
H : IsEmbedding (g ∘ kerLift f ∘ ⇑Φ)
⊢ IsEmbedding (g ∘ kerLift f)
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ↑(f a) ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ ¬f a = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
h'x : ¬f x = 0
⊢ ¬f x = 0
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsIdempotentElem 0
⊢ IsTopCompl ⊥ ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsIdempotentElem 0
⊢ IsTopCompl ⊥ ⊤
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsIdempotentElem (ContinuousLinearMap.id R M)
⊢ IsTopCompl ⊤ ⊥

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
this : IsIdempotentElem (ContinuousLinearMap.id R M)
⊢ IsTopCompl ⊤ ⊥
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsTopCompl p (↑f).ker

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ IsTopCompl p (↑f).ker
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ i ∈ s, (μ (t i)).toReal ≤ (μ univ).toReal

Tactic:
rw [← ENNReal.toReal_sum (by finiteness)]

Goal state after:
α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ (∑ a ∈ s, μ (t a)).toReal ≤ (μ univ).toReal
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x ↦ ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / p.toReal)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ‖c‖ₑ * ↑η ^ (1 / p.toReal) ≤ ε

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
this : Tendsto (fun x ↦ ↑(‖c‖₊ * x ^ (1 / p.toReal))) (𝓝 0) (𝓝 ↑0)
hε' : 0 < ε
δ : ℝ≥0
hδ : 0 < δ
hδε' : ∀ ⦃x : ℝ≥0⦄, x ∈ Set.Iio δ → ↑(‖c‖₊ * x ^ (1 / p.toReal)) ≤ ε
η : ℝ≥0
hη : 0 < η
hηδ : η < δ
⊢ ↑(‖c‖₊ * η ^ (1 / p.toReal)) ≤ ε
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ₑ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ eLpNorm (↑↑(indicatorConstLp p hs hμs c)) p μ ≤ ‖c‖ₑ * μ s ^ p.toReal⁻¹
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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
this : Inseparable (update m i 0) m
⊢ Inseparable (f m) 0

Tactic:
simpa using

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
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
this : Inseparable (update m i 0) m
⊢ Inseparable (f m) 0
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x ↦ ‖f x‖ ^ p) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case neg
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0✝ : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : 0 < ∏ i, ‖δ i‖
⊢ ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0
ε : ι → ℝ
C : ℝ
hε : ∀ (i : ι), 0 < ε i
c : ι → 𝕜
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖
m : (i : ι) → E i
hm : ∀ (i : ι), ‖m i‖ ≠ 0
δ : ι → 𝕜
hδ0✝ : ∀ (i : ι), δ i ≠ 0
hδm_lt : ∀ (i : ι), ‖δ i • m i‖ < ε i
hle_δm : ∀ (i : ι), ε i / ‖c i‖ ≤ ‖δ i • m i‖
a✝ : ∀ (i : ι), ‖δ i‖⁻¹ ≤ (ε i)⁻¹ * ‖c i‖ * ‖m i‖
hδ0 : 0 < ∏ i, ‖δ i‖
⊢ ‖f m‖ ≤ C * ∏ i, ‖m i‖
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
h : Integrable f (c • μ)
⊢ Integrable f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
h : Integrable f (c • μ)
⊢ Integrable f μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ ¬c = ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ c⁻¹ ≠ ∞

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ ¬c = 0
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Tactic:
simpa using

Goal state after:
case intro
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : s.Finite
f : α → E
⊢ IntegrableOn f s μ

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : s.Finite
f : α → E
⊢ IntegrableOn f s μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_8
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddCommMonoid ε'
inst✝ : ContinuousAdd ε'
ι : Type u_9
s : Finset ι
f : ι → α → ε'
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Integrable (fun a ↦ (∑ c ∈ s, f c) a) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f - g) μ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f + -g) μ
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
⊢ Function.Surjective ⇑(l.ker.liftQ l ⋯)

Tactic:
rw [← LinearMap.range_eq_top, Submodule.range_liftQ]

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
⊢ l.range = ⊤
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
x : α
hx : x ∈ u
⊢ ‖f x‖ₑ ≠ 0

Tactic:
simpa using

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
x : α
hx : x ∈ u
⊢ ¬f x = 0
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ ε⁻¹ ^ ENNReal.toReal 1 < ∞

Tactic:
simpa using

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ 0 < ε
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ eLpNorm f 1 μ ^ ENNReal.toReal 1 < ∞

Tactic:
simpa using

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousENorm E
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : 0 < ε
hε' : ε ≠ ∞
⊢ eLpNorm f 1 μ < ∞