awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
x : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f' x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t, f' x ∂μ := integral_congr_ae h.1.ae_eq_mk
    _ = ∫ x in s, f' x ∂μ := by
      apply
        setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)
      filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
      rw [← h'x h''x.1, hx h''x]
    _ = ∫ x in s, f x ∂μ := by
      apply integral_congr_ae
      apply ae_restrict_of_ae_restrict_of_subset hts
      exact h.1.ae_eq_mk.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X), f x ∂μ)
have symm : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have nth_rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: nth_rw 1 [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have apply : ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
Tactic: apply setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_univ (subset_univ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
⊢ ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
have h₁ : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∉ s → f x = 0) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ univ \ s → f x = 0) x} x}
    a
Tactic: filter_upwards [h] with x hx h'x using hx h'x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∉ s → f x = 0) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ univ \ s → f x = 0) x} x}
      a
⊢ ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
have h₂ : ∀ (a : X), (a ∉ s → f a = 0) → a ∈ univ \ s → f a = 0
Tactic: filter_upwards [h] with x hx h'x using hx h'x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
have simp_rw : Eq.{u_1 + 1} (α := Set X) {x : X | f x < 0 ∨ f x = 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
Tactic: simp_rw [le_iff_lt_or_eq, setOf_or]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ) (∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ)
have h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
Tactic: have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
    simp_rw [le_iff_lt_or_eq, setOf_or]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ) (∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
  (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
Tactic: rw [h_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
have B : NullMeasurableSet {x : X | f x = 0} μ
Tactic: have B : NullMeasurableSet {x | f x = 0} μ :=
    hf.nullMeasurableSet_eq_fun aestronglyMeasurable_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
have symm : Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
  (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
have refine : ∀ᵐ (x : X) ∂μ.restrict {x : X | f x = 0}, f x = 0
Tactic: refine integral_union_eq_left_of_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
⊢ ∀ᵐ (x : X) ∂μ.restrict {x : X | f x = 0}, f x = 0
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ Membership.mem (γ := Set X) {x : X | f x = 0} x) x} x →
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x = 0) x} x}
    a
Tactic: filter_upwards [ae_restrict_mem₀ B] with x hx using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ Membership.mem (γ := Set X) {x : X | f x = 0} x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x = 0) x} x}
      a
⊢ ∀ᵐ (x : X) ∂μ.restrict {x : X | f x = 0}, f x = 0
have h₁ : ∀ (a : X), f a = 0 → f a = 0
Tactic: filter_upwards [ae_restrict_mem₀ B] with x hx using hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ ∫ (x : X), ‖f x‖ ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)
have rw : HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
  HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)
