awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MemLp (f i) (p i) μ),
    MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ
cons :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih : ∀ (hf : ∀ i ∈ s, MemLp (f i) (p i) μ), MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ)
    (hf : ∀ i_1 ∈ Finset.cons i s hi, MemLp (f i_1) (p i_1) μ),
    MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ Finset.cons i s hi, f i) (∑ i ∈ Finset.cons i s hi, (p i)⁻¹)⁻¹ μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
induction s using cons_induction with
  | empty =>
    by_cases hμ : μ = 0 <;>
      simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]
  | cons i s hi ih =>
    rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Premises used: MeasureTheory.aestronglyMeasurable_const, Finset.cons, MeasureTheory.eLpNormEssSup_const, MeasureTheory.MemLp, Pi.one_def, Finset.prod_cons
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x : MeasurableSpace α
inst : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ s, MemLp (f i) (p i) μ
⊢ MemLp.{u_2, u_3} (ε := 𝕜) (fun (ω : α) ↦ ∏ i ∈ s, f i ω) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ

Tactic:
simpa [Finset.prod_fn] using MemLp.prod hf

Premises used: MeasureTheory.MemLp.prod, Finset.prod_fn
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
simp_rw : (if p = ∞ then eLpNormEssSup (m0 := inst) f (dirac i) else @eLpNorm' _ _ _ inst f p.toReal (dirac i)) = ‖f i‖ₑ
⊢ @eLpNorm _ _ _ inst f p (dirac i) = ‖f i‖ₑ

Tactic:
simp_rw [eLpNorm, if_neg hp]

Premises used: if_neg, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
pos : p = ∞ → eLpNormEssSup (m0 := inst) f (dirac i) = ‖f i‖ₑ
neg : ¬p = ∞ → @eLpNorm' _ _ _ inst f p.toReal (dirac i) = ‖f i‖ₑ
⊢ (if p = ∞ then eLpNormEssSup (m0 := inst) f (dirac i) else @eLpNorm' _ _ _ inst f p.toReal (dirac i)) = ‖f i‖ₑ

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
h : p = ∞
⊢ eLpNormEssSup (m0 := inst) f (dirac i) = ‖f i‖ₑ

Tactic:
simp [eLpNormEssSup, essSup, limsup, limsSup, Set.Ici_def]

Premises used: Filter.limsSup, Filter.limsup, Set.Ici_def, MeasureTheory.eLpNormEssSup, essSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
h : ¬p = ∞
⊢ @eLpNorm' _ _ _ inst f p.toReal (dirac i) = ‖f i‖ₑ

Tactic:
simp [eLpNorm', ENNReal.toReal_eq_zero_iff, *]

Premises used: MeasureTheory.eLpNorm', ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
rw rw₁ : ‖f i‖ₑ = ‖f i‖ₑ
⊢ ‖f i‖ₑ = @eLpNorm _ _ _ inst f p (dirac i)

Tactic:
rw [eLpNorm_dirac f i hp]

Premises used: MeasureTheory.eLpNorm_dirac
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ @eLpNorm _ _ _ inst f p (dirac i) = @eLpNorm _ _ _ inst f p (Measure.restrict count {i})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
⊢ @eLpNorm _ _ _ inst f p (Measure.restrict count {i}) ≤ @eLpNorm _ _ _ inst f p count

Tactic:
eLpNorm_restrict_le ..

Premises used: MeasureTheory.eLpNorm_restrict_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
p : ℝ≥0∞
f : α → ε
i : α
hp : p ≠ 0
eLpNorm : ‖f i‖ₑ = @MeasureTheory.eLpNorm _ _ _ inst f p (dirac i)
eLpNorm₁ :
  @MeasureTheory.eLpNorm _ _ _ inst f p (dirac i) = @MeasureTheory.eLpNorm _ _ _ inst f p (Measure.restrict count {i})
⊢ ‖f i‖ₑ ≤ @MeasureTheory.eLpNorm _ _ _ inst f p count

Tactic:
calc
    ‖f i‖ₑ = eLpNorm f p (dirac i) := by rw [eLpNorm_dirac f i hp]
      _ = eLpNorm f p (count.restrict {i}) := by simp
      _ ≤ eLpNorm f p count := eLpNorm_restrict_le ..

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.dirac, MeasureTheory.Measure.count, Singleton.singleton, MeasureTheory.eLpNorm_restrict_le, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
haveI : ∀ (this : Fintype α), @eLpNorm _ _ _ inst f p count < ∞
⊢ @eLpNorm _ _ _ inst f p count < ∞

Tactic:
haveI := Fintype.ofFinite α
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ @eLpNorm _ _ _ inst f p count < ∞

Tactic:
(eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_

Premises used: MeasureTheory.eLpNorm_mono_enorm, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
refine_1 :
  ∀ (x : α), ‖f x‖ₑ ≤ enorm (E := ℝ≥0∞) ((fun (x : α) ↦ (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ : ℝ≥0∞)) x)
refine_2 : @eLpNorm _ ℝ≥0∞ _ inst (fun (x : α) ↦ Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ) p count < ∞
⊢ @eLpNorm _ _ _ inst f p count < ∞

Tactic:
refine (eLpNorm_mono_enorm (g := fun _ ↦ Finset.univ.sup (‖f ·‖ₑ)) ?_).trans_lt ?_

Premises used: MeasureTheory.eLpNorm_mono_enorm, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ ∀ (x : α), ‖f x‖ₑ ≤ enorm (E := ℝ≥0∞) ((fun (x : α) ↦ (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ : ℝ≥0∞)) x)

Tactic:
fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ ∀ (x : α), ‖f x‖ₑ ≤ enorm (E := ℝ≥0∞) ((fun (x : α) ↦ (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ : ℝ≥0∞)) x)

Tactic:
exact fun x ↦ Finset.le_sup (f := (‖f ·‖ₑ)) (Finset.mem_univ x)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ enorm (E := ℝ≥0∞) (Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ) ≠ ∞

Tactic:
simp [h, LT.lt.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_3 : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ @eLpNorm _ ℝ≥0∞ _ inst (fun (x : α) ↦ Finset.sup Finset.univ fun (x : α) ↦ ‖f x‖ₑ) p count < ∞

Tactic:
exact (memLp_const_enorm <| by simp [h, LT.lt.ne]).eLpNorm_lt_top

Premises used: MeasureTheory.memLp_const_enorm, MeasureTheory.MemLp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count
Goal:
α : Type u_1
ε : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
inst_2 : TopologicalSpace ε
inst_3 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst_4 : Finite α
hp : p ≠ 0
⊢ @eLpNorm _ _ _ inst f p count < ∞ ↔ ∀ (i : α), ‖f i‖ₑ < ∞

Tactic:
⟨fun h i ↦ (enorm_le_eLpNorm_count f i hp).trans_lt h, eLpNorm_count_lt_top_of_lt⟩

Premises used: MeasureTheory.eLpNorm_count_lt_top_of_lt, Iff.intro, MeasureTheory.enorm_le_eLpNorm_count, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
f : α → ε
q : ℝ
μ : Measure α
⊢ eLpNorm' f q μ = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
rfl

Premises used: MeasureTheory.eLpNorm', rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
f : α → ε
μ : Measure α
⊢ eLpNormEssSup f μ = essSup (fun (x : α) ↦ ‖f x‖ₑ) μ

Tactic:
rfl

Premises used: MeasureTheory.eLpNormEssSup, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
⊢ eLpNorm f p μ = eLpNorm' f p.toReal μ

Tactic:
simp [eLpNorm, hp_ne_zero, hp_ne_top]

Premises used: MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ (↑p : ℝ≥0∞) ≠ 0

Tactic:
exact_mod_cast hp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
inst : ENorm ε
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
rw : eLpNorm' f p.toReal μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
rw₁ rw₂ : (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ eLpNorm f (↑p : ℝ≥0∞) μ = (∫⁻ (x : α), ‖f x‖ₑ ^ (↑p : ℝ) ∂μ) ^ (1 / (↑p : ℝ))

Tactic:
eLpNorm_nnreal_eq_eLpNorm' hp

Premises used: MeasureTheory.eLpNorm', MeasureTheory.eLpNorm_nnreal_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
simp_rw : (∫⁻ (x : α), ‖f x‖ₑ ^ ENNReal.toReal 1 ∂μ) ^ (1 / ENNReal.toReal 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
simp_rw₁ : (∫⁻ (x : α), HPow.hPow (β := ℝ) ‖f x‖ₑ 1 ∂μ) ^ (1 / 1) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
simp_rw₂ : HPow.hPow (β := ℝ) (∫⁻ (x : α), HPow.hPow (β := ℝ) ‖f x‖ₑ 1 ∂μ) 1 = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
⊢ eLpNorm f 1 μ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal one_ne_zero ENNReal.coe_ne_top,
    ENNReal.toReal_one, one_div_one, ENNReal.rpow_one]

Premises used: ENNReal.toReal_one, ENNReal.rpow_one, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, one_ne_zero, one_div_one, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
⊢ eLpNorm f ∞ μ = eLpNormEssSup f μ

Tactic:
simp [eLpNorm]

Premises used: MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
inst_1 : TopologicalSpace ε
f : α → ε
p : ℝ≥0∞
h : MemLp f p μ
⊢ AEStronglyMeasurable f μ

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
inst_1 : MeasurableSpace ε
inst_2 : TopologicalSpace ε
inst_3 : TopologicalSpace.PseudoMetrizableSpace ε
inst_4 : BorelSpace ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
⊢ AEMeasurable f μ

Tactic:
hf.aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
rw : q ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ = eLpNorm' f q μ ^ q

Tactic:
rw [eLpNorm'_eq_lintegral_enorm, ← ENNReal.rpow_mul, one_div, inv_mul_cancel₀, ENNReal.rpow_one]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, one_div, MeasureTheory.eLpNorm'_eq_lintegral_enorm, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0

Tactic:
hq0_lt.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
inst : ENorm ε
μ : Measure α
f : α → ε
hq0_lt : 0 < q
⊢ q ≠ 0

Tactic:
exact hq0_lt.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Defs
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
inst : ENorm ε
μ : Measure α
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ eLpNorm f (↑p : ℝ≥0∞) μ ^ (↑p : ℝ) = ∫⁻ (x : α), ‖f x‖ₑ ^ (↑p : ℝ) ∂μ

Tactic:
simp [eLpNorm_eq_eLpNorm' (by exact_mod_cast hp) ENNReal.coe_ne_top,
    lintegral_rpow_enorm_eq_rpow_eLpNorm' ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hp)]

Premises used: Iff.mpr, MeasureTheory.eLpNorm_eq_eLpNorm', MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm', Iff.trans, NNReal.coe_pos, pos_iff_ne_zero, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
pos : ∀ (hp_zero : p = 0), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
neg : ∀ (hp_zero : ¬p = 0), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : p = 0
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Premises used: MeasureTheory.eLpNorm_exponent_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
neg : ∀ (hp_top : ¬p = ∞), eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : p = ∞
pos : eLpNorm (s.indicator f) ∞ μ = eLpNorm f ∞ (μ.restrict s)
pos₁ : eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)
pos₂ : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.indicator f x‖ₑ) μ) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s))
pos₃ :
  Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) μ)
    (essSup (fun (a : α) ↦ ‖f a‖ₑ) (μ.restrict s))
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp_rw [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm,
       enorm_indicator_eq_indicator_enorm, ENNReal.essSup_indicator_eq_essSup_restrict hs]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, ENNReal.essSup_indicator_eq_essSup_restrict, enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ eLpNorm (s.indicator f) p μ = eLpNorm f p (μ.restrict s)

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top]

