awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw : lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ lintegral (restrict (const α c) 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 [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
⊢ f.lintegral μ ≤ g.lintegral μ
have refine : ∀ (f g : α →ₛ ℝ≥0∞),
  LE.le (α := ℝ≥0∞) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) f) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) (f ⊔ g))
Tactic: refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
⊢ f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ
have rw : f.lintegral μ = f.lintegral μ
Tactic: rw [map_fst_pair]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
⊢ (map Prod.fst (f.pair g)).lintegral μ ≤ lintegral (map (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ max p.1 p.2) (f.pair g)) μ
have simp : LE.le (α := ℝ≥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∞) (max x.1 x.2)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
Tactic: simp only [map_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
⊢ LE.le (α := ℝ≥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∞) (max x.1 x.2)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
have h₁ : ∀ i ∈ (f.pair g).range, i.1 ≤ max i.1 i.2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) f) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) (f ⊔ g))
have μ₁ : f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ
Tactic: calc
    f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
μ₁ : f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) f) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) (f ⊔ g))
have μ₂ : (map Prod.fst (f.pair g)).lintegral μ ≤ lintegral (map (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ max p.1 p.2) (f.pair g)) μ
Tactic: calc
    f.lintegral μ = ((pair f g).map Prod.fst).lintegral μ := by rw [map_fst_pair]
    _ ≤ ((pair f g).map fun p ↦ p.1 ⊔ p.2).lintegral μ := by
      simp only [map_lintegral]
      gcongr
      exact le_sup_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H :
  ∀ (y : ℝ≥0∞),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) {y}) : ℝ≥0∞)
⊢ f.lintegral μ = g.lintegral ν
have simp : Eq (α := ℝ≥0∞)
  (∑ x ∈ f.range,
    HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
  (∑ x ∈ g.range,
    HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
Tactic: simp only [lintegral, ← H]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H :
  ∀ (y : ℝ≥0∞),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) {y}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ g.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
have 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∞) g.range ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: apply lintegral_eq_of_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
ν : Measure β
H :
  ∀ (y : ℝ≥0∞),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) {y}) : ℝ≥0∞)
⊢ ∀ (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∞) g.range ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
have hs : ∀ (x : α),
  Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
    Ne (α := ℝ≥0∞)
        ((ν : (a : Set β) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
          ℝ≥0∞)
        (0 : ℝ≥0∞) →
      Membership.mem (α := ℝ≥0∞) g.range ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: simp only [H]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((g : (a : β) → ℝ≥0∞) (m' a) : ℝ≥0∞)
h :
  ∀ (s : Set β),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ' : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (m' ⁻¹' s) : ℝ≥0∞)
y : ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
    ((μ' : (a : Set β) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) {y}) : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      {x : α | Membership.mem (α := ℝ≥0∞) (γ := Set ℝ≥0∞) {y} ((g : (a : β) → ℝ≥0∞) (m' x) : ℝ≥0∞)} :
    ℝ≥0∞)
  ((μ' : (a : Set β) → ℝ≥0∞) {x : β | Membership.mem (α := ℝ≥0∞) (γ := Set ℝ≥0∞) {y} ((g : (a : β) → ℝ≥0∞) x : ℝ≥0∞)} :
    ℝ≥0∞)
Tactic: simp only [preimage, eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet.{u_1} (α := α) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β))
have rw : MeasurableSet.{u_1} (α := α) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y})
Tactic: rw [f.support_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [support_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine : ∀ (y : β) (hy : y ∈ {y ∈ f.range | y ≠ 0}),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
y : β
hy : y ∈ {y ∈ f.range | y ≠ 0}
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hy₁ : y ∈ f.range ∧ y ≠ 0
Tactic: rw [Finset.mem_filter] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: classical
  rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ rw₂ :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₃ : ∀ (y : β) (hy : y ∈ {y ∈ f.range | y ≠ 0}),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: classical
  rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
hf :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw rw₁ rw₂ :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
rw₃ :
  ∀ (y : β) (hy : y ∈ {y ∈ f.range | y ≠ 0}),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₄ : ∀ (y : β) (hy : y ∈ f.range ∧ y ≠ 0),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: classical
  rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ ↔
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have mp : f.FinMeasSupp μ →
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
mp :
  f.FinMeasSupp μ →
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ ↔
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have mpr : (∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)) →
  f.FinMeasSupp μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ →
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have mp : ∀ (h : f.FinMeasSupp μ) (y : β) (hy : y ≠ 0),
  Subset.{u_1} (α := Set α) (Set.preimage (β := β) (⇑f : (a : α) → β) {y})
    {x : α | (fun (x : α) ↦ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) (0 x : β)) x}ᶜ
