awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : AEStronglyMeasurable f μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have pos : (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal
Tactic: simp [← toReal_eLpNorm, hf, hf.smul_measure, eLpNorm_smul_measure_of_ne_zero' hc f p μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
      simpa [hc] using h.smul_measure c⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
pos : ∀ (hf : AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : AEStronglyMeasurable f μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have pos : (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal
Tactic: simp [← toReal_eLpNorm, hf, hf.smul_measure, eLpNorm_smul_measure_of_ne_top' hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞), lpNorm f 0 (c • μ) = c ^ (ENNReal.toReal 0)⁻¹ • lpNorm f 0 μ
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
neg : ∀ (hp : Ne (α := ℝ≥0∞) 0 ∞), lpNorm f 0 (c • μ) = c ^ (ENNReal.toReal 0)⁻¹ • lpNorm f 0 μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg₁ : ∀ (hp₀ : p ≠ 0), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HPow.hPow (α := ℝ≥0) 0 p.toReal⁻¹ • lpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
neg : lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HPow.hPow (α := ℝ≥0) 0 p.toReal⁻¹ • lpNorm f p μ
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg₁ : ∀ (hc : c ≠ 0), lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
⊢ lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HPow.hPow (α := ℝ≥0) 0 p.toReal⁻¹ • lpNorm f p μ
have neg : lpNorm f p (HSMul.hSMul (α := ℝ≥0) 0 μ) = HSMul.hSMul (α := ℝ≥0) 0 (lpNorm f p μ)
Tactic: rw [NNReal.zero_rpow (by simp [ENNReal.toReal_eq_zero_iff, *])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : ¬AEStronglyMeasurable f μ
hp₀ : p ≠ 0
hc : c ≠ 0
⊢ lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • lpNorm f p μ
have neg : 0 = HSMul.hSMul (β := ℝ) (c ^ p.toReal⁻¹) 0
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf <| by
    simpa [hc] using h.smul_measure c⁻¹]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
have pos : ∀ (hf : AEStronglyMeasurable f μ),
  lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
pos :
  ∀ (hf : AEStronglyMeasurable f μ),
    lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
have neg : ∀ (hf : ¬AEStronglyMeasurable f μ),
  lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
Tactic: by_cases hf : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
have pos : lpNorm (E := ℝ) (fun (x : α) ↦ norm.{u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f x : K)) p μ =
  lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
Tactic: rw [← lpNorm_norm hf, ← lpNorm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : AEStronglyMeasurable f μ
pos :
  lpNorm (E := ℝ) (fun (x : α) ↦ norm.{u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f x : K)) p μ =
    lpNorm (E := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
have pos₁ : AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ
Tactic: rw [← lpNorm_norm hf, ← lpNorm_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
K : Type u_3
inst : RCLike K
f : α → K
p : ℝ≥0∞
μ : Measure α
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm.{u_1, u_3} (E := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) p μ = lpNorm f p μ
have rw : ∀ (h : AEStronglyMeasurable.{u_1, u_3} (β := K) ((starRingEnd (α → K) : (a : α → K) → α → K) f) μ),
  AEStronglyMeasurable f μ
Tactic: rw [lpNorm_of_not_aestronglyMeasurable hf, lpNorm_of_not_aestronglyMeasurable fun h ↦ hf ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)
have rw : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Tactic: rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.smul_def, smul_eq_mul,
    ENNReal.mul_rpow_of_nonneg _ _ hp.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
have simp_rw : ∫⁻ (a : α), (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞) ∂μ
Tactic: simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one, enorm,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top,
    ← ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞) ∂μ
have h₁ : ∀ᵐ (a : α) ∂μ, (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞)
Tactic: apply lintegral_mono_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
⊢ ∀ᵐ (a : α) ∂μ, (↑(‖f a‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g a‖₊ ^ p) : ℝ≥0∞)
have h₁ : ∀ (x : α) (hx : ‖f x‖₊ ≤ c * ‖g x‖₊), (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g x‖₊ ^ p) : ℝ≥0∞)
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
x : α
hx : ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑(c ^ p * ‖g x‖₊ ^ p) : ℝ≥0∞)
have h₁ : (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑((c * ‖g x‖₊) ^ p) : ℝ≥0∞)
Tactic: rw [← NNReal.mul_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ
hp : 0 < p
x : α
hx : ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ (↑(‖f x‖₊ ^ p) : ℝ≥0∞) ≤ (↑((c * ‖g x‖₊) ^ p) : ℝ≥0∞)
have h₁ : 0 ≤ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hp : 0 < p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c • (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)
have rw : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Tactic: rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.smul_def, smul_eq_mul,
    ENNReal.mul_rpow_of_nonneg _ _ hp.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hp : 0 < p
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ (↑c : ℝ≥0∞) ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
have simp_rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p ∂μ
Tactic: simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hp : 0 < p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p ∂μ
have h₁ : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p
Tactic: apply lintegral_mono_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hp : 0 < p
x : α
⊢ ¬p < 0
have linarith : p < 0 → 0 - p + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hp : 0 < p
x : α
⊢ (↑c : ℝ≥0∞) ^ p * ‖g x‖ₑ ^ p = ((↑c : ℝ≥0∞) * ‖g x‖ₑ) ^ p
have this : ¬p < 0
Tactic: have : ¬(p < 0) := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hp : 0 < p
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ (↑(c ^ p) : ℝ≥0∞) * ‖g a‖ₑ ^ p
have aux : ∀ (x : α), (↑c : ℝ≥0∞) ^ p * ‖g x‖ₑ ^ p = ((↑c : ℝ≥0∞) * ‖g x‖ₑ) ^ p
Tactic: have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    have : ¬(p < 0) := by linarith
    simp [ENNReal.mul_rpow_eq_ite, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
⊢ ¬p < 0
have linarith : p < 0 → 0 - p + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have hp' : ¬p < 0
Tactic: have hp' : ¬(p < 0) := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have pos : ∀ (hc : c = ∞), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Tactic: by_cases hc : c = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
pos : ∀ (hc : c = ∞), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have neg : ∀ (hc : ¬c = ∞), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Tactic: by_cases hc : c = ⊤
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have pos : ∀ (hg' : eLpNorm' g p μ = 0), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Tactic: by_cases hg' : eLpNorm' g p μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
pos : ∀ (hg' : eLpNorm' g p μ = 0), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have neg : ∀ (hg' : ¬eLpNorm' g p μ = 0), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
Tactic: by_cases hg' : eLpNorm' g p μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
have hg'₁ : ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0
Tactic: simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
have hg'₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ ^ p) 0
Tactic: rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
Tactic: have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have this₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
Tactic: have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (hypothesis)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ
have this : c ^ p ≠ ∞
Tactic: have : c ^ p ≠ ⊤ := by simp [hp.le, hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)
have neg : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
Tactic: rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.mul_rpow_of_nonneg _ _ hp.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
have neg : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), c ^ p * ‖g a‖ₑ ^ p ∂μ
Tactic: simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← lintegral_const_mul' _ _ this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity (goal)
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 : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), c ^ p * ‖g a‖ₑ ^ p ∂μ
have neg : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ c ^ p * ‖g a‖ₑ ^ p
Tactic: apply lintegral_mono_ae