Premises used: MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (a : α), s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a ∂μ) ^ (1 / p.toReal)
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [← lintegral_indicator hs]

Premises used: MeasureTheory.lintegral_indicator
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖s.indicator f x‖ₑ ^ p.toReal) fun (a : α) ↦
    s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
⊢ (∫⁻ (x : α), ‖s.indicator f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (a : α), s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a ∂μ) ^ (1 / p.toReal)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (α := ℝ≥0∞) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal)
    fun (a : α) ↦ s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖s.indicator f x‖ₑ ^ p.toReal) fun (a : α) ↦
    s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a

Tactic:
simp_rw [enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (α := ℝ≥0∞) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal)
    fun (a : α) ↦ s.indicator (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) a

Tactic:
rw [eq_comm, ← Function.comp_def (fun x : ℝ≥0∞ => x ^ p.toReal), Set.indicator_comp_of_zero,
    Function.comp_def]

Premises used: eq_comm, Function.comp_def, Set.indicator_comp_of_zero, ENNReal.toReal, HPow.hPow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
s : Set α
hs : MeasurableSet s
hp_zero : ¬p = 0
hp_top : ¬p = ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0

Tactic:
simp [ENNReal.toReal_pos hp_zero hp_top]

Premises used: ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε' : Type u_8
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
f : α → ε'
p : ℝ≥0∞
μ : Measure α
s : Set α
⊢ eLpNorm f p (μ.restrict s) ≤ eLpNorm f p μ

