awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : Zero β
inst_1 : Zero γ
μ : Measure α
f : α →ₛ β
g : α →ₛ γ
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f.pair g).FinMeasSupp μ

Tactic:
calc
    μ (support <| pair f g) = μ (support f ∪ support g) := congr_arg μ <| support_prodMk f g
    _ ≤ μ (support f) + μ (support g) := measure_union_le _ _
    _ < _ := add_lt_top.2 ⟨hf, hg⟩

Premises used: Iff.mpr, Trans.trans, Set.Mem, Filter.Eventually, setOf, MeasureTheory.SimpleFunc.FinMeasSupp, Filter.EventuallyEq, Function.support_prodMk, congr_arg, Function.support, And.intro, ENNReal.add_lt_top, DFunLike.coe, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m : MeasurableSpace α
inst : Zero β
inst_1 : Zero γ
μ : Measure α
f : α →ₛ β
inst_2 : Zero δ
hf : f.FinMeasSupp μ
g : α →ₛ γ
hg : g.FinMeasSupp μ
op : β → γ → δ
H : op 0 0 = 0
⊢ (map (uncurry op) (f.pair g)).FinMeasSupp μ

Tactic:
(hf.pair hg).map H

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.map, MeasureTheory.SimpleFunc.FinMeasSupp.pair
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
rw : SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 + p.2) (f.pair g)) μ
⊢ (f + g).FinMeasSupp μ

Tactic:
rw [add_eq_map₂]

Premises used: MeasureTheory.SimpleFunc.add_eq_map₂
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 + p.2) (f.pair g)) μ

Tactic:
hf.map₂ hg (zero_add 0)

Premises used: zero_add, MeasureTheory.SimpleFunc.FinMeasSupp.map₂, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : AddZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 + p.2) (f.pair g)) μ

Tactic:
exact hf.map₂ hg (zero_add 0)

Premises used: zero_add, MeasureTheory.SimpleFunc.FinMeasSupp.map₂, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
rw : SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 * p.2) (f.pair g)) μ
⊢ (f * g).FinMeasSupp μ

Tactic:
rw [mul_eq_map₂]

Premises used: MeasureTheory.SimpleFunc.mul_eq_map₂
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 * p.2) (f.pair g)) μ

Tactic:
hf.map₂ hg (zero_mul 0)

Premises used: MulZeroClass.zero_mul, MeasureTheory.SimpleFunc.FinMeasSupp.map₂, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MulZeroClass β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ SimpleFunc.FinMeasSupp (β := β) (map (fun (p : β × β) ↦ p.1 * p.2) (f.pair g)) μ

Tactic:
exact hf.map₂ hg (zero_mul 0)

Premises used: MulZeroClass.zero_mul, MeasureTheory.SimpleFunc.FinMeasSupp.map₂, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.lintegral μ < ∞

Tactic:
sum_lt_top.2 fun a ha => ?_

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.lintegral, ENNReal.sum_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∀ (a : ℝ≥0∞) (ha : a ∈ f.range),
    HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞
⊢ f.lintegral μ < ∞

Tactic:
refine sum_lt_top.2 fun a ha => ?_

Premises used: Iff.mpr, ENNReal.sum_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞) <
      ∞
inr :
  ∀ (ha : a ≠ ∞),
    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∞) < ∞

Tactic:
rcases eq_or_ne a ∞ with (rfl | ha)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ 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

Premises used: Classical.not_not, Ne, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
ha : ∞ ∈ f.range
hf :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {∞}) : ℝ≥0∞) <
    ∞

Tactic:
simp [Set.preimage, hf]

Premises used: Set.preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞) < ∞
neg :
  ∀ (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∞) < ∞

Tactic:
by_cases ha0 : a = 0
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
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∞) <
      ∞
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) < ∞

Tactic:
subst a
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hm : f.FinMeasSupp μ
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
ha_1 : 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:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞) < ∞

Tactic:
mul_lt_top ha.lt_top (finMeasSupp_iff.1 hm _ ha0)

Premises used: ENNReal.mul_lt_top, Ne.lt_top, Iff.mp, MeasureTheory.SimpleFunc.finMeasSupp_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞) < ∞

Tactic:
exact mul_lt_top ha.lt_top (finMeasSupp_iff.1 hm _ ha0)

Premises used: ENNReal.mul_lt_top, Ne.lt_top, Iff.mp, MeasureTheory.SimpleFunc.finMeasSupp_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ

Tactic:
finMeasSupp_iff.2 fun b hb => ?_

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.finMeasSupp_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
refine :
  ∀ (b : ℝ≥0∞) (hb : b ≠ 0),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ

Tactic:
refine finMeasSupp_iff.2 fun b hb => ?_

