awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
h : μ ≤ ν
⊢ LE.le (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) x ((ν : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
hfg : f ≤ g
hμν : μ ≤ ν
⊢ f.lintegral μ ≤ g.lintegral ν

Tactic:
(lintegral_mono_fun hfg).trans (lintegral_mono_measure hμν)

Premises used: MeasureTheory.SimpleFunc.lintegral_mono_fun, LE.le.trans, MeasureTheory.SimpleFunc.lintegral_mono_measure
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
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∞))
⊢ f.lintegral μ = g.lintegral ν

Tactic:
simp only [lintegral, ← H]

Premises used: MeasureTheory.SimpleFunc.lintegral
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
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∞)
⊢ 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:
apply lintegral_eq_of_subset

Premises used: MeasureTheory.SimpleFunc.lintegral_eq_of_subset
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
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∞)
⊢ ∀ (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:
simp only [H]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 : α
h : Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 :
  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:
mem_range_of_measure_ne_zero ‹_›

Premises used: MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 : α
h : Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 :
  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:
exact mem_range_of_measure_ne_zero ‹_›

Premises used: MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞)
y : ℝ≥0∞
x : α
hx : Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) ((g : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) x ↔
    Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) {y}) x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y}) : ℝ≥0∞)
    ((μ' : (a : Set β) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑g : (a : β) → ℝ≥0∞) {y}) : ℝ≥0∞)

Tactic:
simp only [preimage, eq]

Premises used: Set.preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
        {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:
(h (g ⁻¹' {y}) (g.measurableSet_preimage _)).symm

Premises used: Set.Mem, setOf, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_preimage, Set.singleton, Singleton.singleton, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
        {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:
exact (h (g ⁻¹' {y}) (g.measurableSet_preimage _)).symm

Premises used: Set.preimage, MeasureTheory.SimpleFunc.measurableSet_preimage, Singleton.singleton, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MeasurableSpace β
g : β →ₛ ℝ≥0∞
f : α → β
hf : Measurable f
⊢ g.lintegral (Measure.map f μ) = (g.comp f hf).lintegral μ

Tactic:
Eq.symm <| lintegral_map' _ _ f (fun _ => rfl) fun _s hs => Measure.map_apply hf hs

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.SimpleFunc.lintegral_map', Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Zero β
f : α →ₛ β
x : α
⊢ Membership.mem (γ := Set α) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) x ↔
    Membership.mem (γ := Set α) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) x

Tactic:
simp only [mem_support, Set.mem_preimage, mem_filter, mem_range_self, true_and, exists_prop,
      mem_iUnion, mem_singleton_iff, exists_eq_right']

Premises used: exists_eq_right', Set.mem_iUnion, exists_prop, Set.mem_singleton_iff, Function.mem_support, Finset.mem_filter, MeasureTheory.SimpleFunc.mem_range_self, Set.mem_preimage, true_and
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : MeasurableSpace α
f : α →ₛ β
rw : MeasurableSet.{u_1} (α := α) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y})
⊢ MeasurableSet.{u_1} (α := α) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β))

Tactic:
rw [f.support_eq]

Premises used: MeasureTheory.SimpleFunc.support_eq
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet.{u_1} (α := α) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y})

Tactic:
Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _

Premises used: MeasureTheory.SimpleFunc.measurableSet_fiber, Finset.measurableSet_biUnion
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : MeasurableSpace α
f : α →ₛ β
⊢ MeasurableSet.{u_1} (α := α) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y})

Tactic:
exact Finset.measurableSet_biUnion _ fun y _ => measurableSet_fiber _ _

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

Tactic:
rw [support_eq]

Premises used: MeasureTheory.SimpleFunc.support_eq
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)

Tactic:
(measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)

Premises used: Iff.mpr, ENNReal.sum_lt_top, MeasureTheory.measure_biUnion_finset_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
refine :
  ∀ (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∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)

Premises used: Iff.mpr, ENNReal.sum_lt_top, MeasureTheory.measure_biUnion_finset_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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}
⊢ y ∈ f.range ∧ y ≠ 0

Tactic:
rw [Finset.mem_filter] at hy

Premises used: Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 ∈ f.range ∧ y ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hf y hy.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 ∈ f.range ∧ y ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hf y hy.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
rw₄ :
  ∀ (y : β) (hy : 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∞)

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

Premises used: Iff.mpr, ENNReal.sum_lt_top, MeasureTheory.measure_biUnion_finset_le, Finset.mem_filter, MeasureTheory.SimpleFunc.support_eq, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
⊢ f.FinMeasSupp μ ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑f : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.Eventually, Iff.rfl, setOf, MeasureTheory.SimpleFunc.FinMeasSupp, Filter.EventuallyEq, Function.support
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
mpr :
  (∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)) →
    f.FinMeasSupp μ
⊢ f.FinMeasSupp μ ↔
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)

Tactic:
fun h y hy => lt_of_le_of_lt (measure_mono ?_) h

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
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}ᶜ
⊢ f.FinMeasSupp μ →
    ∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
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:
fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx

Premises used: Set.Mem, setOf, Eq.rec, Set.Subset, Eq.symm, Not
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
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:
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
mpr :
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ f.FinMeasSupp μ

Tactic:
rw [finMeasSupp_iff_support, support_eq]

Premises used: MeasureTheory.SimpleFunc.support_eq, MeasureTheory.SimpleFunc.finMeasSupp_iff_support
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2

Premises used: MeasureTheory.measure_biUnion_lt_top, And.right, Iff.mp, Finset.mem_filter, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ {y ∈ f.range | y ≠ 0}, Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2

Premises used: MeasureTheory.measure_biUnion_lt_top, And.right, Iff.mp, Finset.mem_filter, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
mpr mpr₁ :
  (∀ (y : β),
      y ≠ 0 →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)) →
    f.FinMeasSupp μ
⊢ 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

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, MeasureTheory.SimpleFunc.support_eq, MeasureTheory.SimpleFunc.finMeasSupp_iff_support
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Zero β
μ : Measure α
f : α →ₛ β
h : f.FinMeasSupp μ
y : β
hy : y ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := β) (⇑f : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finMeasSupp_iff.1 h y hy

Premises used: Iff.mp, MeasureTheory.SimpleFunc.finMeasSupp_iff
-- 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 0 = 0
⊢ (map g f).FinMeasSupp μ

Tactic:
flip lt_of_le_of_lt hf (measure_mono <| support_comp_subset hg f)

Premises used: Function.support_comp_subset, flip, MeasureTheory.measure_mono, DFunLike.coe
-- 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 : β → γ
h : (map g f).FinMeasSupp μ
hg : ∀ (b : β), g b = 0 → b = 0
⊢ f.FinMeasSupp μ

Tactic:
flip lt_of_le_of_lt h <| measure_mono <| support_subset_comp @hg _

Premises used: flip, MeasureTheory.measure_mono, Function.support_subset_comp
-- 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 : β → γ
hg : ∀ {b : β}, g b = 0 ↔ b = 0
⊢ (map g f).FinMeasSupp μ ↔ f.FinMeasSupp μ

Tactic:
⟨fun h => h.of_map fun _ => hg.1, fun h => h.map <| hg.2 rfl⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp, MeasureTheory.SimpleFunc.FinMeasSupp.of_map, MeasureTheory.SimpleFunc.FinMeasSupp.map, rfl