Tactic: refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
H :
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ
have mpr : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [finMeasSupp_iff_support, support_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ ↔
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have mp : f.FinMeasSupp μ →
  ∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: classical
  constructor
  · refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h
    exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx
  · intro H
    rw [finMeasSupp_iff_support, support_eq]
    exact measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
mp :
  f.FinMeasSupp μ →
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ ↔
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have mpr : (∀ (y : β),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)) →
  f.FinMeasSupp μ
Tactic: classical
  constructor
  · refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h
    exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx
  · intro H
    rw [finMeasSupp_iff_support, support_eq]
    exact measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f + g).FinMeasSupp μ
have rw : SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 + p.2) (f.pair g)) μ
Tactic: rw [add_eq_map₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f * g).FinMeasSupp μ
have rw : SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 * p.2) (f.pair g)) μ
Tactic: rw [mul_eq_map₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.lintegral μ < ∞
have refine : ∀ (a : ℝ≥0∞) (ha : a ∈ f.range),
  HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
Tactic: refine sum_lt_top.2 fun a ha => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ℝ≥0∞
ha : a ∈ f.range
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
have inl : ∀ (ha : ∞ ∈ f.range),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) <
    ∞
Tactic: rcases eq_or_ne a ∞ with (rfl | ha)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ℝ≥0∞
ha : a ∈ f.range
inl :
  ∀ (ha : ∞ ∈ f.range),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) <
      ∞
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
have inr : ∀ (ha : a ≠ ∞),
  HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
Tactic: rcases eq_or_ne a ∞ with (rfl | ha)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : ∞ ∈ f.range
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) <
    ∞
have hf₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)} : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, Ne, Classical.not_not] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ℝ≥0∞
ha_1 : a ∈ f.range
ha : a ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
have pos : ∀ (ha0 : a = 0),
  HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ℝ≥0∞
ha_1 : a ∈ f.range
ha : a ≠ ∞
pos :
  ∀ (ha0 : a = 0),
    HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
have neg : ∀ (ha0 : ¬a = 0),
  HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
Tactic: by_cases ha0 : a = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
a : ℝ≥0∞
ha_1 : a ∈ f.range
ha : a ≠ ∞
ha0 : a = 0
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
have pos : ∀ (ha : 0 ∈ f.range) (ha : Ne (α := ℝ≥0∞) 0 ∞),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {0}) : ℝ≥0∞) <
    ∞
Tactic: subst a
Cleared hypotheses: a, ha_1, ha, ha0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ
have refine : ∀ (b : ℝ≥0∞) (hb : b ≠ 0),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine finMeasSupp_iff.2 fun b hb => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : Ne (α := ℝ≥0∞)
  (∑ x ∈ insert b (f.range \ {0}),
    HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
  ∞
Tactic: rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h :
  Ne (α := ℝ≥0∞)
    (∑ x ∈ insert b (f.range \ {0}),
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    ∞
hb : b ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ ∞
Tactic: refine ENNReal.lt_top_of_mul_ne_top_right ?_ hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (y : ℝ≥0∞),
  y ≠ 0 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine measure_support_lt_top f ?_