awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m_1 : MeasurableSpace α
μ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
⊢ ∀ (x y : Measure α), f.lintegral (x + y) = f.lintegral x + f.lintegral y

Tactic:
simp [lintegral, mul_add, Finset.sum_add_distrib]

Premises used: MeasureTheory.SimpleFunc.lintegral, Finset.sum_add_distrib, mul_add
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
m_1 : MeasurableSpace α
μ_1 ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
c : ℝ≥0∞
μ : Measure α
⊢ f.lintegral (c • μ) = HSMul.hSMul (α := ℝ≥0∞) ((RingHom.id ℝ≥0∞ : (a : ℝ≥0∞) → ℝ≥0∞) c : ℝ≥0∞) (f.lintegral μ)

Tactic:
simp [lintegral, mul_left_comm _ c, Finset.mul_sum, Measure.smul_apply c]

Premises used: MeasureTheory.SimpleFunc.lintegral, Finset.mul_sum, mul_left_comm, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ lintegral 0 μ = 0

Tactic:
LinearMap.ext_iff.1 lintegralₗ.map_zero μ

Premises used: Multiset.sum, MeasureTheory.SimpleFunc.lintegral, Multiset.foldr, MeasureTheory.SimpleFunc.lintegralₗ, LinearMap.map_zero, LinearMap.ext_iff, Iff.mp, Finset.sum
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α →ₛ ℝ≥0∞
⊢ f.lintegral (μ + ν) = f.lintegral μ + f.lintegral ν

Tactic:
(lintegralₗ f).map_add μ ν

Premises used: Multiset.sum, MeasureTheory.SimpleFunc.lintegral, LinearMap.map_add, Multiset.foldr, MeasureTheory.SimpleFunc.lintegralₗ, DFunLike.coe, Finset.sum
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
R : Type u_5
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
f : α →ₛ ℝ≥0∞
c : R
⊢ f.lintegral (c • μ) = c • f.lintegral μ

Tactic:
simpa only [smul_one_smul] using (lintegralₗ f).map_smul (c • 1) μ

Premises used: MeasureTheory.SimpleFunc.lintegralₗ, smul_one_smul, LinearMap.map_smul, HSMul.hSMul, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α →ₛ ℝ≥0∞
⊢ f.lintegral 0 = 0

Tactic:
(lintegralₗ f).map_zero

Premises used: Multiset.sum, MeasureTheory.SimpleFunc.lintegral, Multiset.foldr, MeasureTheory.SimpleFunc.lintegralₗ, LinearMap.map_zero, DFunLike.coe, Finset.sum
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
s : Finset ι
⊢ f.lintegral (∑ i ∈ s, μ i) = ∑ i ∈ s, f.lintegral (μ i)

Tactic:
map_sum (lintegralₗ f) ..

Premises used: Multiset.sum, MeasureTheory.SimpleFunc.lintegral, Multiset.foldr, MeasureTheory.SimpleFunc.lintegralₗ, map_sum, DFunLike.coe, Finset.sum
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
simp :
  Eq (α := ℝ≥0∞)
    (∑' (x : ↥f.range) (i : ι),
      HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
        ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))
    (∑' (i : ι) (x : ↥f.range),
      HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
        ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))
⊢ f.lintegral (Measure.sum μ) = ∑' (i : ι), f.lintegral (μ i)

Tactic:
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
    ENNReal.tsum_mul_left]

Premises used: MeasureTheory.SimpleFunc.lintegral, ENNReal.tsum_mul_left, MeasureTheory.Measure.sum_apply, MeasureTheory.SimpleFunc.measurableSet_preimage, Finset.tsum_subtype
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : ↥f.range) (i : ι),
      HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
        ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))
    (∑' (i : ι) (x : ↥f.range),
      HMul.hMul (β := ℝ≥0∞) (↑x : ℝ≥0∞)
        ((μ i : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {(↑x : ℝ≥0∞)}) : ℝ≥0∞))

