Behavior of the Lebesgue integral under measure-preserving maps

theorem MeasureTheory.MeasurePreserving.lintegral_map_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} (f : β → ENNReal) (g : α ≃ᵐ β) (hg : MeasurePreserving (⇑g) μ ν) : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ

theorem MeasureTheory.MeasurePreserving.lintegral_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) {f : β → ENNReal} (hf : Measurable f) : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

theorem MeasureTheory.MeasurePreserving.lintegral_comp_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) {s : Set β} (hs : MeasurableSet s) {f : β → ENNReal} (hf : Measurable f) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_preimage_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set β) : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

theorem MeasureTheory.MeasurePreserving.setLIntegral_comp_emb {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {ν : Measure β} {g : α → β} (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν