-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem norm_integral_sub_setIntegral_le [IsFiniteMeasure μ] {C : ℝ}
    (hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) {s : Set X} (hs : MeasurableSet s) (hf1 : Integrable f μ) :
    ‖∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ ∫ (x : X) in sᶜ, C ∂μ = (μ sᶜ).toReal * C

Tactic:
rw [setIntegral_const C, smul_eq_mul]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Tactic:
have h1 : ∫ x in sᶜ, ‖f x‖ ∂μ ≤ ∫ _ in sᶜ, C ∂μ :=
  integral_mono_ae (Integrable.restrict (Integrable.norm hf1))
    (integrable_const C) (ae_restrict_of_ae hf)

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = (μ sᶜ).toReal * C
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Tactic:
rw [h0, ← h2]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = (μ sᶜ).toReal * C
⊢ ‖∫ (x : X) in sᶜ, f x ∂μ‖ ≤ ∫ (x : X) in sᶜ, C ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Tactic:
have h0 : ∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ = ∫ x in sᶜ, f x ∂μ := by
  rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Tactic:
have h2 : ∫ _ in sᶜ, C ∂μ = (μ sᶜ).toReal * C := by
  rw [setIntegral_const C, smul_eq_mul]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = (μ sᶜ).toReal * C
⊢ ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ (μ sᶜ).toReal * C

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = (μ sᶜ).toReal * C
⊢ ‖∫ (x : X) in sᶜ, f x ∂μ‖ ≤ ∫ (x : X) in sᶜ, C ∂μ

Tactic:
exact le_trans (norm_integral_le_integral_norm f) h1

Result:
no goals