Theorem: exists_mul_eq_setInterval (ForML/IntegralMeanValue.lean)

State before:
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
have hz' : ∫ x in s, g x ∂μ = ENNReal.toReal (∫⁻ x in s, ↑‖g x‖₊ ∂μ)
State after:
case hz'
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
⊢ ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)

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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
case hz'
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
⊢ ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)

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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
. rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
  rw [integral_congr_ae]
  apply Filter.Eventually.mp hg_nonneg
  simp
  apply Filter.eventually_of_forall
  intro x hx
  symm
  rw [abs_eq_self]
  exact hx
State after:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [ENNReal.toReal] at hz'
State after:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
generalize hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
State after:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
z : NNReal
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
z : NNReal
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [hz] at hz'
State after:
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  simp [hz_zero] at hz'
  simp [hz']
  refine And.intro hs_ne ?_
  apply integral_eq_zero_of_ae
  rw [integral_eq_zero_iff_of_nonneg_ae hg_nonneg hg_int] at hz'
  apply Filter.Eventually.mp hz'
  simp
  apply Filter.eventually_of_forall
  intro x hx
  exact Or.inr hx
| inr hz_pos =>
  have hmM := existsBoundsOn_integral_mul_nonneg hs_meas hg_int hg_nonneg ?_ h_int
  swap
  . intro h_zero
    simp [h_zero] at hz'
    rw [eq_comm] at hz'
    rw [NNReal.coe_eq_zero] at hz'
    simp [hz'] at hz_pos
  rw [hz']
  rw [hz'] at hmM
  have hz_ne_zero : (z : ℝ) ≠ 0 := ne_of_gt hz_pos
  conv => arg 1; intro c; rhs; rw [← div_eq_iff hz_ne_zero]
  rcases hmM with ⟨m, hmM⟩
  rcases hmM with ⟨M, hmM⟩
  rcases hmM with ⟨⟨hm_mem, hM_mem⟩, ⟨hm, hM⟩⟩
  cases eq_or_gt_of_le hm with
  | inl hm => exists m
  | inr hm_lt =>
    cases eq_or_lt_of_le hM with
    | inl hM_eq => exists M
    | inr hM_lt =>
      simp_rw [eq_comm]
      rw [← Set.mem_image]
      refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
      . exact And.intro hm_lt hM_lt
      . refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
          hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
          hf_cont _ _ ?_ ?_
        . rw [← mem_closure_iff_nhdsWithin_neBot]
          rw [IsClosed.closure_eq hs_closed]
          exact hm_mem
        . rw [← mem_closure_iff_nhdsWithin_neBot]
          rw [IsClosed.closure_eq hs_closed]
          exact hM_mem
        . simp; exact self_mem_nhdsWithin
        . simp; exact self_mem_nhdsWithin
        . exact hf_cont m hm_mem
        . exact hf_cont M hM_mem
State after:
no goals

State before:
case hz'
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
⊢ ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
Tactic:
rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
State after:
case hz'
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
⊢ ∫ (x : ℝ) in s, g x ∂μ = ∫ (x : ℝ) in s, ‖g x‖ ∂μ

State before:
case hz'
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
⊢ ∫ (x : ℝ) in s, g x ∂μ = ∫ (x : ℝ) in s, ‖g x‖ ∂μ
Tactic:
rw [integral_congr_ae]
State after:
case hz'
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
⊢ (fun x => g x) =ᵐ[Measure.restrict μ s] fun a => ‖g a‖

State before:
case hz'
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
⊢ (fun x => g x) =ᵐ[Measure.restrict μ s] fun a => ‖g a‖
Tactic:
apply Filter.Eventually.mp hg_nonneg
State after:
case hz'
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
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => g x) x = (fun a => ‖g a‖) x

State before:
case hz'
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
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => g x) x = (fun a => ‖g a‖) x
Tactic:
simp
State after:
case hz'
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
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → g x = |g x|

State before:
case hz'
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
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → g x = |g x|
Tactic:
apply Filter.eventually_of_forall
State after:
case hz'.hp
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
⊢ ∀ (x : ℝ), 0 ≤ g x → g x = |g x|

State before:
case hz'.hp
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
⊢ ∀ (x : ℝ), 0 ≤ g x → g x = |g x|
Tactic:
intro x hx
State after:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ g x = |g x|

State before:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ g x = |g x|
Tactic:
symm
State after:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ |g x| = g x

State before:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ |g x| = g x
Tactic:
rw [abs_eq_self]
State after:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ 0 ≤ g x

State before:
case hz'.hp
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
x : ℝ
hx : 0 ≤ g x
⊢ 0 ≤ g x
Tactic:
exact hx
State after:
no goals

State before:
case inl
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_zero : z = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
simp [hz_zero] at hz'
State after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
simp [hz']
State after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (∃ x, x ∈ s) ∧ ∫ (x : ℝ) in s, f x * g x ∂μ = 0

State before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (∃ x, x ∈ s) ∧ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Tactic:
refine And.intro hs_ne ?_
State after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∫ (x : ℝ) in s, f x * g x ∂μ = 0

State before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Tactic:
apply integral_eq_zero_of_ae
State after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0

State before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Tactic:
rw [integral_eq_zero_iff_of_nonneg_ae hg_nonneg hg_int] at hz'
State after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0

State before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Tactic:
apply Filter.Eventually.mp hz'
State after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 x → (fun a => f a * g a) x = 0 x

State before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 x → (fun a => f a * g a) x = 0 x
Tactic:
simp
State after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 → f x = 0 ∨ g x = 0

State before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 → f x = 0 ∨ g x = 0
Tactic:
apply Filter.eventually_of_forall
State after:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ (x : ℝ), g x = 0 → f x = 0 ∨ g x = 0

State before:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ (x : ℝ), g x = 0 → f x = 0 ∨ g x = 0
Tactic:
intro x hx
State after:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
x : ℝ
hx : g x = 0
⊢ f x = 0 ∨ g x = 0

State before:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
x : ℝ
hx : g x = 0
⊢ f x = 0 ∨ g x = 0
Tactic:
exact Or.inr hx
State after:
no goals

State before:
case inr
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
have hmM := existsBoundsOn_integral_mul_nonneg hs_meas hg_int hg_nonneg ?_ h_int
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

case inr.refine_1
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
⊢ ∫ (x : ℝ) in s, g x ∂μ ≠ 0

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

case inr.refine_1
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
⊢ ∫ (x : ℝ) in s, g x ∂μ ≠ 0
Tactic:
swap
State after:
case inr.refine_1
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
⊢ ∫ (x : ℝ) in s, g x ∂μ ≠ 0

case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
case inr.refine_1
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
⊢ ∫ (x : ℝ) in s, g x ∂μ ≠ 0

case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
. intro h_zero
  simp [h_zero] at hz'
  rw [eq_comm] at hz'
  rw [NNReal.coe_eq_zero] at hz'
  simp [hz'] at hz_pos
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [hz']
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z
Tactic:
rw [hz'] at hmM
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z
Tactic:
have hz_ne_zero : (z : ℝ) ≠ 0 := ne_of_gt hz_pos
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
hz_ne_zero : ↑z ≠ 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
hz_ne_zero : ↑z ≠ 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z
Tactic:
conv => arg 1; intro c; rhs; rw [← div_eq_iff hz_ne_zero]
State after:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
hz_ne_zero : ↑z ≠ 0
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c

State before:
case inr.refine_2
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
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
hz_ne_zero : ↑z ≠ 0
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
rcases hmM with ⟨m, hmM⟩
State after:
case inr.refine_2.intro
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 : ℝ
hmM : ∃ M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c

State before:
case inr.refine_2.intro
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 : ℝ
hmM : ∃ M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
rcases hmM with ⟨M, hmM⟩
State after:
case inr.refine_2.intro.intro
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 : ℝ
hmM : (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c

State before:
case inr.refine_2.intro.intro
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 : ℝ
hmM : (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
rcases hmM with ⟨⟨hm_mem, hM_mem⟩, ⟨hm, hM⟩⟩
State after:
case inr.refine_2.intro.intro.intro.intro.intro
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
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c

State before:
case inr.refine_2.intro.intro.intro.intro.intro
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
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
cases eq_or_gt_of_le hm with
| inl hm => exists m
| inr hm_lt =>
  cases eq_or_lt_of_le hM with
  | inl hM_eq => exists M
  | inr hM_lt =>
    simp_rw [eq_comm]
    rw [← Set.mem_image]
    refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
    . exact And.intro hm_lt hM_lt
    . refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
        hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
        hf_cont _ _ ?_ ?_
      . rw [← mem_closure_iff_nhdsWithin_neBot]
        rw [IsClosed.closure_eq hs_closed]
        exact hm_mem
      . rw [← mem_closure_iff_nhdsWithin_neBot]
        rw [IsClosed.closure_eq hs_closed]
        exact hM_mem
      . simp; exact self_mem_nhdsWithin
      . simp; exact self_mem_nhdsWithin
      . exact hf_cont m hm_mem
      . exact hf_cont M hM_mem
State after:
no goals

State before:
case inr.refine_1
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
⊢ ∫ (x : ℝ) in s, g x ∂μ ≠ 0
Tactic:
intro h_zero
State after:
case inr.refine_1
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
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ False

State before:
case inr.refine_1
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
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ False
Tactic:
simp [h_zero] at hz'
State after:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : 0 = ↑z
⊢ False

State before:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : 0 = ↑z
⊢ False
Tactic:
rw [eq_comm] at hz'
State after:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : ↑z = 0
⊢ False

State before:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : ↑z = 0
⊢ False
Tactic:
rw [NNReal.coe_eq_zero] at hz'
State after:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : z = 0
⊢ False

State before:
case inr.refine_1
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
h_zero : ∫ (x : ℝ) in s, g x ∂μ = 0
hz' : z = 0
⊢ False
Tactic:
simp [hz'] at hz_pos
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inl
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 : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f m
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
exists m
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr
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
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
cases eq_or_lt_of_le hM with
| inl hM_eq => exists M
| inr hM_lt =>
  simp_rw [eq_comm]
  rw [← Set.mem_image]
  refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
  . exact And.intro hm_lt hM_lt
  . refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
      hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
      hf_cont _ _ ?_ ?_
    . rw [← mem_closure_iff_nhdsWithin_neBot]
      rw [IsClosed.closure_eq hs_closed]
      exact hm_mem
    . rw [← mem_closure_iff_nhdsWithin_neBot]
      rw [IsClosed.closure_eq hs_closed]
      exact hM_mem
    . simp; exact self_mem_nhdsWithin
    . simp; exact self_mem_nhdsWithin
    . exact hf_cont m hm_mem
    . exact hf_cont M hM_mem
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inl
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_eq : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f M
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
exists M
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
simp_rw [eq_comm]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
⊢ ∃ c ∈ s, f c = (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
⊢ ∃ c ∈ s, f c = (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
Tactic:
rw [← Set.mem_image]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ (fun c => f c) '' s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ (fun c => f c) '' s
Tactic:
refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Tactic:
. exact And.intro hm_lt hM_lt
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Tactic:
. refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
    hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
    hf_cont _ _ ?_ ?_
  . rw [← mem_closure_iff_nhdsWithin_neBot]
    rw [IsClosed.closure_eq hs_closed]
    exact hm_mem
  . rw [← mem_closure_iff_nhdsWithin_neBot]
    rw [IsClosed.closure_eq hs_closed]
    exact hM_mem
  . simp; exact self_mem_nhdsWithin
  . simp; exact self_mem_nhdsWithin
  . exact hf_cont m hm_mem
  . exact hf_cont M hM_mem
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)
Tactic:
exact And.intro hm_lt hM_lt
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Tactic:
refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
  hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
  hf_cont _ _ ?_ ?_
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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.NeBot (nhdsWithin m s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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.NeBot (nhdsWithin M s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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))

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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.NeBot (nhdsWithin m s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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.NeBot (nhdsWithin M s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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:
. rw [← mem_closure_iff_nhdsWithin_neBot]
  rw [IsClosed.closure_eq hs_closed]
  exact hm_mem
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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.NeBot (nhdsWithin M s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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))

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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.NeBot (nhdsWithin M s)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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:
. rw [← mem_closure_iff_nhdsWithin_neBot]
  rw [IsClosed.closure_eq hs_closed]
  exact hM_mem
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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))

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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_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
State after:
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))

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
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))

State before:
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:
. exact hf_cont m hm_mem
State after:
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))

State before:
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:
. exact hf_cont M hM_mem
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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.NeBot (nhdsWithin m s)
Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
⊢ m ∈ closure s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
⊢ m ∈ closure s
Tactic:
rw [IsClosed.closure_eq hs_closed]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
⊢ m ∈ s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
⊢ m ∈ s
Tactic:
exact hm_mem
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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.NeBot (nhdsWithin M s)
Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
⊢ M ∈ closure s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
⊢ M ∈ closure s
Tactic:
rw [IsClosed.closure_eq hs_closed]
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
⊢ M ∈ s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
⊢ M ∈ s
Tactic:
exact hM_mem
State after:
no goals

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
Tactic:
simp
State after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
⊢ s ∈ nhdsWithin m s

State before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
⊢ s ∈ nhdsWithin m s
Tactic:
exact self_mem_nhdsWithin
State after:
no goals

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
Tactic:
simp
State after:
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
⊢ s ∈ nhdsWithin M s

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
⊢ s ∈ nhdsWithin M s
Tactic:
exact self_mem_nhdsWithin
State after:
no goals

State before:
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))
Tactic:
exact hf_cont m hm_mem
State after:
no goals

State before:
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:
exact hf_cont M hM_mem
State after:
no goals