awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ f.range with g i = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {i}) : ℝ≥0∞))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞))
have refine_1 : {b ∈ f.range | g b = g ((f : (a : α) → β) a)} = {j ∈ f.range | g j = g ((f : (a : α) → β) a)}
Tactic: refine Finset.sum_congr ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
refine_1 : {b ∈ f.range | g b = g ((f : (a : α) → β) a)} = {j ∈ f.range | g j = g ((f : (a : α) → β) a)}
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ f.range with g i = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {i}) : ℝ≥0∞))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞))
have refine_2 : ∀ x ∈ {j ∈ f.range | g j = g ((f : (a : α) → β) a)},
  HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞)
Tactic: refine Finset.sum_congr ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ (f + g).lintegral μ =
    ∑ x ∈ (f.pair g).range,
      (HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
have rw : Eq (α := ℝ≥0∞)
  (∑ x ∈ (f.pair g).range,
    HMul.hMul (β := ℝ≥0∞) (x.1 + x.2)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
  (∑ x ∈ (f.pair g).range,
    (HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)))
Tactic: rw [add_eq_map₂, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x ∈ (f.pair g).range,
      (HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥0∞)
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
have rw : HAdd.hAdd (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
  HAdd.hAdd (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
Tactic: rw [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ
have rw : HAdd.hAdd (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
  ∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
    (map Prod.snd (f.pair g)).lintegral μ
Tactic: rw [map_lintegral, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
rw :
  HAdd.hAdd (α := ℝ≥0∞)
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    ∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
      (map Prod.snd (f.pair g)).lintegral μ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
      (∑ x ∈ (f.pair g).range,
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ
have rw₁ : HAdd.hAdd (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
  HAdd.hAdd (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.1
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) x.2
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
Tactic: rw [map_lintegral, map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
x : ℝ≥0∞
⊢ ∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (x * r) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) =
    x *
      ∑ r ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  (∑ r ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (x * r) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
  (∑ i ∈ f.range,
    x * HMul.hMul (β := ℝ≥0∞) i ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {i}) : ℝ≥0∞))
Tactic: simp_rw [Finset.mul_sum, mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)
have simp : Eq (α := ℝ≥0∞)
  (∑' (x : ↥f.range) (i : ι),
    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
      ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))
  (∑' (i : ι) (x : ↥f.range),
    HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
      ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))
Tactic: simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
    ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(f.restrict s) : (a : α) → ℝ≥0∞)
            (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (s ∩ preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
      ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
      ℝ≥0∞)
Tactic: rw [restrict_preimage_singleton _ hs hb, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (s ∩ preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(f.restrict s) : (a : α) → ℝ≥0∞)
            (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
      ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
      ℝ≥0∞)
Tactic: rw [restrict_preimage_singleton _ hs hb, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
have rw : ∑ r ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r} ∩ s) : ℝ≥0∞) =
  f.lintegral (μ.restrict s)
Tactic: rw [f.restrict_lintegral hs, lintegral_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw :
  ∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r} ∩ s) : ℝ≥0∞) =
    f.lintegral (μ.restrict s)
⊢ (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
have rw₁ : Eq (α := ℝ≥0∞)
  (∑ r ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r} ∩ s) : ℝ≥0∞))
  (∑ y ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))
Tactic: rw [f.restrict_lintegral hs, lintegral_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
⊢ f.lintegral (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), f.lintegral (μ.restrict (s i))
have simp : Eq (α := ℝ≥0∞)
  (∑ x ∈ f.range,
    ⨆ (i : ι),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
  (⨆ (i : ι),
    ∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
Tactic: simp only [lintegral, Measure.restrict_iUnion_apply_eq_iSup hd (measurableSet_preimage ..),
    ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      ⨆ (i : ι),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (⨆ (i : ι),
      ∑ x ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
have refine : ∀ (i j k : ι),
  (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k) →
    ∀ (hik : s i ⊆ s k) (hjk : s j ⊆ s k) (a : ℝ≥0∞),
      HMul.hMul (β := ℝ≥0∞) a
            ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
          HMul.hMul (β := ℝ≥0∞) a
            ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ∧
        HMul.hMul (β := ℝ≥0∞) a
            ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
          HMul.hMul (β := ℝ≥0∞) a
            ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
Tactic: refine finsetSum_iSup fun i j ↦ (hd i j).imp fun k ⟨hik, hjk⟩ ↦ fun a ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
h : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ∧
    HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
have left : HMul.hMul (β := ℝ≥0∞) a
    ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) a
    ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
h : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
left :
  HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ∧
    HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
have right : HMul.hMul (β := ℝ≥0∞) a
    ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) a
    ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inl : IsEmpty α →
  ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
inl :
  IsEmpty α →
    ∑ x ∈ SimpleFunc.range (const α c),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : Nonempty α →
  ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (Function.const α c ⁻¹' {c}) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp only [range_const, coe_const, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (Function.const α c ⁻¹' {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (fun (x : α) ↦ c) {c}) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: unfold Function.const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (fun (x : α) ↦ c) {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [preimage_const_of_mem (mem_singleton c)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
rw :
  HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
rw :
  HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₂ : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ lintegral (restrict (const α c) s) μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]