Premises used: Iff.mpr, MeasureTheory.SimpleFunc.finMeasSupp_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
b : ℝ≥0∞
hb : b ≠ 0
⊢ 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

Premises used: MeasureTheory.SimpleFunc.lintegral_eq_of_subset', Finset.subset_insert
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ∞
b : ℝ≥0∞
hb : 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∞))
    ∞
⊢ b ≠ 0

Tactic:
rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h

Premises used: MeasureTheory.SimpleFunc.lintegral_eq_of_subset', Finset.subset_insert
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)

Tactic:
ENNReal.lt_top_of_mul_ne_top_right ?_ hb

Premises used: ENNReal.lt_top_of_mul_ne_top_right
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
refine :
  HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ENNReal.lt_top_of_mul_ne_top_right ?_ hb

Premises used: ENNReal.lt_top_of_mul_ne_top_right
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ ∞

Tactic:
(lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne

Premises used: Finset.mem_insert_self, ENNReal.lt_top_of_sum_ne_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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
⊢ HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ ∞

Tactic:
exact (lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne

Premises used: Finset.mem_insert_self, ENNReal.lt_top_of_sum_ne_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : ∀ᵐ (a : α) ∂μ, Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ ↔ f.lintegral μ < ∞

Tactic:
⟨fun h => h.lintegral_lt_top hf, fun h => of_lintegral_ne_top h.ne⟩

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top, MeasureTheory.SimpleFunc.FinMeasSupp.lintegral_lt_top, Iff.intro, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)

Tactic:
measure_support_lt_top f ?_

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
refine :
  ∀ (y : ℝ≥0∞),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
        (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine measure_support_lt_top f ?_

Premises used: MeasureTheory.SimpleFunc.measure_support_lt_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
rw : f.FinMeasSupp μ
⊢ ∀ (y : ℝ≥0∞),
    y ≠ 0 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
        (∞ : ℝ≥0∞)

Tactic:
rw [← finMeasSupp_iff]

Premises used: MeasureTheory.SimpleFunc.finMeasSupp_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ

Tactic:
FinMeasSupp.of_lintegral_ne_top hf

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
hf : f.lintegral μ ≠ ∞
⊢ f.FinMeasSupp μ

Tactic:
exact FinMeasSupp.of_lintegral_ne_top hf

Premises used: MeasureTheory.SimpleFunc.FinMeasSupp.of_lintegral_ne_top
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
generalize : ∀ (s : Finset γ) (h : f.range \ {0} = s), motive f
⊢ motive f

Tactic:
generalize h : f.range \ {0} = s

Premises used: MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
s : Finset γ
h : f.range \ {0} = s
⊢ range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)

Tactic:
rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h

Premises used: MeasureTheory.SimpleFunc.coe_range, Finset.coe_singleton, Finset.coe_sdiff, Finset.coe_inj
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑∅ : Set γ)
⊢ Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)

Tactic:
rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h

Premises used: Finset.coe_empty, Set.range_subset_singleton, Set.diff_eq_empty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
⊢ motive (piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0))

Tactic:
const 0 MeasurableSet.univ

Premises used: OfNat.ofNat, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
h₁ : f = piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0)
⊢ motive f

Tactic:
convert! const 0 MeasurableSet.univ

Premises used: OfNat.ofNat, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
h₁ :
  ∀ (x : α),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ)
      ((piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → γ) x : γ)
⊢ f = piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
f : α →ₛ γ
h : Eq (α := α → γ) (⇑f : (a : α) → γ) (Function.const α 0)
x : α
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) x : γ)
    ((piecewise univ ⋯ (SimpleFunc.const α 0) (SimpleFunc.const α 0) : (a : α) → γ) x : γ)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(Insert.insert x s) : Set γ)
insert : ∀ (mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})), motive f
⊢ motive f

Tactic:
have mx := f.measurableSet_preimage {x}
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
h₁ : range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {0} = (↑s : Set γ)
⊢ motive g

Tactic:
apply ih
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add :
  ∀ ⦃f g : α →ₛ γ⦄,
    Disjoint.{u_5} (α := Set α) (support.{u_5, u_6} (M := γ) (⇑f : (a : α) → γ))
        (support.{u_5, u_6} (M := γ) (⇑g : (a : α) → γ)) →
      motive f → motive g → motive (f + g)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑s : Set γ)), motive f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {0} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx 0 f
h₁ :
  (image.{u_5, u_6} (α := α) (⇑0 : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) ∪
        image.{u_5, u_6} (α := α) (⇑f : (a : α) → γ) (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ) \
      {0} =
    (↑s : Set γ)
⊢ range.{u_6, u_5 + 1} (ι := α) (⇑g : (a : α) → γ) \ {0} = (↑s : Set γ)

Tactic:
simp only [g, SimpleFunc.coe_piecewise, range_piecewise]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, Set.range_piecewise