α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
rw [← Lp.simpleFunc.coeFn_nonneg] at hf
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
have hf_ae : 0 ≤ᵐ[μ] simpleFunc.toSimpleFunc f := by
  filter_upwards [toSimpleFunc_eq_toFun f, hf] with _ h1 _; rwa [h1]
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
let s := toMeasurable μ { x | ¬0 ≤ simpleFunc.toSimpleFunc f x }ᶜ
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
have hs_zero : μ (sᶜ) = 0 := by
  rw [compl_compl, measure_toMeasurable]; rwa [EventuallyLE, ae_iff] at hf_ae
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
have hfs_nonneg : ∀ x ∈ s, 0 ≤ simpleFunc.toSimpleFunc f x := by
  intro x hxs
  rw [mem_compl_iff] at hxs
  have hx' : x ∉ { a : α | ¬0 ≤ simpleFunc.toSimpleFunc f a } := fun h =>
    hxs (subset_toMeasurable μ _ h)
  rwa [Set.nmem_setOf_iff, Classical.not_not] at hx'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
let f' :=
  SimpleFunc.piecewise s (measurableSet_toMeasurable μ _).compl (simpleFunc.toSimpleFunc f)
    (SimpleFunc.const α (0 : G))
case refine'_1
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
⊢ ↑0 x ≤ ↑f' x

case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑↑f =ᵐ[μ] ↑f'
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
refine' ⟨f', fun x => _, _⟩
case h
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
h1 : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑(toSimpleFunc f) a✝¹
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
⊢ 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
filter_upwards [toSimpleFunc_eq_toFun f, hf] with _ h1 _
no goals
case h
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
h1 : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑(toSimpleFunc f) a✝¹
rwa [h1]
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
⊢ ↑↑μ {x | ¬0 ≤ ↑(toSimpleFunc f) x} = 0
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
⊢ ↑↑μ (sᶜ) = 0
rw [compl_compl, measure_toMeasurable]
no goals
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
⊢ ↑↑μ {x | ¬0 ≤ ↑(toSimpleFunc f) x} = 0
rwa [EventuallyLE, ae_iff] at hf_ae
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : x ∈ s
⊢ 0 ≤ ↑(toSimpleFunc f) x
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
⊢ ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
intro x hxs
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : ¬x ∈ toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}
⊢ 0 ≤ ↑(toSimpleFunc f) x
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : x ∈ s
⊢ 0 ≤ ↑(toSimpleFunc f) x
rw [mem_compl_iff] at hxs
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : ¬x ∈ toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}
hx' : ¬x ∈ {a | ¬0 ≤ ↑(toSimpleFunc f) a}
⊢ 0 ≤ ↑(toSimpleFunc f) x
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : ¬x ∈ toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}
⊢ 0 ≤ ↑(toSimpleFunc f) x
have hx' : x ∉ { a : α | ¬0 ≤ simpleFunc.toSimpleFunc f a } := fun h =>
  hxs (subset_toMeasurable μ _ h)
no goals
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
x : α
hxs : ¬x ∈ toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}
hx' : ¬x ∈ {a | ¬0 ≤ ↑(toSimpleFunc f) a}
⊢ 0 ≤ ↑(toSimpleFunc f) x
rwa [Set.nmem_setOf_iff, Classical.not_not] at hx'
case refine'_1
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x
case refine'_1
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
⊢ ↑0 x ≤ ↑f' x
rw [SimpleFunc.piecewise_apply]
case pos
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : x ∈ s
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x

