awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
x : α
pos :
  ∀ (hx : x ∈ s),
    ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
      s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
⊢ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
have neg : ∀ (hx : x ∉ s),
  ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
have pos : ∀ (hp_zero : p = 0), MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
pos : ∀ (hp_zero : p = 0), MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
have neg : ∀ (hp_zero : ¬p = 0), MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
have pos : AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ ε) f g) μ
Tactic: simp only [hp_zero, memLp_zero_iff_aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
have neg : eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
Tactic: refine ⟨AEStronglyMeasurable.piecewise hs hf.1 hg.1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
have neg : ∀ (hf : MemLp f ∞ (μ.restrict s)) (hg : MemLp g ∞ (μ.restrict sᶜ)) (hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0),
  eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ < ∞
Tactic: obtain rfl | hp_top := eq_or_ne p ∞
Cleared hypotheses: p, hf, hg, hp_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
neg :
  ∀ (hf : MemLp f ∞ (μ.restrict s)) (hg : MemLp g ∞ (μ.restrict sᶜ)) (hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0),
    eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ < ∞
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
have neg₁ : ∀ (hp_top : p ≠ ∞), eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
Tactic: obtain rfl | hp_top := eq_or_ne p ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f ∞ (μ.restrict s)
hg : MemLp g ∞ (μ.restrict sᶜ)
hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ < ∞
have neg : max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ)) < ∞
Tactic: rw [eLpNorm_top_piecewise f g hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
have neg : ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞ ∧
  ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_zero hp_top, ← lintegral_add_compl _ hs,
    ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞ ∧
    ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have neg : ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
neg : ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞ ∧
    ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have neg₁ : ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have h : ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
Tactic: have h (x) (hx : x ∈ s) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal := by
      simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have neg : ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ < ∞
Tactic: rw [setLIntegral_congr_fun hs h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ sᶜ
⊢ ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
have hx' : x ∉ s
Tactic: have hx' : x ∉ s := hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have h : ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
Tactic: have h (x) (hx : x ∈ sᶜ) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal := by
      have hx' : x ∉ s := hx
      simp [hx']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
have neg : ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ∞
Tactic: rw [setLIntegral_congr_fun hs.compl h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have pos : ∀ (hp : p = 0),
  eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
pos :
  ∀ (hp : p = 0),
    eLpNorm (s.indicator (f - g)) p μ ≤
      ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg : ∀ (hp : ¬p = 0),
  eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
have pos : ∀ (hx : x ∈ s), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
pos : ∀ (hx : x ∈ s), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
have neg : ∀ (hx : x ∉ s), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
x : α
hx : x ∈ s
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
have pos : dist (f x) (g x) ≤ c
Tactic: rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
Tactic: have : ∀ x, ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun _ => c) x‖ := by
    intro x
    by_cases hx : x ∈ s
    · rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]
      exact hf x hx
    · simp [Set.indicator_of_notMem hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg : eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg :
  eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg₁ : ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg :
  eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg₂ : ENNReal.ofReal ‖c‖ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg :
  eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₂ :
  ENNReal.ofReal ‖c‖ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg₃ : ENNReal.ofReal |c| * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg :
  eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₂ :
  ENNReal.ofReal ‖c‖ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₃ :
  ENNReal.ofReal |c| * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have neg₄ : ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ s.indicator (f - g) = f - g
have rw : Function.support (f - g) ⊆ s
Tactic: rw [Set.indicator_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have hs₃ : s.indicator (f - g) = f - g
Tactic: have hs₃ : s.indicator (f - g) = f - g := by
    rw [Set.indicator_eq_self]
    exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have rw : eLpNorm (s.indicator (f - g)) p μ ≤
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: rw [← hs₃]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
have inl : ∀ (hp_top : Ne (α := ℝ≥0∞) 0 ∞) (hf : MemLp f 0 μ),
  ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε
Tactic: rcases eq_or_ne p 0 with rfl | hp₀
Cleared hypotheses: p, hp_top, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSeminorm.Indicator (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (hp_top : Ne (α := ℝ≥0∞) 0 ∞) (hf : MemLp f 0 μ),
    ∃ (s : Set α),
      MeasurableSet s ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
have inr : ∀ (hp₀ : p ≠ 0),
  ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
Tactic: rcases eq_or_ne p 0 with rfl | hp₀