-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem _root_.MeasurableEmbedding.lintegral_map [MeasurableSpace β] {g : α → β}
    (hg : MeasurableEmbedding g) (f : β → ℝ≥0∞) : ∫⁻ a, f a ∂map g μ = ∫⁻ a, f (g a) ∂μ

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0)) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ

Tactic:
refine lintegral_mono_ae (hg.ae_map_iff.2 <| Eventually.of_forall fun x => ?_)

Result:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
x : α
⊢ (f₀.extend g hg (const β 0)) (g x) ≤ f (g x)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
x : α
⊢ (f₀.extend g hg (const β 0)) (g x) ≤ f (g x)

Tactic:
exact (extend_apply _ _ _ _).trans_le (hf₀ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
this : ⇑(f₀.comp g ⋯) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ (_ : ⇑(f₀.comp g ⋯) ≤ fun a => f (g a)), (f₀.comp g ⋯).lintegral μ

Tactic:
exact le_iSup (α := ℝ≥0∞) _ this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ) =
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Tactic:
refine le_antisymm (iSup₂_le fun f₀ hf₀ => ?_) (iSup₂_le fun f₀ hf₀ => ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
⊢ f₀.lintegral (Measure.map g μ) ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
⊢ f₀.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
⊢ f₀.lintegral (Measure.map g μ) ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Tactic:
rw [SimpleFunc.lintegral_map _ hg.measurable]

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [lintegral, lintegral]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ) =
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
this : ⇑(f₀.comp g ⋯) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Tactic:
exact le_iSup_of_le (comp f₀ g hg.measurable) (by exact le_iSup (α := ℝ≥0∞) _ this)

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Tactic:
have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g := fun x => hf₀ (g x)

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : β →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f a
this : ⇑(f₀.comp g ⋯) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f (g a)), g_1.lintegral μ

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
⊢ f₀.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => f a), g_1.lintegral (Measure.map g μ)

Tactic:
rw [← f₀.extend_comp_eq hg (const _ 0), ← SimpleFunc.lintegral_map, ←
  SimpleFunc.lintegral_eq_lintegral, ← lintegral]

Result:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : α →ₛ ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a => f (g a)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0)) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