Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_4
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ nhdsWithin M s ≤ Filter.principal s

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_5
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin m s) (nhds (f m))

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))
Tactic:
. simp; exact self_mem_nhdsWithin
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_5
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin m s) (nhds (f m))

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))