awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ LT.lt (α := ℝ≥0∞)
    ((Finset.range n).sup fun (c : ℕ) ↦
      ((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed c ≤ f a} then
              piecewise {a : α | ennrealRatEmbed c ≤ f a} hs (const α (ennrealRatEmbed c)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a)
    ∞
have rw : ∀ b ∈ Finset.range n,
  LT.lt (α := ℝ≥0∞)
    (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
              piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a :
      ℝ≥0∞)
    (⊤ : WithTop ℝ≥0)
Tactic: rw [Finset.sup_lt_iff (α := ℝ≥0∞) WithTop.top_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
⊢ LT.lt (α := ℝ≥0∞)
    (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
              piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a :
      ℝ≥0∞)
    (⊤ : WithTop ℝ≥0)
have pos : ∀ (h : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}),
  LT.lt (α := ℝ≥0∞)
    ((piecewise {a : α | ennrealRatEmbed b ≤ f a} h (const α (ennrealRatEmbed b)) 0 : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (⊤ : WithTop ℝ≥0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
b : ℕ
h : b ∈ Finset.range n
pos :
  ∀ (h : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a}),
    LT.lt (α := ℝ≥0∞)
      ((piecewise {a : α | ennrealRatEmbed b ≤ f a} h (const α (ennrealRatEmbed b)) 0 : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (⊤ : WithTop ℝ≥0)
⊢ LT.lt (α := ℝ≥0∞)
    (((if hs : MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} then
              piecewise {a : α | ennrealRatEmbed b ≤ f a} hs (const α (ennrealRatEmbed b)) 0
            else 0 :
            α →ₛ ℝ≥0∞) :
          (a : α) → ℝ≥0∞)
        a :
      ℝ≥0∞)
    (⊤ : WithTop ℝ≥0)
have neg : ¬MeasurableSet.{u_1} (α := α) {a : α | ennrealRatEmbed b ≤ f a} →
  LT.lt (α := ℝ≥0∞) (((0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (⊤ : WithTop ℝ≥0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a = f a
have rw : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a
Tactic: rw [eapprox, iSup_approx_apply ennrealRatEmbed f a hf rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a
have refine : ¬⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
Tactic: refine le_antisymm (iSup_le fun i => iSup_le fun hi => hi) (le_of_not_gt ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
⊢ False
have rcases : ∀ (q : ℚ),
  0 ≤ q →
    ∀ (lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞))
      (q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a), False
Tactic: rcases ENNReal.lt_iff_exists_rat_btwn.1 h with ⟨q, _, lt_q, q_lt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
have refine : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
  ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
Tactic: refine le_iSup_of_le (Encodable.encode q) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
    ⨆ (_ : ennrealRatEmbed (Encodable.encode q) ≤ f a), ennrealRatEmbed (Encodable.encode q)
have rw : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤
  ⨆ (_ : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ f a), (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
Tactic: rw [ennrealRatEmbed_encode q]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
h : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < f a
q : ℚ
left : 0 ≤ q
lt_q : ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞)
q_lt : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) < f a
⊢ False
have this : (↑(Real.toNNReal (↑q : ℝ)) : ℝ≥0∞) ≤ ⨆ (k : ℕ), ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
Tactic: have :
    (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ (k : ℕ) (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k := by
    refine le_iSup_of_le (Encodable.encode q) ?_
    rw [ennrealRatEmbed_encode q]
    exact le_iSup_of_le (le_of_lt q_lt) le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop (𝓝 (f a))
have nth_rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
  (𝓝 ((⨆ (n : ℕ), (⇑(eapprox f n) : (a : α) → ℝ≥0∞)) a))
Tactic: nth_rw 2 [← iSup_coe_eapprox hf_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
    (𝓝 ((⨆ (n : ℕ), (⇑(eapprox f n) : (a : α) → ℝ≥0∞)) a))
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) atTop
  (𝓝 (⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a))
Tactic: rw [iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1 + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
have succ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≠
  ∞
Tactic: rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≠
    ∞
have apply : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
  ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
Tactic: apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
a : α
n : ℕ
IH :
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
have rw : ((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: rw [tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
⊢ Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
have zero : Eq (α := ℝ≥0∞)
  (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
  (((eapprox f 0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: induction n with
  | zero =>
    simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]
  | succ n IH =>
    rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
    apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
    rw [tsub_le_iff_right]
    exact le_self_add
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
n : ℕ
a : α
zero :
  Eq (α := ℝ≥0∞)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f 0 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
have succ : ∀ (n : ℕ)
  (IH :
    Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
      (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1 + 1), (↑(((eapproxDiff f k : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) : ℝ≥0∞)
    (((eapprox f (n + 1) : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: induction n with
  | zero =>
    simp [eapproxDiff, (eapprox_lt_top f 0 a).ne]
  | succ n IH =>
    rw [Finset.sum_range_succ, IH, eapproxDiff, coe_map, Function.comp_apply,
      coe_sub, Pi.sub_apply, ENNReal.coe_toNNReal,
      add_tsub_cancel_of_le (monotone_eapprox f (Nat.le_succ _) _)]
    apply (lt_of_le_of_lt _ (eapprox_lt_top f (n + 1) a)).ne
    rw [tsub_le_iff_right]
    exact le_self_add
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a
have simp_rw : ⨆ (i : ℕ), ∑ n ∈ Finset.range (i + 1), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a
Tactic: simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
    iSup_eapprox_apply hf a]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
simp_rw : ⨆ (i : ℕ), ∑ n ∈ Finset.range (i + 1), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a
⊢ ∑' (n : ℕ), (↑(((eapproxDiff f n : α →ₛ ℝ≥0) : (a : α) → ℝ≥0) a) : ℝ≥0∞) = f a
have simp_rw₁ : ⨆ (i : ℕ), ((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a = f a
Tactic: simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
    iSup_eapprox_apply hf a]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)
have refine_1 : ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range)
  (h₂ : HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
  (fun (r : ℝ≥0∞) (x : r ∈ f.range)
          (x_1 :
            HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
              0) ↦
        r)
      a h₁ h₂ ∈
    s
Tactic: refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
refine_1 :
  ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range)
    (h₂ :
      HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ ∈
      s
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)
have refine_2 : ∀ (a₁ : ℝ≥0∞) (h₁₁ : a₁ ∈ f.range)
  (h₁₂ :
    HMul.hMul (β := ℝ≥0∞) a₁ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₁}) : ℝ≥0∞) ≠ 0)
  (a₂ : ℝ≥0∞) (h₂₁ : a₂ ∈ f.range)
  (h₂₂ :
    HMul.hMul (β := ℝ≥0∞) a₂ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₂}) : ℝ≥0∞) ≠ 0),
  Eq (α := ℝ≥0∞)
      ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a₁ h₁₁ h₁₂)
      ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a₂ h₂₁ h₂₂) →
    a₁ = a₂
Tactic: refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
refine_1 :
  ∀ (a : ℝ≥0∞) (h₁ : a ∈ f.range)
    (h₂ :
      HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ ∈
      s
refine_2 :
  ∀ (a₁ : ℝ≥0∞) (h₁₁ : a₁ ∈ f.range)
    (h₁₂ :
      HMul.hMul (β := ℝ≥0∞) a₁ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₁}) : ℝ≥0∞) ≠ 0)
    (a₂ : ℝ≥0∞) (h₂₁ : a₂ ∈ f.range)
    (h₂₂ :
      HMul.hMul (β := ℝ≥0∞) a₂ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₂}) : ℝ≥0∞) ≠ 0),
    Eq (α := ℝ≥0∞)
        ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
              (x_1 :
                HMul.hMul (β := ℝ≥0∞) r
                    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                  0) ↦
            r)
          a₁ h₁₁ h₁₂)
        ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
              (x_1 :
                HMul.hMul (β := ℝ≥0∞) r
                    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                  0) ↦
            r)
          a₂ h₂₁ h₂₂) →
      a₁ = a₂
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)
have refine_3 : ∀ b ∈ s,
  HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0 →
    ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
      HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
      (fun (r : ℝ≥0∞) (x : r ∈ f.range)
              (x_1 :
                HMul.hMul (β := ℝ≥0∞) r
                    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                  0) ↦
            r)
          a h₁ h₂ =
        b
Tactic: refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
⊢ ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
    HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ =
      b
have refine_3 : b ∈ f.range
Tactic: refine ⟨b, ?_, hb, rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
⊢ b ∈ f.range
have refine_3 : Set.Nonempty (α := α) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b})
Tactic: rw [mem_range, ← preimage_singleton_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ (map g f).lintegral μ =
    ∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  (∑ x ∈ Finset.image g f.range,
    HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
  (∑ x ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞))
Tactic: simp only [lintegral, range_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ Finset.image g f.range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞))
have refine : ∀ (b : β) (hb : b ∈ f.range),
  HMul.hMul (β := ℝ≥0∞) (g b)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g b}) : ℝ≥0∞) =
    ∑ j ∈ f.range with g j = g b,
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)
Tactic: refine Finset.sum_image' _ fun b hb => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ f.range
⊢ HMul.hMul (β := ℝ≥0∞) (g b)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g b}) : ℝ≥0∞) =
    ∑ j ∈ f.range with g j = g b,
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)
have rcases : ∀ (a : α) (hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)),
  HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g ((f : (a : α) → β) a)}) : ℝ≥0∞) =
    ∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)
Tactic: rcases mem_range.1 hb with ⟨a, rfl⟩
Cleared hypotheses: b, hb
-- 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 : β)
⊢ HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g ((f : (a : α) → β) a)}) : ℝ≥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 rw : 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∞))
Tactic: rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]