awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
neg : ∀ (p_zero : ¬p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞

Tactic:
by_cases p_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : p = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞

Tactic:
simp [p_zero]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
neg : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) ∞ μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞

Tactic:
rw [ENNReal.div_zero p_zero]

Premises used: ENNReal.div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ ENorm.enorm (E := ℝ≥0∞) 1 ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) ∞ μ < ∞

Tactic:
simpa only [ENNReal.rpow_zero, eLpNorm_exponent_top] using (memLp_top_const_enorm (by simp)).2

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.memLp_top_const_enorm, And.right, ENNReal.rpow_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞

Tactic:
rw [eLpNorm_enorm_rpow _ (ENNReal.toReal_pos q_zero q_top)]

Premises used: ENNReal.toReal_pos, MeasureTheory.eLpNorm_enorm_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ENNReal.rpow_lt_top_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f p μ ≠ ∞
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞

Tactic:
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]

Premises used: mul_assoc, ENNReal.ofReal_toReal, div_eq_mul_inv, ENNReal.inv_mul_cancel, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞

Tactic:
hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞

Tactic:
exact hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ

Tactic:
⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.MemLp, MeasureTheory.AEStronglyMeasurable.norm, ENNReal.toReal, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
refine : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ

Tactic:
refine ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
neg : ∀ (q_top : ¬q = ∞), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
by_cases q_top : q = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : q = ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
simp [q_top]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
neg : ∀ (q_zero : ¬q = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
by_cases q_zero : q = 0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
simp only [q_zero, ENNReal.toReal_zero, Real.rpow_zero]

Premises used: Real.rpow_zero, ENNReal.toReal_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
neg : ∀ (p_zero : ¬p = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞

Tactic:
by_cases p_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : p = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞

Tactic:
simp [p_zero]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
neg : eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) ∞ μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞

Tactic:
rw [ENNReal.div_zero p_zero]

Premises used: ENNReal.div_zero
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) ∞ μ < ∞

Tactic:
(memLp_top_const (1 : ℝ)).2

Premises used: And.right, OfNat.ofNat, MeasureTheory.memLp_top_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) ∞ μ < ∞

Tactic:
exact (memLp_top_const (1 : ℝ)).2

Premises used: And.right, OfNat.ofNat, MeasureTheory.memLp_top_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞

Tactic:
rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]

Premises used: ENNReal.toReal_pos, MeasureTheory.eLpNorm_norm_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ENNReal.rpow_lt_top_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
neg : eLpNorm f p μ ≠ ∞
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞

Tactic:
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]

Premises used: mul_assoc, ENNReal.ofReal_toReal, div_eq_mul_inv, ENNReal.inv_mul_cancel, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞

Tactic:
hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f p μ ≠ ∞

Tactic:
exact hf.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
⟨fun h => ?_, fun h => h.enorm_rpow_div q⟩

Premises used: Iff.intro, MeasureTheory.MemLp.enorm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
refine : ∀ (h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ), MemLp f p μ
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
refine ⟨fun h => ?_, fun h => h.enorm_rpow_div q⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
apply : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
⊢ MemLp f p μ

Tactic:
apply (memLp_enorm_iff hf).1

Premises used: MeasureTheory.memLp_enorm_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal) (p / q / q⁻¹) μ

Tactic:
h.enorm_rpow_div q⁻¹

Premises used: Inv.inv, MeasureTheory.MemLp.enorm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
h₂ : p = p / q / q⁻¹
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ

Tactic:
convert! h.enorm_rpow_div q⁻¹ using 1

Premises used: Inv.inv, MeasureTheory.MemLp.enorm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : ∀ (x : α), ‖f x‖ₑ = ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
x : α
⊢ q.toReal * q.toReal⁻¹ = 1

Tactic:
have : q.toReal * q.toReal⁻¹ = 1 :=
      CommGroupWithZero.mul_inv_cancel q.toReal <| ENNReal.toReal_ne_zero.mpr ⟨q_zero, q_top⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
x : α
this : q.toReal * q.toReal⁻¹ = 1
⊢ ‖f x‖ₑ = ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal

