awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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) ∂μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
have neg : ∀ (hg : ¬AEMeasurable g μ), ∫⁻ (a : β), f a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Tactic: by_cases hg : AEMeasurable g μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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) ∂μ
have pos : ⨆ (g_1 : β → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f), ∫⁻ (a : β), g_1 a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Tactic: rw [← iSup_lintegral_measurable_le_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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) ∂μ
have pos : ∀ (i : β → ℝ≥0∞) (hi : Measurable i) (h'i : i ≤ f), ∫⁻ (a : β), i a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Tactic: refine iSup₂_le fun i hi => iSup_le fun h'i => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 a ∂Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
have pos : ∫⁻ (a : α), i (g a) ∂μ ≤ ∫⁻ (a : α), f (g a) ∂μ
Tactic: rw [lintegral_map' hi.aemeasurable hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
have rw : ∫⁻ (y : β), f y ∂Measure.map g (μ.restrict (g ⁻¹' s)) = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
Tactic: rw [restrict_map hg hs, lintegral_map hf hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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) ∂μ
⊢ ∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
have rw₁ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
Tactic: rw [restrict_map hg hs, lintegral_map hf hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun (x : β) ↦ c) (f a) ∂μ =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : ∫⁻ (a : β), s.indicator (fun (x : β) ↦ c) a ∂Measure.map f μ =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : β) ↦ c) (f a) ∂μ =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₁ : HMul.hMul (β := ℝ≥0∞) c (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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∞)
⊢ ∫⁻ (a : α), s.indicator (fun (x : β) ↦ c) (f a) ∂μ =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₂ : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
have 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 μ)
Tactic: rw [lintegral, lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ)
have 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 μ
Tactic: refine le_antisymm (iSup₂_le fun f₀ hf₀ => ?_) (iSup₂_le fun f₀ hf₀ => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
⊢ 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 μ)
have 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 μ)
Tactic: refine le_antisymm (iSup₂_le fun f₀ hf₀ => ?_) (iSup₂_le fun f₀ hf₀ => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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₀.lintegral (Measure.map g μ) ≤
    ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ
have refine_1 : (f₀.comp g sorry).lintegral μ ≤
  ⨆ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (hypothesis)
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 ⋯).lintegral μ ≤
    ⨆ (g_1 : SimpleFunc α ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f (g a)), g_1.lintegral μ
have this : (⇑(f₀.comp g sorry) : (a : α) → ℝ≥0∞) ≤ f ∘ g
Tactic: have : (f₀.comp g hg.measurable : α → ℝ≥0∞) ≤ f ∘ g := fun x => hf₀ (g x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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)
⊢ f₀.lintegral μ ≤
    ⨆ (g_1 : SimpleFunc β ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : β) → ℝ≥0∞) (⇑g_1 : (a : β) → ℝ≥0∞) fun (a : β) ↦ f a), g_1.lintegral (Measure.map g μ)
have refine_2 : ∫⁻ (a : β), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) a ∂Measure.map g μ ≤ ∫⁻ (a : β), f a ∂Measure.map g μ
Tactic: rw [← f₀.extend_comp_eq hg (const _ 0), ← SimpleFunc.lintegral_map, ←
      SimpleFunc.lintegral_eq_lintegral, ← lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
have refine_2 : ∀ (x : α), (f₀.extend g hg (const β 0) : (a : β) → ℝ≥0∞) (g x) ≤ f (g x)
Tactic: refine lintegral_mono_ae (hg.ae_map_iff.2 <| Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : (↑s : Type u_1)), f (↑x : α) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ =
    ∫⁻ (x : α) in s, f x ∂μ
have 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 ∂μ
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 ∂μ
⊢ ∫⁻ (x : (↑s : Type u_1)), f (↑x : α) ∂Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ =
    ∫⁻ (x : α) in s, f x ∂μ
have rw₁ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (x : α) in s, f x ∂μ
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set (↑s : Type u_1)
f : α → ℝ≥0∞
⊢ ∫⁻ (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 ∂μ
have 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 ∂μ
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 ∂μ
⊢ ∫⁻ (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 ∂μ
have 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 ∂μ
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 ∂μ
⊢ ∫⁻ (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 ∂μ
have 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 ∂μ
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 ∂μ
⊢ ∫⁻ (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 ∂μ
have 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 ∂μ
Tactic: rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
    restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g : (a : α) → β) μ ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f ((g : (a : α) → β) a) ∂μ
have rw : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂Measure.map (⇑g : (a : α) → β) μ
Tactic: rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 : α) → β) μ
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f ((g : (a : α) → β) a) ∂μ
have rw₁ : ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : β), f a ∂ν
Tactic: rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
f : β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
have rw : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g μ
Tactic: rw [← hg.map_eq, lintegral_map hf hg.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
have rw₁ : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (a : α), f (g a) ∂μ
Tactic: rw [← hg.map_eq, lintegral_map hf hg.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
have rw : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g μ
Tactic: rw [← hg.map_eq, hge.lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
⊢ ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
have rw₁ : ∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (a : α), f (g a) ∂μ
Tactic: rw [← hg.map_eq, hge.lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
have rw : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂Measure.map g μ
Tactic: rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
have rw₁ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
Tactic: rw [← hg.map_eq, setLIntegral_map hs hf hg.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
have rw : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂Measure.map g μ
Tactic: rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 μ
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
have rw₁ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β), f b ∂Measure.map g (μ.restrict (g ⁻¹' s))
Tactic: rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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))
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
have rw₂ : ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ
Tactic: rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 α
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
have rw : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' g '' s, f (g a) ∂μ
Tactic: rw [← hg.setLIntegral_comp_preimage_emb hge, Set.preimage_image_eq _ hge.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Map (goal)
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 s, f (g a) ∂μ = ∫⁻ (a : α) in g ⁻¹' g '' s, f (g a) ∂μ
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
have rw₁ : ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (a : α) in s, f (g a) ∂μ
Tactic: rw [← hg.setLIntegral_comp_preimage_emb hge, Set.preimage_image_eq _ hge.injective]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (a : α), g a ∂μ
have rcases : ∀ (φ : α → ℝ≥0∞) (hφm : Measurable φ) (hφ_le : φ ≤ f) (hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ),
  ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (a : α), g a ∂μ
Tactic: rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), f x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) =
    ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞)
have rw : ∫⁻ (a : α), φ a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) =
  ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞)
Tactic: rw [hφ_eq]