Tactic:
eLpNorm_mono_measure f Measure.restrict_le_self

Premises used: MeasureTheory.Measure.restrict_le_self, MeasureTheory.eLpNorm_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Tactic:
eLpNorm_mono_ae' <| .of_forall fun x ↦ ?_

Premises used: Filter.Eventually.of_forall, MeasureTheory.eLpNorm_mono_ae'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
refine : ∀ (x : α), ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ
⊢ eLpNorm (s.indicator f) p μ ≤ eLpNorm f p μ

Tactic:
refine eLpNorm_mono_ae' <| .of_forall fun x ↦ ?_

Premises used: MeasureTheory.eLpNorm_mono_ae'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ
⊢ ‖s.indicator f x‖ₑ ≤ ‖f x‖ₑ

Tactic:
rw [enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ

Tactic:
s.indicator_le_self _ x

Premises used: Set.indicator_le_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
x : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) x ≤ ‖f x‖ₑ

Tactic:
exact s.indicator_le_self _ x

Premises used: Set.indicator_le_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
essSup_mono_ae (Eventually.of_forall fun x => ?_)

Premises used: Filter.Eventually.of_forall, essSup_mono_ae, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
refine : ∀ (x : α), LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ ‖s.indicator f x‖ₑ) x) ((fun (x : α) ↦ ‖f x‖ₑ) x)
⊢ eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ

Tactic:
refine essSup_mono_ae (Eventually.of_forall fun x => ?_)

Premises used: Filter.Eventually.of_forall, essSup_mono_ae