awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
a₁ : ℝ≥0∞
h₁₁ : a₁ ∈ f.range
h₁₂ : HMul.hMul (β := ℝ≥0∞) a₁ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₁}) : ℝ≥0∞) ≠ 0
a₂ : ℝ≥0∞
h₂₁ : a₂ ∈ f.range
h₂₂ : HMul.hMul (β := ℝ≥0∞) a₂ ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a₂}) : ℝ≥0∞) ≠ 0
h :
  Eq (α := ℝ≥0∞)
    ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
          (x_1 :
            HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
              0) ↦
        r)
      a₁ h₁₁ h₁₂)
    ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
          (x_1 :
            HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
              0) ↦
        r)
      a₂ h₂₁ h₂₂)
⊢ a₁ = a₂

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
refine_3 :
  b ∈ s →
    HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0 →
      ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
        HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
        (fun (r : ℝ≥0∞) (x : r ∈ f.range)
                (x_1 :
                  HMul.hMul (β := ℝ≥0∞) r
                      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                    0) ↦
              r)
            a h₁ h₂ =
          b
⊢ b ∈ s →
    HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0 →
      ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
        HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
        (fun (r : ℝ≥0∞) (x : r ∈ f.range)
                (x_1 :
                  HMul.hMul (β := ℝ≥0∞) r
                      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                    0) ↦
              r)
            a h₁ h₂ =
          b

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
⊢ ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
    HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ =
      b

Tactic:
⟨b, ?_, hb, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
refine_3 : b ∈ f.range
⊢ ∃ (a : ℝ≥0∞) (h₁ : a ∈ f.range) (h₂ :
    HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0),
    (fun (r : ℝ≥0∞) (x : r ∈ f.range)
            (x_1 :
              HMul.hMul (β := ℝ≥0∞) r
                  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                0) ↦
          r)
        a h₁ h₂ =
      b

Tactic:
refine ⟨b, ?_, hb, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
refine_3 : Set.Nonempty (α := α) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b})
⊢ b ∈ f.range

Tactic:
rw [mem_range, ← preimage_singleton_nonempty]

Premises used: Set.preimage_singleton_nonempty, MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
⊢ Set.Nonempty (α := α) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b})

Tactic:
nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, And.right, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
b : ℝ≥0∞
h : b ∈ s
hb : HMul.hMul (β := ℝ≥0∞) b ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b}) : ℝ≥0∞) ≠ 0
⊢ Set.Nonempty (α := α) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {b})

Tactic:
exact nonempty_of_measure_ne_zero (mul_ne_zero_iff.1 hb).2

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, And.right, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs :
  ∀ (x : α),
    Ne (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞) →
      Ne (α := ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞)
              (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) (singleton (α := ℝ≥0∞) ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞))) :
            ℝ≥0∞)
          (0 : ℝ≥0∞) →
        Membership.mem (α := ℝ≥0∞) s ((f : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
a : ℝ≥0∞
h₁ : a ∈ f.range
h₂ : HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) ≠ 0
⊢ HMul.hMul (β := ℝ≥0∞) a ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {a}) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((fun (r : ℝ≥0∞) (x : r ∈ f.range)
              (x_1 :
                HMul.hMul (β := ℝ≥0∞) r
                    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                  0) ↦
            r)
          a h₁ h₂ :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞)
            {(fun (r : ℝ≥0∞) (x : r ∈ f.range)
                    (x_1 :
                      HMul.hMul (β := ℝ≥0∞) r
                          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) ≠
                        0) ↦
                  r)
                a h₁ h₂}) :
        ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : f.range \ {0} ⊆ s
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)

Tactic:
f.lintegral_eq_of_subset fun x hfx _ =>
    hs <| Finset.mem_sdiff.2 ⟨f.mem_range_self x, mt Finset.mem_singleton.1 hfx⟩

Premises used: Iff.mpr, Finset.mem_singleton, mt, Finset.mem_sdiff, And.intro, Iff.mp, MeasureTheory.SimpleFunc.lintegral_eq_of_subset, MeasureTheory.SimpleFunc.mem_range_self
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
simp :
  Eq (α := ℝ≥0∞)
    (∑ x ∈ Finset.image g f.range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞))
⊢ (map g f).lintegral μ =
    ∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞)

Tactic:
simp only [lintegral, range_map]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.range_map
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ Finset.image g f.range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞))

Tactic:
Finset.sum_image' _ fun b hb => ?_

Premises used: Finset.sum_image'
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
refine :
  ∀ (b : β) (hb : b ∈ f.range),
    HMul.hMul (β := ℝ≥0∞) (g b)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g b}) : ℝ≥0∞) =
      ∑ j ∈ f.range with g j = g b,
        HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ Finset.image g f.range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞))
    (∑ x ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞))

Tactic:
refine Finset.sum_image' _ fun b hb => ?_

