awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
hpq : p ≤ q
hf : AEStronglyMeasurable f μ
hp0 : p ≠ 0
hq0_lt : 0 < q
hq_top : q ≠ ∞
hp_lt_top : p < ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm' f p.toReal μ ≤
    eLpNorm' f q.toReal μ *
      HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal - 1 / q.toReal)
have hpq_real : p.toReal ≤ q.toReal
Tactic: have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ
have h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
Tactic: have h_le_μ := eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp0_lt hpq hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ :
  eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ
have rwa : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) 1 (1 / p - 1 / q)), eLpNorm' f p μ ≤ eLpNorm' f q μ
Tactic: rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ
Cleared hypotheses: h_le_μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ :
  eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
rwa :
  ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) 1 (1 / p - 1 / q)),
    eLpNorm' f p μ ≤ eLpNorm' f q μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ
have rwa₁ : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * 1), eLpNorm' f p μ ≤ eLpNorm' f q μ
Tactic: rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ
Cleared hypotheses: h_le_μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
hp0_lt : 0 < p
hpq : p ≤ q
μ : Measure α
inst_2 : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
h_le_μ :
  eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q)
rwa :
  ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) 1 (1 / p - 1 / q)),
    eLpNorm' f p μ ≤ eLpNorm' f q μ
rwa₁ : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ * 1), eLpNorm' f p μ ≤ eLpNorm' f q μ
⊢ eLpNorm' f p μ ≤ eLpNorm' f q μ
have rwa₂ : ∀ (h_le_μ : eLpNorm' f p μ ≤ eLpNorm' f q μ), eLpNorm' f p μ ≤ eLpNorm' f q μ
Tactic: rwa [measure_univ, ENNReal.one_rpow, mul_one] at h_le_μ
Cleared hypotheses: h_le_μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
⊢ eLpNorm' f p μ < ∞
have inl : ∀ (hp_nonpos : p ≤ 0), eLpNorm' f p μ < ∞
Tactic: rcases le_or_gt p 0 with hp_nonpos | hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
inl : ∀ (hp_nonpos : p ≤ 0), eLpNorm' f p μ < ∞
⊢ eLpNorm' f p μ < ∞
have inr : ∀ (hp_pos : 0 < p), eLpNorm' f p μ < ∞
Tactic: rcases le_or_gt p 0 with hp_nonpos | hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_nonpos : p ≤ 0
⊢ eLpNorm' f p μ < ∞
have inl : eLpNorm' f 0 μ < ∞
Tactic: rw [le_antisymm hp_nonpos hp_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
⊢ eLpNorm' f p μ < ∞
have hq_pos : 0 < q
Tactic: have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞
have rw : eLpNorm' f q μ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞ ∨
  eLpNorm' f q μ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) = 0
Tactic: rw [ENNReal.mul_lt_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f q μ < ∞ ∧ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞ ∨
    eLpNorm' f q μ = 0 ∨ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) = 0
have refine : 0 ≤ 1 / p - 1 / q
Tactic: refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (by finiteness)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ 0 ≤ 1 / p - 1 / q
have rwa : 1 / q ≤ 1 / p - 0
Tactic: rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
rwa : 1 / q ≤ 1 / p - 0
⊢ 0 ≤ 1 / p - 1 / q
have rwa₁ : 1 / q ≤ 1 / p
Tactic: rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
rwa : 1 / q ≤ 1 / p - 0
rwa₁ : 1 / q ≤ 1 / p
⊢ 0 ≤ 1 / p - 1 / q
have rwa₂ : q⁻¹ ≤ 1 / p
Tactic: rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
rwa : 1 / q ≤ 1 / p - 0
rwa₁ : 1 / q ≤ 1 / p
rwa₂ : q⁻¹ ≤ 1 / p
⊢ 0 ≤ 1 / p - 1 / q
have rwa₃ : q⁻¹ ≤ p⁻¹
Tactic: rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ
inst_2 : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q μ < ∞
hp_nonneg : 0 ≤ p
hpq : p ≤ q
hp_pos : 0 < p
hq_pos : 0 < q
⊢ eLpNorm' f p μ < ∞
have eLpNorm' : eLpNorm' f q μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p - 1 / q) < ∞
Tactic: calc
    eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
      eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq hf
    _ < ∞ := by
      rw [ENNReal.mul_lt_top_iff]
      refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (by finiteness)⟩
      rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
⊢ MemLp f p μ
have hfq_m : AEStronglyMeasurable f μ
Tactic: obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
Cleared hypotheses: hfq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq : MemLp f q μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
⊢ MemLp f p μ
have hfq_lt_top : eLpNorm f q μ < ∞
Tactic: obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
Cleared hypotheses: hfq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
⊢ MemLp f p μ
have pos : ∀ (hp0 : p = 0), MemLp f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
pos : ∀ (hp0 : p = 0), MemLp f p μ
⊢ MemLp f p μ
have neg : ∀ (hp0 : ¬p = 0), MemLp f p μ
Tactic: by_cases hp0 : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p = 0
⊢ MemLp f p μ
have pos : MemLp f 0 μ
Tactic: rwa [hp0, memLp_zero_iff_aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : ¬p = 0
⊢ MemLp f p μ
have hp0₁ : p ≠ 0
Tactic: rw [← Ne] at hp0
Cleared hypotheses: hp0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
⊢ MemLp f p μ
have neg : eLpNorm f p μ < ∞
Tactic: refine ⟨hfq_m, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
⊢ eLpNorm f p μ < ∞
have pos : ∀ (hp_top : p = ∞), eLpNorm f p μ < ∞
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞
have neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p μ < ∞
Tactic: by_cases hp_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ q = ∞
have rwa : ∀ (hpq : ∞ ≤ q) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞),
  q = ∞
Tactic: rwa [hp_top, top_le_iff] at hpq
Cleared hypotheses: hpq, hfq_m, hfq_lt_top, hp0, hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
rwa :
  ∀ (hpq : ∞ ≤ q) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞),
    q = ∞