case neg
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : ¬x ∈ s
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x
case refine'_1
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x
by_cases hxs : x ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : x ∈ s
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x
simp only [hxs, hfs_nonneg x hxs, if_true, Pi.zero_apply, SimpleFunc.coe_zero]
case neg
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : ¬x ∈ s
⊢ ↑0 x ≤ ↑0 x
case neg
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : ¬x ∈ s
⊢ ↑0 x ≤ if x ∈ s then ↑(toSimpleFunc f) x else ↑(SimpleFunc.const α 0) x
simp only [hxs, SimpleFunc.const_zero, if_false]
no goals
case neg
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
x : α
hxs : ¬x ∈ s
⊢ ↑0 x ≤ ↑0 x
rfl
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑↑f =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑↑f =ᵐ[μ] ↑f'
rw [SimpleFunc.coe_piecewise]
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this : s =ᵐ[μ] Set.univ
⊢ ↑↑↑f =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑↑f =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
have : s =ᵐ[μ] univ := by
  rw [ae_eq_set]
  simp only [true_and_iff, measure_empty, eq_self_iff_true, diff_univ, ← compl_eq_univ_diff]
  exact hs_zero
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this : s =ᵐ[μ] Set.univ
⊢ ↑(toSimpleFunc f) =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this : s =ᵐ[μ] Set.univ
⊢ ↑↑↑f =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
refine' EventuallyEq.trans (toSimpleFunc_eq_toFun f).symm _
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this : s =ᵐ[μ] Set.univ
⊢ ↑(toSimpleFunc f) =ᵐ[μ] Set.piecewise Set.univ ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this : s =ᵐ[μ] Set.univ
⊢ ↑(toSimpleFunc f) =ᵐ[μ] Set.piecewise s ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
refine' EventuallyEq.trans _ (piecewise_ae_eq_of_ae_eq_set this.symm)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this✝ : s =ᵐ[μ] Set.univ
this : DecidablePred fun x => x ∈ Set.univ := fun x => Classical.propDecidable ((fun x => x ∈ Set.univ) x)
⊢ ↑(toSimpleFunc f) =ᵐ[μ] ↑(toSimpleFunc f)
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this✝ : s =ᵐ[μ] Set.univ
this : DecidablePred fun x => x ∈ Set.univ := fun x => Classical.propDecidable ((fun x => x ∈ Set.univ) x)
⊢ ↑(toSimpleFunc f) =ᵐ[μ] Set.piecewise Set.univ ↑(toSimpleFunc f) ↑(SimpleFunc.const α 0)
simp only [SimpleFunc.const_zero, indicator_univ, piecewise_eq_indicator, SimpleFunc.coe_zero]
no goals
case refine'_2
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
this✝ : s =ᵐ[μ] Set.univ
this : DecidablePred fun x => x ∈ Set.univ := fun x => Classical.propDecidable ((fun x => x ∈ Set.univ) x)
⊢ ↑(toSimpleFunc f) =ᵐ[μ] ↑(toSimpleFunc f)
rfl
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑μ (s \ Set.univ) = 0 ∧ ↑↑μ (Set.univ \ s) = 0
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ s =ᵐ[μ] Set.univ
rw [ae_eq_set]
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑μ (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜᶜ) = 0
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑μ (s \ Set.univ) = 0 ∧ ↑↑μ (Set.univ \ s) = 0
simp only [true_and_iff, measure_empty, eq_self_iff_true, diff_univ, ← compl_eq_univ_diff]
no goals
α : Type u_1
β : Type ?u.2426547
ι : Type ?u.2426550
E : Type ?u.2426553
F : Type ?u.2426556
𝕜 : Type ?u.2426559
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
hf : 0 ≤ᵐ[μ] ↑↑↑f
hf_ae : 0 ≤ᵐ[μ] ↑(toSimpleFunc f)
s : Set α := toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ
hs_zero : ↑↑μ (sᶜ) = 0
hfs_nonneg : ∀ (x : α), x ∈ s → 0 ≤ ↑(toSimpleFunc f) x
f' : α →ₛ G :=
  SimpleFunc.piecewise s (_ : MeasurableSet (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜ)) (toSimpleFunc f)
    (SimpleFunc.const α 0)
⊢ ↑↑μ (toMeasurable μ {x | ¬0 ≤ ↑(toSimpleFunc f) x}ᶜᶜ) = 0
exact hs_zero