Tactic: rw [← integral_add_compl₀ h_meas hfi.norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)
have e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ)
have e_a : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x), ‖f x‖ = f x
Tactic: refine setIntegral_congr_fun₀ h_meas fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x} x
⊢ ‖f x‖ = f x
have rw : 0 ≤ f x
Tactic: rw [Real.norm_eq_abs, abs_eq_self.mpr _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)
have e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (-∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (-∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ)
have e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (∫ (a : X) in {x : X | 0 ≤ f x}ᶜ, -f a ∂μ)
Tactic: rw [← integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) (∫ (a : X) in {x : X | 0 ≤ f x}ᶜ, -f a ∂μ)
have e_a : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x), ‖f x‖ = -f x
Tactic: refine setIntegral_congr_fun₀ h_meas.compl fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x
⊢ ‖f x‖ = -f x
have rw : f x ≤ 0
Tactic: rw [Real.norm_eq_abs, abs_eq_neg_self.mpr _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : Membership.mem (γ := Set X) {x : X | 0 ≤ f x}ᶜ x
⊢ f x ≤ 0
have hx₁ : ¬0 ≤ f x
Tactic: rw [Set.mem_compl_iff, Set.notMem_setOf_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
x : X
hx : ¬0 ≤ f x
⊢ f x ≤ 0
have linarith : 0 < f x → f x - 0 + (0 - f x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, f x ∂μ) =
    HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ)
have rw : HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {a : X | ¬0 ≤ f a}, f x ∂μ) =
  HSub.hSub (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
Tactic: rw [← setIntegral_neg_eq_setIntegral_nonpos hfi.1, compl_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set X
μ : Measure X
inst_2 : CompleteSpace E
c : E
⊢ ∫ (x : X) in s, c ∂μ = μ.real s • c
have rw : (μ.restrict s).real univ • c = μ.real s • c
Tactic: rw [integral_const, measureReal_restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set X
μ : Measure X
inst_2 : CompleteSpace E
c : E
rw : (μ.restrict s).real univ • c = μ.real s • c
⊢ ∫ (x : X) in s, c ∂μ = μ.real s • c
have rw₁ : μ.real s • c = μ.real s • c
Tactic: rw [integral_const, measureReal_restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
⊢ ∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ = μ.real s • e
have rw : ∫ (x : X) in s, e ∂μ = μ.real s • e
Tactic: rw [integral_indicator s_meas, ← setIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
inst_2 : CompleteSpace E
e : E
s : Set X
s_meas : MeasurableSet s
rw : ∫ (x : X) in s, e ∂μ = μ.real s • e
⊢ ∫ (x : X), s.indicator (fun (x : X) ↦ e) x ∂μ = μ.real s • e
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, e ∂μ) (∫ (x : X) in s, e ∂μ)
Tactic: rw [integral_indicator s_meas, ← setIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)
  (∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ)
Tactic: rw [setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
⊢ ∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ = μ.real (t ∩ s) • e
have rw : (μ.restrict s).real t • e = μ.real (t ∩ s) • e
Tactic: rw [integral_indicator_const _ ht, measureReal_restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
rw : (μ.restrict s).real t • e = μ.real (t ∩ s) • e
⊢ ∫ (x : X) in s, t.indicator (fun (x : X) ↦ e) x ∂μ = μ.real (t ∩ s) • e
have rw₁ : μ.real (t ∩ s) • e = μ.real (t ∩ s) • e
Tactic: rw [integral_indicator_const _ ht, measureReal_restrict_apply ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
    (∫ (x : X) in univ, (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
  (∫ (x : X), (↑(↑(indicatorConstLp (s := t) p ht hμt e) : X →ₘ[μ] E) : X → E) x ∂μ)
Tactic: rw [setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : Set X
μ : Measure X
inst_2 : CompleteSpace E
p : ℝ≥0∞
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
e : E
⊢ μ.real (t ∩ univ) • e = μ.real t • e
have rw : μ.real t • e = μ.real t • e
Tactic: rw [inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst_2 : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable (m₀ := inst_2) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ inst_2 (Measure.restrict (Measure.map g μ) s) fun (y : Y) ↦ f y)
    (∫ (x : X) in g ⁻¹' s, f (g x) ∂μ)
have rw : LE.le (α := Measure Y) (Measure.map g (μ.restrict (g ⁻¹' s))) (Measure.map g μ)
Tactic: rw [Measure.restrict_map_of_aemeasurable hg hs,
    integral_map (hg.mono_measure Measure.restrict_le_self) (hf.mono_measure _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x : MeasurableSpace Y
f : X → Y
hf : MeasurableEmbedding f
g : Y → E
s : Set Y
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.restrict (Measure.map f μ) s) fun (y : Y) ↦ g y)
    (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.map f (μ.restrict (f ⁻¹' s))) fun (y : Y) ↦ g y)
  (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
Tactic: rw [hf.restrict_map, hf.integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
x : MeasurableSpace Y
f : X → Y
hf : MeasurableEmbedding f
g : Y → E
s : Set Y
rw :
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.map f (μ.restrict (f ⁻¹' s))) fun (y : Y) ↦ g y)
    (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ x (Measure.restrict (Measure.map f μ) s) fun (y : Y) ↦ g y)
    (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ) (∫ (x : X) in f ⁻¹' s, g (f x) ∂μ)
Tactic: rw [hf.restrict_map, hf.integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have hs₁ : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Measure.restrict_apply_univ] at *
Cleared hypotheses: hs, hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have this : IsFiniteMeasure (μ.restrict s)
Tactic: haveI : IsFiniteMeasure (μ.restrict s) := ⟨hs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have pos : ∀ (hfm : AEStronglyMeasurable f (μ.restrict s)), norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
Tactic: by_cases hfm : AEStronglyMeasurable f (μ.restrict s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
pos : ∀ (hfm : AEStronglyMeasurable f (μ.restrict s)), norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have neg : ∀ (hfm : ¬AEStronglyMeasurable f (μ.restrict s)), norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
Tactic: by_cases hfm : AEStronglyMeasurable f (μ.restrict s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s
have pos : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
Tactic: apply norm_setIntegral_le_of_norm_le_const_ae hs