7.6. 密度付き測度🔗

定義.

X を可測空間とし、\mu を X 上の測度、f : X \to [0,\infty] を関数とする。測度 f \cdot \mu を、任意の可測集合 A \subseteq X に対して (f \cdot \mu)(A) \coloneqq \underline{\int}_{x \in A} f(x)\,d\mu で定める。

Lean code

/-- The measure with density `f` with respect to `μ`. -/
def withDensity (μ : Measure X) (f : X → ℝ≥0∞) : Measure X :=
  Measure.ofMeasurable (fun A _ ↦ ∫⁻ x in A, f x ∂μ) (byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞⊢ (fun A x => ∫⁻ (x : X) in A, f x ∂μ) ∅ ⋯ = 0 simpAll goals completed! 🐙) <| byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞⊢ ∀ ⦃f_1 : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f_1 i)),
  Pairwise (Function.onFun Disjoint f_1) →
    (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (⋃ i, f_1 i) ⋯ = ∑' (i : ℕ), (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (f_1 i) ⋯
    intro A hAX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Function.onFun Disjoint A) →
  (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (A i) ⋯ hAdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => ∫⁻ (x : X) in A, f x ∂μ) (A i) ⋯
    exact lintegral_iUnion hA hAd fAll goals completed! 🐙

theorem withDensity_apply (μ : Measure X) (f : X → ℝ≥0∞) {A : Set X}
    (hA : MeasurableSet A) :
    Measure.withDensity μ f A = ∫⁻ x in A, f x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞A:Set XhA:MeasurableSet A⊢ (withDensity μ f) A = ∫⁻ (x : X) in A, f x ∂μ
  rw [Measure.withDensity]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞A:Set XhA:MeasurableSet A⊢ (Measure.ofMeasurable (fun A x => ∫⁻ (x : X) in A, f x ∂μ) ⋯ ⋯) A = ∫⁻ (x : X) in A, f x ∂μ
  exact Measure.ofMeasurable_apply _ hAAll goals completed! 🐙

補題.

f, g : X \to [0,\infty] を可測とする。このとき \underline{\int}_{x \in X} g(x)\,d(f \cdot \mu) = \underline{\int}_{x \in X} f(x) g(x)\,d\mu. が成り立つ。

Lean code