Tactic:
simp [← ENNReal.rpow_mul, this, ENNReal.rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
h₅ : p = p * 1
h₆ h₇ : p = p
⊢ p = p / q / q⁻¹

Tactic:
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

Premises used: mul_assoc, div_eq_mul_inv, inv_inv, ENNReal.inv_mul_cancel, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
⟨fun h => ?_, fun h => h.norm_rpow_div q⟩

Premises used: MeasureTheory.MemLp.norm_rpow_div, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
refine : ∀ (h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ), MemLp f p μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ

Tactic:
refine ⟨fun h => ?_, fun h => h.norm_rpow_div q⟩
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
apply : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
⊢ MemLp f p μ

Tactic:
apply (memLp_norm_iff hf).1

Premises used: Iff.mp, MeasureTheory.memLp_norm_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal) (p / q / q⁻¹) μ

Tactic:
h.norm_rpow_div q⁻¹

Premises used: MeasureTheory.MemLp.norm_rpow_div, Inv.inv
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : Eq.{u_1 + 1} (α := α → ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
h₂ : p = p / q / q⁻¹
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ

Tactic:
convert! h.norm_rpow_div q⁻¹ using 1

Premises used: MeasureTheory.MemLp.norm_rpow_div, Inv.inv
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : ∀ (x : α), ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
⊢ Eq.{u_1 + 1} (α := α → ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
h₁ : q.toReal ≠ 0
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal

Tactic:
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _),
      ENNReal.toReal_inv, mul_inv_cancel₀, abs_of_nonneg (norm_nonneg _), Real.rpow_one]

Premises used: mul_inv_cancel₀, ENNReal.toReal_inv, Real.abs_rpow_of_nonneg, Real.rpow_one, abs_of_nonneg, Real.rpow_mul, abs_nonneg, norm_nonneg, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ q.toReal ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, q_zero, q_top]

Premises used: ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
h₅ : p = p * 1
h₆ h₇ : p = p
⊢ p = p / q / q⁻¹

Tactic:
rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

Premises used: mul_assoc, div_eq_mul_inv, inv_inv, ENNReal.inv_mul_cancel, mul_one
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ

Tactic:
hf.enorm_rpow_div p

Premises used: MeasureTheory.MemLp.enorm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p / p
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ

Tactic:
convert! hf.enorm_rpow_div p

Premises used: MeasureTheory.MemLp.enorm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p * p⁻¹
h₁ h₂ : Eq (α := ℝ≥0∞) 1 1
⊢ 1 = p / p

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

Premises used: div_eq_mul_inv, ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ

Tactic:
hf.norm_rpow_div p

Premises used: MeasureTheory.MemLp.norm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p / p
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ

Tactic:
convert! hf.norm_rpow_div p

Premises used: MeasureTheory.MemLp.norm_rpow_div
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
h : 1 = p * p⁻¹
h₁ h₂ : Eq (α := ℝ≥0∞) 1 1
⊢ 1 = p / p

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel hp_ne_zero hp_ne_top]

Premises used: div_eq_mul_inv, ENNReal.mul_inv_cancel
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : Membership.mem (γ := AddSubgroup (β →ₘ[μb] E)) (Lp E p μb) g
f : α → β
hf : MeasurePreserving f μ μb
rw :
  ∀ (hg : eLpNorm (↑g : β → E) p μb < ∞) {f : α → β} (hf : MeasurePreserving f μ μb),
    eLpNorm (↑(g.compMeasurePreserving f hf) : α → E) p μ < ∞
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (g.compMeasurePreserving f hf)

Tactic:
rw [Lp.mem_Lp_iff_eLpNorm_lt_top] at hg ⊢

Premises used: MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Basic
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_7
inst_1 : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : eLpNorm (↑g : β → E) p μb < ∞
f : α → β
hf : MeasurePreserving f μ μb
rwa rwa₁ rwa₂ rwa₃ : eLpNorm (↑g : β → E) p μb < ∞
⊢ eLpNorm (↑(g.compMeasurePreserving f hf) : α → E) p μ < ∞

Tactic:
rwa [eLpNorm_compMeasurePreserving]

Premises used: MeasureTheory.AEEqFun.eLpNorm_compMeasurePreserving