Tactic:
apply ENNReal.tsum_comm

Premises used: ENNReal.tsum_comm
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : Ne (α := ℝ≥0∞) ((f.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
hxs : x ∈ s
h :
  Ne (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (preimage (β := ℝ≥0∞) (⇑(f.restrict s) : (a : α) → ℝ≥0∞)
          (singleton (α := ℝ≥0∞) ((f.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Membership.mem (α := ℝ≥0∞) f.range ((f.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
simp only [f.restrict_apply hs, indicator_of_mem hxs, mem_range_self]

Premises used: Set.indicator_of_mem, MeasureTheory.SimpleFunc.restrict_apply, MeasureTheory.SimpleFunc.mem_range_self
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
x : α
hx : Ne (α := ℝ≥0∞) ((f.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
hxs : x ∉ s
⊢ Eq (α := ℝ≥0∞) ((f.restrict s : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(f.restrict s) : (a : α) → ℝ≥0∞)
            (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)

Tactic:
simp only [hb, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
b : α
hb : ¬Eq (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (s ∩ preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑(f.restrict s) : (a : α) → ℝ≥0∞)
            (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) b : ℝ≥0∞)) ∩ s) :
        ℝ≥0∞)

Tactic:
rw [restrict_preimage_singleton _ hs hb, inter_comm]

Premises used: Set.inter_comm, MeasureTheory.SimpleFunc.restrict_preimage_singleton
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
s : Set α
μ : Measure α
⊢ f.lintegral (μ.restrict s) =
    ∑ y ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞)

Tactic:
simp only [lintegral, Measure.restrict_apply, f.measurableSet_preimage]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.Measure.restrict_apply, MeasureTheory.SimpleFunc.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw :
  ∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r} ∩ s) : ℝ≥0∞) =
    f.lintegral (μ.restrict s)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞)
    (∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r} ∩ s) : ℝ≥0∞))
    (∑ y ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) y ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {y} ∩ s) : ℝ≥0∞))
⊢ (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)

Tactic:
rw [f.restrict_lintegral hs, lintegral_restrict]

Premises used: MeasureTheory.SimpleFunc.restrict_lintegral, MeasureTheory.SimpleFunc.lintegral_restrict
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
simp :
  Eq (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      ⨆ (i : ι),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (⨆ (i : ι),
      ∑ x ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
⊢ f.lintegral (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), f.lintegral (μ.restrict (s i))

Tactic:
simp only [lintegral, Measure.restrict_iUnion_apply_eq_iSup hd (measurableSet_preimage ..),
    ENNReal.mul_iSup]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, MeasureTheory.SimpleFunc.measurableSet_preimage, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      ⨆ (i : ι),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (⨆ (i : ι),
      ∑ x ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))

Tactic:
finsetSum_iSup fun i j ↦ (hd i j).imp fun k ⟨hik, hjk⟩ ↦ fun a ↦ ?_

Premises used: Exists.imp, ENNReal.finsetSum_iSup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
refine :
  ∀ (i j k : ι),
    (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k) →
      ∀ (hik : s i ⊆ s k) (hjk : s j ⊆ s k) (a : ℝ≥0∞),
        HMul.hMul (β := ℝ≥0∞) a
              ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
            HMul.hMul (β := ℝ≥0∞) a
              ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ∧
          HMul.hMul (β := ℝ≥0∞) a
              ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
            HMul.hMul (β := ℝ≥0∞) a
              ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ f.range,
      ⨆ (i : ι),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (⨆ (i : ι),
      ∑ x ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) x
          ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))

Tactic:
refine finsetSum_iSup fun i j ↦ (hd i j).imp fun k ⟨hik, hjk⟩ ↦ fun a ↦ ?_

Premises used: Exists.imp, ENNReal.finsetSum_iSup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
h : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
left :
  HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
right :
  HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ∧
    HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
      HMul.hMul (β := ℝ≥0∞) a
        ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
h : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s i) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
h : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s j) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) a
      ((μ.restrict (s k) : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
inl :
  IsEmpty α →
    ∑ x ∈ SimpleFunc.range (const α c),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr :
  Nonempty α →
    ∑ x ∈ SimpleFunc.range (const α c),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : IsEmpty α
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [μ.eq_zero_of_isEmpty]

Premises used: MeasureTheory.Measure.eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
inr :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (Function.const α c ⁻¹' {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∑ x ∈ SimpleFunc.range (const α c),
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(const α c) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp only [range_const, coe_const, Finset.sum_singleton]

Premises used: Finset.sum_singleton, MeasureTheory.SimpleFunc.range_const, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
inr :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (fun (x : α) ↦ c) {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (Function.const α c ⁻¹' {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
unfold Function.const

Premises used: Function.const
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h : Nonempty α
inr inr₁ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (fun (x : α) ↦ c) {c}) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [preimage_const_of_mem (mem_singleton c)]

Premises used: Set.mem_singleton, Set.preimage_const_of_mem
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
rw :
  HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ lintegral (const α c) (μ.restrict s) = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasureTheory.SimpleFunc.const_lintegral, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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∞)
rw₁ rw₂ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ lintegral (restrict (const α c) s) μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]

Premises used: MeasureTheory.SimpleFunc.const_lintegral_restrict, MeasureTheory.SimpleFunc.restrict_lintegral_eq_lintegral_restrict
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
⊢ f.lintegral μ ≤ g.lintegral μ

Tactic:
Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h

Premises used: Monotone.of_left_le_map_sup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
h : f ≤ g
refine :
  ∀ (f g : α →ₛ ℝ≥0∞),
    LE.le (α := ℝ≥0∞) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) f) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) (f ⊔ g))
⊢ f.lintegral μ ≤ g.lintegral μ

Tactic:
refine Monotone.of_left_le_map_sup (f := (lintegral · μ)) (fun f g ↦ ?_) h

Premises used: Monotone.of_left_le_map_sup
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
rw rw₁ : f.lintegral μ = f.lintegral μ
⊢ f.lintegral μ = (map Prod.fst (f.pair g)).lintegral μ

Tactic:
rw [map_fst_pair]

Premises used: MeasureTheory.SimpleFunc.map_fst_pair
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
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∞))
⊢ (map Prod.fst (f.pair g)).lintegral μ ≤ lintegral (map (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ max p.1 p.2) (f.pair g)) μ

Tactic:
simp only [map_lintegral]

Premises used: MeasureTheory.SimpleFunc.map_lintegral
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
h₁ : ∀ i ∈ (f.pair g).range, i.1 ≤ max i.1 i.2
⊢ 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:
gcongr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
i : ℝ≥0∞ × ℝ≥0∞
h_1 : i ∈ (f.pair g).range
⊢ i.1 ≤ max i.1 i.2

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f_1 g_1 : α →ₛ ℝ≥0∞
h : f_1 ≤ g_1
f g : α →ₛ ℝ≥0∞
i : ℝ≥0∞ × ℝ≥0∞
h_1 : i ∈ (f.pair g).range
⊢ i.1 ≤ max i.1 i.2

Tactic:
exact le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
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 μ
μ₂ : (map Prod.fst (f.pair g)).lintegral μ ≤ lintegral (map (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ max p.1 p.2) (f.pair g)) μ
⊢ LE.le (α := ℝ≥0∞) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) f) ((fun (x : α →ₛ ℝ≥0∞) ↦ x.lintegral μ) (f ⊔ 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

Premises used: MeasureTheory.SimpleFunc.lintegral, Prod.fst, Max.max, MeasureTheory.SimpleFunc.pair, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ max (f.lintegral μ) (g.lintegral μ) ≤ (f ⊔ g).lintegral μ

Tactic:
Monotone.le_map_sup (fun _ _ ↦ lintegral_mono_fun) f g

Premises used: MeasureTheory.SimpleFunc.lintegral_mono_fun, Monotone.le_map_sup