⊢ q = ∞
have rwa₁ : ∀ (hpq : q = ∞) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞),
  q = ∞
Tactic: rwa [hp_top, top_le_iff] at hpq
Cleared hypotheses: hpq, hfq_m, hfq_lt_top, hp0, hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
⊢ eLpNorm f p μ < ∞
have hq_top : q = ∞
Tactic: have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f p μ < ∞
have pos : eLpNorm f ∞ μ < ∞
Tactic: rw [hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : p = ∞
hq_top : q = ∞
⊢ eLpNorm f ∞ μ < ∞
have pos : ∀ (hfq_lt_top : eLpNorm f ∞ μ < ∞) (hp0 : p ≠ 0) (hp_top : p = ∞) (hq_top : q = ∞), eLpNorm f ∞ μ < ∞
Tactic: rwa [hq_top] at hfq_lt_top
Cleared hypotheses: hfq_lt_top, hp0, hp_top, hq_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm f p μ < ∞
have hp_pos : 0 < p.toReal
Tactic: have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
⊢ eLpNorm f p μ < ∞
have pos : ∀ (hq_top : q = ∞), eLpNorm f p μ < ∞
Tactic: by_cases hq_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
pos : ∀ (hq_top : q = ∞), eLpNorm f p μ < ∞
⊢ eLpNorm f p μ < ∞
have neg : ∀ (hq_top : ¬q = ∞), eLpNorm f p μ < ∞
Tactic: by_cases hq_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm f p μ < ∞
have pos : eLpNorm' f p.toReal μ < ∞
Tactic: rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm' f p.toReal μ < ∞
have hfq_lt_top₁ : eLpNormEssSup f μ < ∞
Tactic: rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top
Cleared hypotheses: hfq_lt_top, hp0, hp_top, hp_pos, hq_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNorm' f p.toReal μ < ∞
have pos : eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
Tactic: refine lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
have pos : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
Tactic: refine ENNReal.mul_lt_top hfq_lt_top ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (goal)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
⊢ p ≤ 0
have rwa : ∀ (hpq : p ≤ 0) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : ¬p = ∞)
  (hp_pos : 0 < p.toReal) (hq_top : ¬q = ∞) (hq_eq_zero : q = 0), p ≤ 0
Tactic: rwa [hq_eq_zero] at hpq
Cleared hypotheses: hpq, hfq_m, hfq_lt_top, hp0, hp_top, hp_pos, hq_top, hq_eq_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
⊢ False
have hpq₁ : 0 ≤ q
Tactic: obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
Cleared hypotheses: p, hpq, hp0, hp_top, hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
⊢ False
have hp0₁ : Ne (α := ℝ≥0∞) 0 0
Tactic: obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
Cleared hypotheses: p, hpq, hp0, hp_top, hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
hp0₁ : Ne (α := ℝ≥0∞) 0 0
⊢ False
have hp_top₁ : ¬Eq (α := ℝ≥0∞) 0 ∞
Tactic: obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
Cleared hypotheses: p, hpq, hp0, hp_top, hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
hp0₁ : Ne (α := ℝ≥0∞) 0 0
hp_top₁ : ¬Eq (α := ℝ≥0∞) 0 ∞
⊢ False
have hp_pos₁ : 0 < ENNReal.toReal 0
Tactic: obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
Cleared hypotheses: p, hpq, hp0, hp_top, hp_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp (hypothesis)
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : Ne (α := ℝ≥0∞) 0 0
hp_top : ¬Eq (α := ℝ≥0∞) 0 ∞
hp_pos : 0 < ENNReal.toReal 0
⊢ False
have hp_pos₁ : LT.lt (α := ℝ) 0 0
Tactic: rw [ENNReal.toReal_zero] at hp_pos
Cleared hypotheses: hp_pos