-- 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∞)
refine_1 :
  ∀ (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₂ ∈
      s
refine_2 :
  ∀ (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),
    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₂
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
refine_4 :
  ∀ (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∞)
⊢ f.lintegral μ =
    ∑ x ∈ s, HMul.hMul (β := ℝ≥0∞) x ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑f : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)

Tactic:
refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_

Premises used: Finset.sum_bij_ne_zero