Premises used: Finset.sum_image'
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
b : β
hb : b ∈ f.range
rcases :
  ∀ (a : α) (hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)),
    HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g ((f : (a : α) → β) a)}) :
          ℝ≥0∞) =
      ∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
        HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (g b)
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g b}) : ℝ≥0∞) =
    ∑ j ∈ f.range with g j = g b,
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)

Tactic:
rcases mem_range.1 hb with ⟨a, rfl⟩

Premises used: MeasureTheory.SimpleFunc.mem_range, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
rw :
  Eq (α := ℝ≥0∞)
    (∑ i ∈ f.range with g i = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {i}) : ℝ≥0∞))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(map g f) : (a : α) → ℝ≥0∞) {g ((f : (a : α) → β) a)}) : ℝ≥0∞) =
    ∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞)

Tactic:
rw [map_preimage_singleton, ← f.sum_measure_preimage_singleton, Finset.mul_sum]

Premises used: MeasureTheory.SimpleFunc.sum_measure_preimage_singleton, Finset.mul_sum, MeasureTheory.SimpleFunc.map_preimage_singleton
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ f.range with g i = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {i}) : ℝ≥0∞))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞))

Tactic:
Finset.sum_congr ?_ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
refine_1 : {b ∈ f.range | g b = g ((f : (a : α) → β) a)} = {j ∈ f.range | g j = g ((f : (a : α) → β) a)}
refine_2 :
  ∀ x ∈ {j ∈ f.range | g j = g ((f : (a : α) → β) a)},
    HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑ i ∈ f.range with g i = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {i}) : ℝ≥0∞))
    (∑ j ∈ f.range with g j = g ((f : (a : α) → β) a),
      HMul.hMul (β := ℝ≥0∞) (g j) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {j}) : ℝ≥0∞))

Tactic:
refine Finset.sum_congr ?_ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
⊢ {b ∈ f.range | g b = g ((f : (a : α) → β) a)} = {j ∈ f.range | g j = g ((f : (a : α) → β) a)}

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : Membership.mem (α := β) f.range ((f : (a : α) → β) a : β)
⊢ ∀ x ∈ {j ∈ f.range | g j = g ((f : (a : α) → β) a)},
    HMul.hMul (β := ℝ≥0∞) (g ((f : (a : α) → β) a))
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) (g x) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑f : (a : α) → β) {x}) : ℝ≥0∞)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
rw :
  Eq (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) (x.1 + x.2)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥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∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)))
⊢ (f + g).lintegral μ =
    ∑ x ∈ (f.pair g).range,
      (HMul.hMul (β := ℝ≥0∞) x.1
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))

Tactic:
rw [add_eq_map₂, map_lintegral]

Premises used: MeasureTheory.SimpleFunc.map_lintegral, MeasureTheory.SimpleFunc.add_eq_map₂
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) (x.1 + x.2)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥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∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)))

Tactic:
Finset.sum_congr rfl fun a _ => add_mul _ _ _

Premises used: add_mul, Prod.fst, Set.preimage, Singleton.singleton, Prod.snd, DFunLike.coe, Finset.sum_congr, rfl, MeasureTheory.SimpleFunc.pair
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ (f.pair g).range,
      HMul.hMul (β := ℝ≥0∞) (x.1 + x.2)
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥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∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)))

Tactic:
exact Finset.sum_congr rfl fun a _ => add_mul _ _ _

Premises used: add_mul, Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
rw rw₁ :
  HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥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∞) +
        HMul.hMul (β := ℝ≥0∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))

Tactic:
rw [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α →ₛ ℝ≥0∞
rw :
  HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥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∞) +
      (map Prod.snd (f.pair g)).lintegral μ
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞))
⊢ HAdd.hAdd (α := ℝ≥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∞) x.2
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞ × ℝ≥0∞) (⇑(f.pair g) : (a : α) → ℝ≥0∞ × ℝ≥0∞) {x}) : ℝ≥0∞)) =
    (map Prod.fst (f.pair g)).lintegral μ + (map Prod.snd (f.pair g)).lintegral μ

Tactic:
rw [map_lintegral, map_lintegral]

Premises used: MeasureTheory.SimpleFunc.map_lintegral
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
x : ℝ≥0∞
simp_rw :
  Eq (α := ℝ≥0∞)
    (∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (x * r) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
    (∑ i ∈ f.range,
      x * HMul.hMul (β := ℝ≥0∞) i ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {i}) : ℝ≥0∞))
⊢ ∑ r ∈ f.range,
      HMul.hMul (β := ℝ≥0∞) (x * r) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞) =
    x *
      ∑ r ∈ f.range,
        HMul.hMul (β := ℝ≥0∞) r ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)

Tactic:
simp_rw [Finset.mul_sum, mul_assoc]

Premises used: Finset.mul_sum, mul_assoc