α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ ∀ (s : Set α), ↑m s ≤ extend (fun s x => ↑m s) s

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ m ≤ trim m
apply le_ofFunction.mpr
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ↑m s ≤ extend (fun s x => ↑m s) s

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ ∀ (s : Set α), ↑m s ≤ extend (fun s x => ↑m s) s

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
intro s
case h
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∀ (i : (fun s => MeasurableSet s) s), ↑m s ≤ (fun s x => ↑m s) s i

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ↑m s ≤ extend (fun s x => ↑m s) s

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
apply le_iInf
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
case h
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ∀ (i : (fun s => MeasurableSet s) s), ↑m s ≤ (fun s x => ↑m s) s i

α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
simp
no goals
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
⊢ extend (fun s x => ↑m s) ∅ = 0
apply extend_empty <;> simp