-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem continuous_setIntegral [NormedSpace ℝ E] (s : Set X) :
    Continuous fun f : X →₁[μ] E => ∫ x in s, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ

Tactic:
rw [h_comp]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous (integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f))

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous (integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f))

Tactic:
exact continuous_integral.comp (LpToLpRestrictCLM X E ℝ μ 1 s).continuous

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
⊢ Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ

Tactic:
haveI : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
⊢ Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
⊢ Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ

Tactic:
have h_comp :
  (fun f : X →₁[μ] E => ∫ x in s, f x ∂μ) =
    integral (μ.restrict s) ∘ fun f => LpToLpRestrictCLM X E ℝ μ 1 s f := by
  ext1 f
  rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
h_comp : (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)
⊢ Continuous fun f => ∫ (x : X) in s, ↑↑f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
⊢ (fun f => ∫ (x : X) in s, ↑↑f x ∂μ) = integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)

Tactic:
ext1 f

Result:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
f : ↥(Lp E 1 μ)
⊢ ∫ (x : X) in s, ↑↑f x ∂μ = (integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)) f

Proof state:
case h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
inst✝ : NormedSpace ℝ E
s : Set X
this : Fact (1 ≤ 1)
f : ↥(Lp E 1 μ)
⊢ ∫ (x : X) in s, ↑↑f x ∂μ = (integral (μ.restrict s) ∘ fun f => ↑↑((LpToLpRestrictCLM X E ℝ μ 1 s) f)) f

Tactic:
rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]

Result:
no goals