awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
e_s :
  ∀ (n : ℕ),
    SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = SimpleFunc.lintegral (eapprox (f ∘ g) n) μ
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ))
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (f ∘ g) n) μ)

Tactic:
congr with n : 1
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = (comp (eapprox f n) g hg).lintegral μ

Tactic:
SimpleFunc.lintegral_map _ hg

Premises used: MeasureTheory.SimpleFunc.lintegral_map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
h : eapprox (f ∘ g) n = comp (eapprox f n) g hg
⊢ SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = SimpleFunc.lintegral (eapprox (f ∘ g) n) μ

Tactic:
convert! SimpleFunc.lintegral_map _ hg

Premises used: MeasureTheory.SimpleFunc.lintegral_map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) (((eapprox (f ∘ g) n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
      ((comp (eapprox f n) g hg : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
⊢ eapprox (f ∘ g) n = comp (eapprox f n) g hg

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
n : ℕ
x : α
⊢ Eq (α := ℝ≥0∞) (((eapprox (f ∘ g) n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x : ℝ≥0∞)
    ((comp (eapprox f n) g hg : (a : α) → ℝ≥0∞) x : ℝ≥0∞)

Tactic:
simp only [eapprox_comp hf hg, coe_comp]

Premises used: MeasureTheory.SimpleFunc.eapprox_comp, MeasureTheory.SimpleFunc.coe_comp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable (_m := inst_1) f (Measure.map g μ)
hg : AEMeasurable g μ
e_μ : Eq (α := Measure β) (Measure.map g μ) (Measure.map (AEMeasurable.mk g hg) μ)
⊢ ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map g μ =
    ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map (AEMeasurable.mk g hg) μ

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable (_m := inst_1) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Eq (α := Measure β) (Measure.map g μ) (Measure.map (AEMeasurable.mk g hg) μ)

Tactic:
Measure.map_congr hg.ae_eq_mk

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable (_m := inst_1) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Eq (α := Measure β) (Measure.map g μ) (Measure.map (AEMeasurable.mk g hg) μ)

Tactic:
exact Measure.map_congr hg.ae_eq_mk

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
pos : ∀ (hg : AEMeasurable g μ), ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
neg : ∀ (hg : ¬AEMeasurable g μ), ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
by_cases hg : AEMeasurable g μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
pos :
  ⨆ (g_1 : β → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤
    ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral]

Premises used: MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
⊢ ⨆ (g_1 : β → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤
    ∫⁻ (a : α), f (g a) ∂μ

Tactic:
iSup₂_le fun i hi => iSup_le fun h'i => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
pos : ∀ (i : β → ℝ≥0∞) (hi : Measurable i) (h'i : i ≤ f), ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
⊢ ⨆ (g_1 : β → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤
    ∫⁻ (a : α), f (g a) ∂μ

Tactic:
refine iSup₂_le fun i hi => iSup_le fun h'i => ?_

Premises used: iSup₂_le, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
pos : ∫⁻ (a : α), i (g a) ∂μ ≤ ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [lintegral_map' hi.aemeasurable hg]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_map'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : α), i (g a) ∂μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
lintegral_mono fun _ ↦ h'i _

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : AEMeasurable g μ
i : β → ℝ≥0∞
hi : Measurable i
h'i : i ≤ f
⊢ ∫⁻ (a : α), i (g a) ∂μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
exact lintegral_mono fun _ ↦ h'i _

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hg : ¬AEMeasurable g μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ

Tactic:
simp [map_of_not_aemeasurable hg]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
⊢ lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂Measure.map g μ

Tactic:
(lintegral_map hf hg).symm

Premises used: MeasureTheory.lintegral_map, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable (_m := inst_1) f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂Measure.map g μ

Tactic:
(lintegral_map' hf hg).symm

Premises used: Eq.symm, MeasureTheory.lintegral_map'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
rw : ∫⁻ (y : β), f y ∂Measure.map g (μ.restrict (g ⁻¹' s)) = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ

Tactic:
rw [restrict_map hg hs, lintegral_map hf hg]

Premises used: MeasureTheory.Measure.restrict_map, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
rw :
  ∫⁻ (a : β), s.indicator (fun (x : β) ↦ c) a ∂Measure.map f μ =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
rw₁ :
  HMul.hMul (β := ℝ≥0∞) c (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
rw₂ rw₃ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : β) ↦ c) (f a) ∂μ =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [← lintegral_map (measurable_const.indicator hs) hf, lintegral_indicator_const hs,
    Measure.map_apply hf hs]

Premises used: MeasureTheory.Measure.map_apply, Measurable.indicator, MeasureTheory.lintegral_indicator_const, MeasureTheory.lintegral_map, measurable_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (g_1 : SimpleFunc β ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a), g_1.lintegral (Measure.map g μ))
    (⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ)
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [lintegral, lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞)
    (⨆ (g_1 : SimpleFunc β ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a), g_1.lintegral (Measure.map g μ))
    (⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ)

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

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
refine_1 :
  ∀ (f₀ : SimpleFunc β ℝ≥0∞) (hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a),
    f₀.lintegral (Measure.map g μ) ≤
      ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ
refine_2 :
  ∀ (f₀ : SimpleFunc α ℝ≥0∞) (hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)),
    f₀.lintegral μ ≤
      ⨆ (g_1 : SimpleFunc β ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a), g_1.lintegral (Measure.map g μ)
⊢ Eq (α := ℝ≥0∞)
    (⨆ (g_1 : SimpleFunc β ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a), g_1.lintegral (Measure.map g μ))
    (⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ)

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

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a
refine_1 :
  (f₀.comp g ⋯).lintegral μ ≤
    ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ
⊢ f₀.lintegral (Measure.map g μ) ≤
    ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ

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

Premises used: MeasureTheory.SimpleFunc.lintegral_map, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a
⊢ (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) ≤ f ∘ g

Tactic:
have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g := fun x => hf₀ (g x)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a
this : (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)),
      (f₀.comp g ⋯).lintegral μ

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

Premises used: le_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a
this : (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤
    ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)),
      (f₀.comp g ⋯).lintegral μ

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

Premises used: le_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : LE.le (α := (a : β) → ℝ≥0∞) (⇑f₀ : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a
this : (⇑(f₀.comp g ⋯) : (a : α) → ℝ≥0∞) ≤ f ∘ g
⊢ (f₀.comp g ⋯).lintegral μ ≤
    ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) 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)

Premises used: le_iSup_of_le, MeasurableEmbedding.measurable, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)
refine_2 :
  ∫⁻ (a : β), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ
⊢ f₀.lintegral μ ≤
    ⨆ (g_1 : SimpleFunc β ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) 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]

Premises used: MeasureTheory.SimpleFunc.const, MeasureTheory.SimpleFunc.extend_comp_eq, MeasureTheory.SimpleFunc.lintegral_map, OfNat.ofNat, MeasureTheory.lintegral, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ

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

Premises used: Iff.mpr, MeasureTheory.lintegral_mono_ae, Filter.Eventually.of_forall, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)
refine_2 : ∀ (x : α), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) (g x) ≤ f (g x)
⊢ ∫⁻ (a : β), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥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 => ?_)

Premises used: Iff.mpr, MeasureTheory.lintegral_mono_ae, Filter.Eventually.of_forall, MeasurableEmbedding.ae_map_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)
x : α
⊢ (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) (g x) ≤ f (g x)

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

Premises used: Eq.trans_le, MeasureTheory.SimpleFunc.extend_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc α ℝ≥0∞
hf₀ : LE.le (α := (a : α) → ℝ≥0∞) (⇑f₀ : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)
x : α
⊢ (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) (g x) ≤ f (g x)

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

Premises used: Eq.trans_le, MeasureTheory.SimpleFunc.extend_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α ≃ᵐ β
⊢ ∫⁻ (a : β), f a ∂Measure.map (⇑g : (a : α) → β) μ = ∫⁻ (a : α), f ((g : (a : α) → β) a) ∂μ

Tactic:
g.measurableEmbedding.lintegral_map f

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.lintegral_map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
rw :
  ∫⁻ (a : α),
      f
        a ∂Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) =
    ∫⁻ (x : α) in s, f x ∂μ
