Theorem: exists_mul_eq_setInterval_Icc (ForML/IntegralMeanValue.lean)

State before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
Tactic:
apply exists_mul_eq_setInterval hf_cont hg_int hg_nonneg h_int <;> try simp [hab]
State after:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsPreconnected (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)

State before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsPreconnected (Set.Icc a b)

a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
Tactic:
repeat simp [isClosed_Icc, isPreconnected_Icc, hab]
State after:
no goals

State before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ MeasurableSet (Set.Icc a b)
Tactic:
simp [hab]
State after:
no goals

State before:
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
Tactic:
simp [isClosed_Icc, isPreconnected_Icc, hab]
State after:
no goals