awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
hc : c < 0
p : ℝ≥0∞
⊢ (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0

Tactic:
simp_rw [le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg (norm_nonneg _) hc (norm_nonneg _),
    norm_eq_zero, eventually_and] at h

Premises used: norm_eq_zero, Filter.eventually_and, _private.0.MeasureTheory.le_mul_iff_eq_zero_of_nonneg_of_neg_of_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : (∀ᵐ (x : α) ∂μ, f x = 0) ∧ ∀ᵐ (x : α) ∂μ, g x = 0
⊢ f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0

Tactic:
change f =ᵐ[μ] 0 ∧ g =ᵐ[μ] 0 at h
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
hc : c < 0
p : ℝ≥0∞
h : f =ᶠ[ae μ] 0 ∧ g =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

Tactic:
simp [eLpNorm_congr_ae h.1, eLpNorm_congr_ae h.2]

Premises used: And.right, And.left, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ ENNReal.ofReal c * eLpNorm g p μ

Tactic:
eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
    (h.mono fun _x hx => hx.trans <| mul_le_mul_of_nonneg_right c.le_coe_toNNReal (norm_nonneg _)) _

Premises used: ENNReal.ofReal, Filter.Eventually.mono, mul_le_mul_of_nonneg_right, LE.le.trans, norm_nonneg, MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul, Real.le_coe_toNNReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
⊢ eLpNorm f p μ ≤ (↑c : ℝ≥0∞) * eLpNorm g p μ

Tactic:
apply eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' h

Premises used: MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
pos : ∀ (h₀ : p = 0), eLpNorm f p μ ≤ c * eLpNorm g p μ
neg : ∀ (h₀ : ¬p = 0), eLpNorm f p μ ≤ c * eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
by_cases h₀ : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : p = 0
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
simp [h₀]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
neg :
  (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
⊢ eLpNorm f p μ ≤ c * eLpNorm g p μ

Tactic:
simp only [eLpNorm, h₀, ↓reduceIte, mul_ite]

Premises used: mul_ite, reduceIte, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
pos :
  ∀ (hp' : p = ∞),
    (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
      if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
neg :
  ∀ (hp' : ¬p = ∞),
    (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
      if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
by_cases hp' : p = ⊤
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
simpa [hp'] using eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h

Premises used: MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ≥0∞
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h₀ : ¬p = 0
hp' : ¬p = ∞
⊢ (if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = ∞ then c * eLpNormEssSup g μ else c * eLpNorm' g p.toReal μ

Tactic:
simpa [hp'] using eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul hg h (ENNReal.toReal_pos h₀ hp')

Premises used: MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul, ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α → E
g : α → F
c : ℝ≥0
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ eLpNorm g p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
⊢ eLpNorm g p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α → E
g : α → F
c : ℝ
hg : MemLp g p μ
hf : AEStronglyMeasurable f μ
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖
⊢ eLpNorm g p μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
rw : ∫⁻ (a : α), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤ eLpNorm f p μ

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, eLpNorm_eq_lintegral_rpow_enorm_toReal hp hp',
    one_div, ENNReal.le_rpow_inv_iff (ENNReal.toReal_pos hp hp'),
    ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg, ← ENNReal.rpow_mul,
    inv_mul_cancel₀ (ENNReal.toReal_pos hp hp').ne', ENNReal.rpow_one, ← setLIntegral_const,
    ← lintegral_indicator hs]

Premises used: ENNReal.rpow_mul, ENNReal.smul_def, ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_one, ENNReal.toReal_nonneg, ENNReal.le_rpow_inv_iff, ENNReal.toReal_pos, LT.lt.ne', MeasureTheory.lintegral_indicator, MeasureTheory.setLIntegral_const, one_div, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, smul_eq_mul, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
refine : ∀ᵐ (a : α) ∂μ, s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal
⊢ ∫⁻ (a : α), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
refine lintegral_mono_ae ?_

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
h : ∀ (x : α) (hx : x ∈ s → C ≤ ‖f x‖₊), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
⊢ ∀ᵐ (a : α) ∂μ, s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) a ≤ ‖f a‖ₑ ^ p.toReal

Tactic:
filter_upwards [hf] with x hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
pos : ∀ (hxs : x ∈ s), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
neg : ∀ (hxs : x ∉ s), s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∈ s
pos : ∀ (hx : C ≤ ‖f x‖₊), (↑C : ℝ≥0∞) ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
simp only [Set.indicator_of_mem, hxs, true_implies] at hx ⊢

Premises used: Set.indicator_of_mem, true_implies
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx : C ≤ ‖f x‖₊
pos : (↑C : ℝ≥0∞) ≤ ‖f x‖ₑ
⊢ (↑C : ℝ≥0∞) ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hxs : x ∈ s
hx pos pos₁ pos₂ pos₃ : C ≤ ‖f x‖₊
⊢ (↑C : ℝ≥0∞) ≤ ‖f x‖ₑ

Tactic:
rwa [coe_le_enorm]

Premises used: coe_le_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
hp : p ≠ 0
hp' : p ≠ ∞
f : α → F
C : ℝ≥0
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊
x : α
hx : x ∈ s → C ≤ ‖f x‖₊
hxs : x ∉ s
⊢ s.indicator (fun (x : α) ↦ (↑C : ℝ≥0∞) ^ p.toReal) x ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
simp [Set.indicator_of_notMem hxs]

Premises used: Set.indicator_of_notMem
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : NormedAddCommGroup R
inst_1 : StarAddMonoid R
inst_2 : NormedStarGroup R
p : ℝ≥0∞
f : α → R
⊢ ∀ (x : α), ‖star f x‖ = ‖f x‖

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : NormedAddCommGroup R
inst_1 : StarAddMonoid R
inst_2 : NormedStarGroup R
p : ℝ≥0∞
f : α →ₘ[μ] R
⊢ eLpNorm (star (↑f : α → R)) p μ = eLpNorm (↑f : α → R) p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : NormedAddCommGroup R
inst_1 : StarAddMonoid R
inst_2 : NormedStarGroup R
p : ℝ≥0∞
f : α → R
hf : MemLp f p μ
⊢ eLpNorm (star f) p μ < ∞

Tactic:
simpa using hf.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm.{u_1, u_5} (ε := 𝕜) ((starRingEnd (α → 𝕜) : (a : α → 𝕜) → α → 𝕜) f) p μ = eLpNorm f p μ

Tactic:
simp [← eLpNorm_norm]

Premises used: MeasureTheory.eLpNorm_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
rw : Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖
⊢ Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖

Tactic:
RCLike.norm_re_le_norm (f x)

Premises used: RCLike.norm_re_le_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖

Tactic:
exact RCLike.norm_re_le_norm (f x)

Premises used: RCLike.norm_re_le_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖

Tactic:
have : ∀ x, ‖RCLike.re (f x)‖ ≤ 1 * ‖f x‖ := by
    intro x
    rw [one_mul]
    exact RCLike.norm_re_le_norm (f x)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) p μ

Tactic:
hf.of_le_mul ?_ (Eventually.of_forall this)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
refine : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) p μ

Tactic:
refine hf.of_le_mul ?_ (Eventually.of_forall this)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.continuous_re.comp_aestronglyMeasurable hf.1

Premises used: Continuous.comp_aestronglyMeasurable, RCLike.continuous_re, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.re : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
exact RCLike.continuous_re.comp_aestronglyMeasurable hf.1

Premises used: Continuous.comp_aestronglyMeasurable, RCLike.continuous_re, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
rw : Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖
⊢ Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖

Tactic:
RCLike.norm_im_le_norm (f x)

Premises used: RCLike.norm_im_le_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ ‖f x‖

Tactic:
exact RCLike.norm_im_le_norm (f x)

Premises used: RCLike.norm_im_le_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖

Tactic:
have : ∀ x, ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖ := by
    intro x
    rw [one_mul]
    exact RCLike.norm_im_le_norm (f x)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) p μ

Tactic:
hf.of_le_mul ?_ (Eventually.of_forall this)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
refine : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) p μ

Tactic:
refine hf.of_le_mul ?_ (Eventually.of_forall this)

Premises used: MeasureTheory.MemLp.of_le_mul, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
RCLike.continuous_im.comp_aestronglyMeasurable hf.1

Premises used: Continuous.comp_aestronglyMeasurable, And.left, RCLike.continuous_im
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_5
inst : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), Norm.norm (E := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) (f x) : ℝ) ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (RCLike.im : (a : 𝕜) → ℝ) (f x)) μ

Tactic:
exact RCLike.continuous_im.comp_aestronglyMeasurable hf.1

Premises used: Continuous.comp_aestronglyMeasurable, And.left, RCLike.continuous_im
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
⊢ MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)

Tactic:
have hf' : MemLp f p (ν .univ • μ) := hf.smul_measure (by simp)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
change : MemLp (f ∘ Prod.fst) p (μ.prod ν)
⊢ MemLp (ε := ε) (fun (x : α × β) ↦ f x.1) p (μ.prod ν)

Tactic:
change MemLp (f ∘ Prod.fst) p (μ.prod ν)

Premises used: Function.comp, MeasureTheory.MemLp, Prod.fst, MeasureTheory.Measure.prod
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
⊢ AEMeasurable Prod.fst (μ.prod ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
rw : MemLp (m0 := mα) f p (Measure.map Prod.fst (μ.prod ν))
rw₁ : AEStronglyMeasurable (m₀ := mα) f (Measure.map Prod.fst (μ.prod ν))
⊢ MemLp (f ∘ Prod.fst) p (μ.prod ν)

Tactic:
rw [← memLp_map_measure_iff ?_ (by fun_prop)]

Premises used: MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod
Goal:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
μ : Measure α
p : ℝ≥0∞
f : α → ε
hf : MemLp f p μ
ν : Measure β
inst_2 : IsFiniteMeasure ν
hf' : MemLp f p (HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) μ)
⊢ MemLp (m0 := mα) f p (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa using hf'