awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) =
    ENNReal.ofReal (‖c‖ * μ.real s ^ (1 / p.toReal))
have rw : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≠ ∞
Tactic: rw [ENNReal.ofReal_mul (norm_nonneg _), ofReal_norm, measureReal_def,
    ENNReal.toReal_rpow, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ edist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c) =
    enorm (E := ↥(Lp E p μ)) (indicatorConstLp (s := s ∆ t) p ⋯ ⋯ c)
have unfold : edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) sorry) (MemLp.toLp (t.indicator fun (x : α) ↦ c) sorry) =
  enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) sorry)
Tactic: unfold indicatorConstLp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
have rw : eLpNorm (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)) p μ =
  enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) sorry)
Tactic: rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  eLpNorm (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)) p μ =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
⊢ edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
have rw₁ : eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ =
  enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) sorry)
Tactic: rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  eLpNorm (HSub.hSub (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)) p μ =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
rw₁ :
  eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
⊢ edist (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) ⋯) (MemLp.toLp (t.indicator fun (x : α) ↦ c) ⋯) =
    enorm (E := ↥(Lp E p μ)) (MemLp.toLp ((s ∆ t).indicator fun (x : α) ↦ c) ⋯)
have rw₂ : eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ =
  eLpNorm.{u_1, u_2} (ε := E) ((s ∆ t).indicator fun (x : α) ↦ c) p μ
Tactic: rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (β := ↥(Lp E p μ)) (fun (b : β) ↦ indicatorConstLp (s := t b) p ⋯ ⋯ c) l
    (𝓝 (indicatorConstLp (s := s) p hs hμs c))
have rw : Tendsto (β := ℝ)
  (fun (b : β) ↦ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := t b) p sorry sorry c) (indicatorConstLp (s := s) p hs hμs c)) l
  (𝓝 0)
Tactic: rw [tendsto_iff_dist_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (b : β) ↦ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := t b) p ⋯ ⋯ c) (indicatorConstLp (s := s) p hs hμs c))
    l (𝓝 0)
have hp₀ : p ≠ 0
Tactic: have hp₀ : p ≠ 0 := (one_pos.trans_le hp₁.out).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ Tendsto (β := ℝ)
    (fun (b : β) ↦ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := t b) p ⋯ ⋯ c) (indicatorConstLp (s := s) p hs hμs c))
    l (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (b : β) ↦ ‖c‖ * μ.real (t b ∆ s) ^ (1 / p.toReal)) l (𝓝 0)
Tactic: simp only [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp hp₀ hp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
⊢ Tendsto (β := ℝ) (fun (b : β) ↦ ‖c‖ * μ.real (t b ∆ s) ^ (1 / p.toReal)) l (𝓝 0)
have h₁ : 0 = ‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)
Tactic: convert!
    tendsto_const_nhds.mul (((ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h).rpow_const _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hp₁ : Fact (1 ≤ p)
β : Type u_3
l : Filter β
t : β → Set α
ht : ∀ (b : β), MeasurableSet (t b)
hμt : ∀ (b : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t b) : ℝ≥0∞) (∞ : ℝ≥0∞)
hp : p ≠ ∞
h : Tendsto (β := ℝ≥0∞) (fun (b : β) ↦ (μ : (a : Set α) → ℝ≥0∞) (t b ∆ s)) l (𝓝 0)
hp₀ : p ≠ 0
h₁ : 0 = ‖c‖ * ENNReal.toReal 0 ^ (1 / p.toReal)
⊢ Tendsto (β := ℝ) (fun (b : β) ↦ ‖c‖ * μ.real (t b ∆ s) ^ (1 / p.toReal)) l (𝓝 0)
have convert_3 : ENNReal.toReal 0 ≠ 0 ∨ 0 ≤ 1 / p.toReal
Tactic: convert!
    tendsto_const_nhds.mul (((ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp h).rpow_const _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hc : c ≠ 0
⊢ Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔ s =ᶠ[ae μ] t
have simp_rw : Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
Tactic: simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hc : c ≠ 0
simp_rw :
  Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔
    EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
⊢ Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hsμ c) (indicatorConstLp (s := t) p ht htμ c) ↔ s =ᶠ[ae μ] t
have simp_rw₁ : Eq (α := ↥(Lp E p μ)) (MemLp.toLp (s.indicator fun (x : α) ↦ c) sorry) (MemLp.toLp (t.indicator fun (x : α) ↦ c) sorry) ↔
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
Tactic: simp_rw [← indicator_const_eventuallyEq hc, indicatorConstLp, MemLp.toLp_eq_toLp_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ
have refine_1 : ∀ (hfg : MemLp (f + g) p μ), MemLp f p μ
Tactic: refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
refine_1 : ∀ (hfg : MemLp (f + g) p μ), MemLp f p μ
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ
have refine_2 : ∀ (hfg : MemLp (f + g) p μ), MemLp g p μ
Tactic: refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ
have refine_1 : MemLp ((support f).indicator (f + g)) p μ
Tactic: rw [← Set.indicator_add_eq_left h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ
have refine_2 : MemLp ((support g).indicator (f + g)) p μ
Tactic: rw [← Set.indicator_add_eq_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
⊢ indicatorConstLp (s := s ∪ t) p ⋯ ⋯ c =
    HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)
have h : (↑(↑(indicatorConstLp (s := s ∪ t) p sorry sorry c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  (↑(↑(HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)) :
        α →ₘ[μ] E) :
    α → E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
⊢ (↑(↑(indicatorConstLp (s := s ∪ t) p ⋯ ⋯ c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) (indicatorConstLp (s := t) p ht hμt c)) :
          α →ₘ[μ] E) :
      α → E)
have h : ((s ∪ t).indicator fun (x : α) ↦ c) =ᶠ[ae μ]
  HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
Tactic: grw [Lp.coeFn_add, indicatorConstLp_coeFn, indicatorConstLp_coeFn, indicatorConstLp_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun (x : α) ↦ c) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
have h : (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)) =ᶠ[ae μ]
  HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
Tactic: rw [Set.indicator_union_of_disjoint hst, Pi.add_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
h :
  (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
⊢ ((s ∪ t).indicator fun (x : α) ↦ c) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
have h₁ : EventuallyEq.{u_1, u_2} (β := E) (ae μ)
  (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)) fun (a : α) ↦
  HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)
Tactic: rw [Set.indicator_union_of_disjoint hst, Pi.add_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have this : μ ≠ 0
Tactic: have := NeZero.ne μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Tactic: rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw₁ : ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₁ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw₂ : ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₁ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₂ :
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw₃ : ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal) =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Tactic: rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw : (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw₁ : ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]