rw₁ rw₂ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (x : α) in s, f x ∂μ
⊢ ∫⁻ (x : (↑s : Type u_1)), f (↑x : α) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ =
    ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]

Premises used: MeasurableEmbedding.lintegral_map, map_comap_subtype_coe, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set (↑s : Type u_1)
f : α → ℝ≥0∞
rw :
  ∫⁻ (x : (↑s : Type u_1)),
      f
        (↑x :
          α) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (μ.restrict (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)) =
    ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ
rw₁ :
  ∫⁻ (x : α) in s, f x ∂μ.restrict (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) =
    ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ
rw₂ :
  ∫⁻ (x : α) in s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ =
    ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ
rw₃ rw₄ :
  ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ =
    ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ
⊢ ∫⁻ (x : (↑s : Type u_1)) in t, f (↑x : α) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ =
    ∫⁻ (x : α) in Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x ∂μ

Tactic:
rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]

Premises used: Iff.mpr, MeasureTheory.lintegral_subtype_comap, Subtype.coe_image_subset, MeasureTheory.Measure.restrict_restrict, Set.inter_eq_right, MeasurableEmbedding.restrict_comap, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g : (a : α) → β) μ ν
rw : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂Measure.map (⇑g : (a : α) → β) μ
rw₁ rw₂ : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f ((g : (a : α) → β) a) ∂μ

Tactic:
rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
f : β → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g μ
rw₁ rw₂ : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

Tactic:
rw [← hg.map_eq, lintegral_map hf hg.measurable]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.lintegral_map
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
rw : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g μ
rw₁ rw₂ : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν

Tactic:
rw [← hg.map_eq, hge.lintegral_map]

Premises used: MeasurableEmbedding.lintegral_map, MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
s : Set β
hs : MeasurableSet s
f : β → ℝ≥0∞
hf : Measurable f
rw : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂Measure.map g μ
rw₁ rw₂ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.setLIntegral_map, MeasureTheory.MeasurePreserving.measurable
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
rw : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂Measure.map g μ
rw₁ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g (μ.restrict (g ⁻¹' s))
rw₂ rw₃ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]

Premises used: MeasurableEmbedding.restrict_map, MeasurableEmbedding.lintegral_map, MeasureTheory.MeasurePreserving.map_eq