theorem lintegral_withDensity_eq_lintegral_mul (μ : Measure X) {f g : X → ℝ≥0∞}
    (hf : Measurable f) (hg : Measurable g) :
    ∫⁻ x, g x ∂(Measure.withDensity μ f) = ∫⁻ x, (f * g) x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : X), g x ∂Measure.withDensity μ f = ∫⁻ (x : X), (f * g) x ∂μ
  have lhs := calc
    ∫⁻ x, g x ∂(Measure.withDensity μ f) =
      ∫⁻ x : X, ⨆ i, (SimpleFunc.eapprox g i) x ∂(Measure.withDensity μ f) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : X), g x ∂Measure.withDensity μ f = ∫⁻ (x : X), ⨆ i, (SimpleFunc.eapprox g i) x ∂Measure.withDensity μ f
        apply lintegral_congrhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (a : X), g a = ⨆ i, (SimpleFunc.eapprox g i) a
        intro xhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable gx:X⊢ g x = ⨆ i, (SimpleFunc.eapprox g i) x
        exact (SimpleFunc.iSup_eapprox_apply hg x).symmAll goals completed! 🐙
    _ = ⨆ n, ∫⁻ x : X, (SimpleFunc.eapprox g n) x ∂(Measure.withDensity μ f) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : X), ⨆ i, (SimpleFunc.eapprox g i) x ∂Measure.withDensity μ f =
  ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f
        apply lintegral_iSuphfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (n : ℕ), Measurable ⇑(SimpleFunc.eapprox g n)h_monoX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => ⇑(SimpleFunc.eapprox g n)
        ·hfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (n : ℕ), Measurable ⇑(SimpleFunc.eapprox g n) intro nhfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable gn:ℕ⊢ Measurable ⇑(SimpleFunc.eapprox g n)
          exact (SimpleFunc.eapprox g n).measurableAll goals completed! 🐙
        ·h_monoX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => ⇑(SimpleFunc.eapprox g n) exact SimpleFunc.monotone_eapprox gAll goals completed! 🐙
  have rhs := calc
    ∫⁻ x, (f * g) x ∂μ =
      ∫⁻ x : X, ⨆ i, f x * (SimpleFunc.eapprox g i) x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∫⁻ (x : X), (f * g) x ∂μ = ∫⁻ (x : X), ⨆ i, f x * (SimpleFunc.eapprox g i) x ∂μ
        apply lintegral_congrhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∀ (a : X), (f * g) a = ⨆ i, f a * (SimpleFunc.eapprox g i) a
        intro xhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))x:X⊢ (f * g) x = ⨆ i, f x * (SimpleFunc.eapprox g i) x
        simp only [Pi.mul_apply, ← mul_iSup]hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))x:X⊢ f x * g x = f x * ⨆ i, (SimpleFunc.eapprox g i) x
        exact congrArg (fun t => f x * t) (SimpleFunc.iSup_eapprox_apply hg x).symmAll goals completed! 🐙
    _ = ⨆ n, ∫⁻ x : X, f x * (SimpleFunc.eapprox g n) x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∫⁻ (x : X), ⨆ i, f x * (SimpleFunc.eapprox g i) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
        apply lintegral_iSuphfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∀ (n : ℕ), Measurable fun a => f a * (SimpleFunc.eapprox g n) ah_monoX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ Monotone fun n a => f a * (SimpleFunc.eapprox g n) a
        ·hfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∀ (n : ℕ), Measurable fun a => f a * (SimpleFunc.eapprox g n) a intro nhfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))n:ℕ⊢ Measurable fun a => f a * (SimpleFunc.eapprox g n) a
          exact hf.mul (SimpleFunc.eapprox g n).measurableAll goals completed! 🐙
        ·h_monoX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ Monotone fun n a => f a * (SimpleFunc.eapprox g n) a apply monotone_lamh_mono.hfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))⊢ ∀ (b : X), Monotone fun a => f b * (SimpleFunc.eapprox g a) b
          intro xh_mono.hfX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))x:X⊢ Monotone fun a => f x * (SimpleFunc.eapprox g a) x
          exact Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)All goals completed! 🐙
  rw [lhs, rhs]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))⊢ ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f =
  ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
  apply iSup_congrhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))⊢ ∀ (i : ℕ),
  ∫⁻ (x : X), (SimpleFunc.eapprox g i) x ∂Measure.withDensity μ f = ∫⁻ (x : X), f x * (SimpleFunc.eapprox g i) x ∂μ
  intro nhX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f = ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
  calc
    ∫⁻ x : X, (SimpleFunc.eapprox g n) x ∂(Measure.withDensity μ f)
        = ∑ y ∈ (SimpleFunc.eapprox g n).range,
            ∫⁻ x : X in (SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f =
  ∑ y ∈ (SimpleFunc.eapprox g n).range, ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ
          rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.lintegral]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ x ∈ (SimpleFunc.eapprox g n).range, x * (Measure.withDensity μ f) (⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) =
  ∑ y ∈ (SimpleFunc.eapprox g n).range, ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ
          apply Finset.sum_congr rflX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∀ x ∈ (SimpleFunc.eapprox g n).range,
  x * (Measure.withDensity μ f) (⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) =
    ∫⁻ (x_1 : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}, x * f x_1 ∂μ
          intro y hyX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).range⊢ y * (Measure.withDensity μ f) (⇑(SimpleFunc.eapprox g n) ⁻¹' {y}) =
  ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ
          rw [Measure.withDensity_apply _ _ ((SimpleFunc.eapprox g n).measurableSet_fiber y)]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).range⊢ y * ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, f x ∂μ =
  ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ
          rw [lintegral_const_mul _ hf]All goals completed! 🐙
    _ = ∑ y ∈ (SimpleFunc.eapprox g n).range,
          ∫⁻ x : X in (SimpleFunc.eapprox g n) ⁻¹' {y}, (SimpleFunc.eapprox g n) x * f x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ y ∈ (SimpleFunc.eapprox g n).range, ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ =
  ∑ y ∈ (SimpleFunc.eapprox g n).range,
    ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, (SimpleFunc.eapprox g n) x * f x ∂μ
          apply Finset.sum_congr rflX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∀ x ∈ (SimpleFunc.eapprox g n).range,
  ∫⁻ (x_1 : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}, x * f x_1 ∂μ =
    ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}, (SimpleFunc.eapprox g n) x * f x ∂μ
          intro y hyX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).range⊢ ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, y * f x ∂μ =
  ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, (SimpleFunc.eapprox g n) x * f x ∂μ
          apply setLIntegral_congr_fun ((SimpleFunc.eapprox g n).measurableSet_fiber y)X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).range⊢ EqOn (fun x => y * f x) (fun x => (SimpleFunc.eapprox g n) x * f x) (⇑(SimpleFunc.eapprox g n) ⁻¹' {y})
          intro x hxX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).rangex:Xhx:x ∈ ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}⊢ (fun x => y * f x) x = (fun x => (SimpleFunc.eapprox g n) x * f x) x
          simp only [mem_preimage, mem_singleton_iff] at hxX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕy:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).rangex:Xhx:(SimpleFunc.eapprox g n) x = y⊢ (fun x => y * f x) x = (fun x => (SimpleFunc.eapprox g n) x * f x) x
          simp [hx]All goals completed! 🐙
    _ = ∫⁻ x : X, f x * (SimpleFunc.eapprox g n) x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ y ∈ (SimpleFunc.eapprox g n).range,
    ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, (SimpleFunc.eapprox g n) x * f x ∂μ =
  ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
          rw [← lintegral_finset_sum_measure]X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∫⁻ (a : X),
    (SimpleFunc.eapprox g n) a *
      f a ∂∑ i ∈ (SimpleFunc.eapprox g n).range, μ.restrict (⇑(SimpleFunc.eapprox g n) ⁻¹' {i}) =
  ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
          apply congrArg₂hxX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ i ∈ (SimpleFunc.eapprox g n).range, μ.restrict (⇑(SimpleFunc.eapprox g n) ⁻¹' {i}) = μhyX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ (fun a => (SimpleFunc.eapprox g n) a * f a) = fun x => f x * (SimpleFunc.eapprox g n) x
          ·hxX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ i ∈ (SimpleFunc.eapprox g n).range, μ.restrict (⇑(SimpleFunc.eapprox g n) ⁻¹' {i}) = μ ext A hAhx.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ (∑ i ∈ (SimpleFunc.eapprox g n).range, μ.restrict (⇑(SimpleFunc.eapprox g n) ⁻¹' {i})) A = μ A
            simp only [Measure.coe_finset_sum, Finset.sum_apply]hx.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ ∑ c ∈ (SimpleFunc.eapprox g n).range, (μ.restrict (⇑(SimpleFunc.eapprox g n) ⁻¹' {c})) A = μ A
            simp only [Measure.restrict_apply hA]hx.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ ∑ x ∈ (SimpleFunc.eapprox g n).range, μ (A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) = μ A
            rw [← measure_biUnion_finset]hx.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ μ (⋃ b ∈ (SimpleFunc.eapprox g n).range, A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b}) = μ Ahx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ (↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}hx.h.hmX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ ∀ b ∈ (SimpleFunc.eapprox g n).range, MeasurableSet (A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b})
            ·hx.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ μ (⋃ b ∈ (SimpleFunc.eapprox g n).range, A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b}) = μ A apply congrArghx.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ ⋃ b ∈ (SimpleFunc.eapprox g n).range, A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b} = A
              ext xhx.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ax:X⊢ x ∈ ⋃ b ∈ (SimpleFunc.eapprox g n).range, A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b} ↔ x ∈ A
              simp only [← inter_iUnion]hx.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ax:X⊢ x ∈ A ∩ ⋃ i ∈ (SimpleFunc.eapprox g n).range, ⇑(SimpleFunc.eapprox g n) ⁻¹' {i} ↔ x ∈ A
              rw [mem_inter_iff]hx.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ax:X⊢ x ∈ A ∧ x ∈ ⋃ i ∈ (SimpleFunc.eapprox g n).range, ⇑(SimpleFunc.eapprox g n) ⁻¹' {i} ↔ x ∈ A
              simpAll goals completed! 🐙
            ·hx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ (↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x} have hpair :
                  ((SimpleFunc.eapprox g n).range : Set ℝ≥0∞).PairwiseDisjoint
                    fun y ↦ (SimpleFunc.eapprox g n) ⁻¹' {y} := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ ∑ y ∈ (SimpleFunc.eapprox g n).range,
    ∫⁻ (x : X) in ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}, (SimpleFunc.eapprox g n) x * f x ∂μ =
  ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ
                exact pairwiseDisjoint_fiber (SimpleFunc.eapprox g n) (SimpleFunc.eapprox g n).rangeAll goals completed! 🐙
              intro y hyhx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).range⊢ ∀ ⦃y_1 : ℝ≥0∞⦄,
  y_1 ∈ ↑(SimpleFunc.eapprox g n).range →
    y ≠ y_1 → Function.onFun Disjoint (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y y_1 zhx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞⊢ z ∈ ↑(SimpleFunc.eapprox g n).range →
  y ≠ z → Function.onFun Disjoint (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y z hzhx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).range⊢ y ≠ z → Function.onFun Disjoint (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y z hyzhx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).rangehyz:y ≠ z⊢ Function.onFun Disjoint (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y z shx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).rangehyz:y ≠ zs:Set X⊢ s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y → s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) z → s ≤ ⊥ hy'hx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).rangehyz:y ≠ zs:Set Xhy':s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) y⊢ s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) z → s ≤ ⊥ hz'hx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).rangehyz:y ≠ zs:Set Xhy':s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) yhz':s ≤ (fun x => A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {x}) z⊢ s ≤ ⊥
              simp only [le_eq_subset, subset_inter_iff] at hy' hz'hx.h.hdX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ahpair:(↑(SimpleFunc.eapprox g n).range).PairwiseDisjoint fun y => ⇑(SimpleFunc.eapprox g n) ⁻¹' {y} := pairwiseDisjoint_fiber ⇑(SimpleFunc.eapprox g n) ↑(SimpleFunc.eapprox g n).rangey:ℝ≥0∞hy:y ∈ ↑(SimpleFunc.eapprox g n).rangez:ℝ≥0∞hz:z ∈ ↑(SimpleFunc.eapprox g n).rangehyz:y ≠ zs:Set Xhy':s ⊆ A ∧ s ⊆ ⇑(SimpleFunc.eapprox g n) ⁻¹' {y}hz':s ⊆ A ∧ s ⊆ ⇑(SimpleFunc.eapprox g n) ⁻¹' {z}⊢ s ≤ ⊥
              exact hpair hy hz hyz hy'.2 hz'.2All goals completed! 🐙
            ·hx.h.hmX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet A⊢ ∀ b ∈ (SimpleFunc.eapprox g n).range, MeasurableSet (A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {b}) intro y hyhx.h.hmX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕA:Set XhA:MeasurableSet Ay:ℝ≥0∞hy:y ∈ (SimpleFunc.eapprox g n).range⊢ MeasurableSet (A ∩ ⇑(SimpleFunc.eapprox g n) ⁻¹' {y})
              exact hA.inter ((SimpleFunc.eapprox g n).measurableSet_fiber y)All goals completed! 🐙
          ·hyX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕ⊢ (fun a => (SimpleFunc.eapprox g n) a * f a) = fun x => f x * (SimpleFunc.eapprox g n) x ext xhy.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝ≥0∞g:X → ℝ≥0∞hf:Measurable fhg:Measurable glhs:∫⁻ (x : X), g x ∂Measure.withDensity μ f = ⨆ n, ∫⁻ (x : X), (SimpleFunc.eapprox g n) x ∂Measure.withDensity μ f := 
  Trans.trans (lintegral_congr fun x => Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))
    (lintegral_iSup (fun n => SimpleFunc.measurable (SimpleFunc.eapprox g n)) (SimpleFunc.monotone_eapprox g))rhs:∫⁻ (x : X), (f * g) x ∂μ = ⨆ n, ∫⁻ (x : X), f x * (SimpleFunc.eapprox g n) x ∂μ := 
  Trans.trans
    (lintegral_congr fun x =>
      Eq.mpr
        (id
          (congrArg (Eq (f x * g x))
            (lintegral_withDensity_eq_lintegral_mul._simp_1 (f x) fun i => (SimpleFunc.eapprox g i) x)))
        (congrArg (fun t => f x * t) (Eq.symm (SimpleFunc.iSup_eapprox_apply hg x))))
    (lintegral_iSup (fun n => Measurable.mul hf (SimpleFunc.measurable (SimpleFunc.eapprox g n)))
      (monotone_lam fun x => Monotone.const_mul' (fun a b hab => SimpleFunc.monotone_eapprox g hab x) (f x)))n:ℕx:X⊢ (SimpleFunc.eapprox g n) x * f x = f x * (SimpleFunc.eapprox g n) x
            ringAll goals completed! 🐙