awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_3 : NormedSpace ℝ E
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ = C * integral μ (map norm f)
have rw : C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ =
  C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) • ‖x‖
Tactic: rw [map_integral f norm hf norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ ‖integral μ f‖ ≤ integral μ (map norm f)
have refine : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      norm.{u_2} (E := E →L[ℝ] E) (weightedSMul μ s) ≤ 1 * μ.real s
Tactic: refine (norm_setToSimpleFunc_le_integral_norm _ (fun s _ _ => ?_) hf).trans (one_mul _).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
⊢ integral (μ + ν) f = integral μ f + integral ν f
have simp_rw : setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
Tactic: simp_rw [integral_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
have refine : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (hμνs : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      weightedSMul (μ + ν) s = HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
Tactic: refine setToSimpleFunc_add_left'
    (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
s : Set α
h : MeasurableSet s
hμνs : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
have hμνs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs
Cleared hypotheses: hμνs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) (μ + ν)
s : Set α
h : MeasurableSet s
hμνs :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
have rw : HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s) =
  HAdd.hAdd (α := E →L[ℝ] E) (weightedSMul μ s) (weightedSMul ν s)
Tactic: rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
⊢ 0 ≤ integral μ f
have rw : LE.le (α := F) 0 (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
Tactic: rw [integral_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
⊢ LE.le (α := F) 0 (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
have h : ∀ i ∈ f.range, 0 ≤ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
Tactic: apply Finset.sum_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
⊢ ∀ i ∈ f.range, 0 ≤ μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
have h : ∀ (x : α),
  0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: rw [forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)
have pos : ∀ (hy : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)),
  0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)
Tactic: by_cases hy : 0 ≤ f y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
pos :
  ∀ (hy : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)),
    0 ≤
      HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
        ((f : (a : α) → F) y : F)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)
have neg : ∀ (hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)),
  0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)
Tactic: by_cases hy : 0 ≤ f y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
⊢ 0 ≤
    HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))))
      ((f : (a : α) → F) y : F)
have neg : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: suffices μ (f ⁻¹' {f y}) = 0 by simp [this, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : LE.le (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : ∀ (x : α)
  (hx :
    Membership.mem (γ := Set α)
      (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F))) x),
  Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} x
Tactic: refine le_of_le_of_eq (measure_mono fun x hx ↦ ?_) (ae_iff.mp hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae μ) 0 (⇑f : (a : α) → F)
y : α
hy : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) y : F)
x : α
hx :
  Membership.mem (γ := Set α) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) y : F)))
    x
⊢ Membership.mem (γ := Set α) {a : α | ¬LE.le.{u_3} (α := F) (0 a : F) ((f : (a : α) → F) a : F)} x
have hx₁ : Eq.{u_3 + 1} (α := F) ((f : (a : α) → F) x : F) ((f : (a : α) → F) y : F)
Tactic: simp only [Set.mem_preimage, mem_singleton_iff, mem_setOf_eq] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f g : α →ₛ F
h : EventuallyLE.{u_1, u_3} (β := F) (ae μ) (⇑f : (a : α) → F) (⇑g : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
⊢ integral μ f ≤ integral μ g
have rw : 0 ≤ integral μ (g - f)
Tactic: rw [← sub_nonneg, ← integral_sub hg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
f g : α →ₛ F
h : EventuallyLE.{u_1, u_3} (β := F) (ae μ) (⇑f : (a : α) → F) (⇑g : (a : α) → F)
hf : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) μ
hg : Integrable.{u_3, u_1} (ε := F) (⇑g : (a : α) → F) μ
⊢ 0 ≤ integral μ (g - f)
have h₁ : 0 ≤ᶠ[ae μ] HSub.hSub (α := α → F) (⇑g : (a : α) → F) (⇑f : (a : α) → F)
Tactic: rw [← sub_nonneg_ae] at h
Cleared hypotheses: h, hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
⊢ integral μ f ≤ integral ν f
have simp : LE.le (α := F) (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
  (∑ x ∈ f.range, ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
Tactic: simp only [integral_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
⊢ LE.le (α := F) (∑ x ∈ f.range, μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
    (∑ x ∈ f.range, ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) • x)
have h : ∀ i ∈ f.range,
  μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i ≤ ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
Tactic: apply Finset.sum_le_sum
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
⊢ ∀ i ∈ f.range,
    μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i ≤
      ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) {i}) • i
have h : ∀ (x : α),
  HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: simp only [forall_mem_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have pos : ∀ (hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
  HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: by_cases hx : 0 ≤ f x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
pos :
  ∀ (hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have neg : ∀ (hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
  HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: by_cases hx : 0 ≤ f x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have pos : ∀ (hx : Eq.{u_3 + 1} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
  HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: obtain (hx | hx) := hx.eq_or_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
pos :
  ∀ (hx : Eq.{u_3 + 1} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
    HSMul.hSMul (β := F)
        (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F) ≤
      HSMul.hSMul (β := F)
        (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
        ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have pos₁ : ∀ (hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)),
  HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
Tactic: obtain (hx | hx) := hx.eq_or_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have pos : HSMul.hSMul (β := F)
    (ENNReal.toReal
      ((μ : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
    ((f : (a : α) → F) x : F) ≤
  HSMul.hSMul (β := F)
    (ENNReal.toReal
      ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
    ((f : (a : α) → F) x : F)
Tactic: simp only [measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (goal)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx_1 : LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
hx : LT.lt.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
⊢ HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((μ : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ENNReal.toReal
        ((ν : (a : Set α) → ℝ≥0∞)
          (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F)))))
      ((f : (a : α) → F) x : F)
have pos : Ne (α := ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.L1 (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder F
inst_3 : IsOrderedAddMonoid F
inst_4 : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : EventuallyLE.{u_1, u_3} (β := F) (ae ν) 0 (⇑f : (a : α) → F)
hμν : μ ≤ ν
hfν : Integrable.{u_3, u_1} (ε := F) (⇑f : (a : α) → F) ν
x : α
hx : ¬LE.le.{u_3} (α := F) (0 : F) ((f : (a : α) → F) x : F)
this :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HSMul.hSMul (β := F)
      (μ.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F) ≤
    HSMul.hSMul (β := F)
      (ν.real (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))))
      ((f : (a : α) → F) x : F)
have A : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := F) (⇑f : (a : α) → F) (singleton (α := F) ((f : (a : α) → F) x : F))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)