-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_mk
    {Ω} {mΩ : MeasurableSpace Ω} (X : Ω → β) {μ : Measure Ω} {f : Ω → F} (hf_int : Integrable f μ) :
    Integrable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω))

Proof state:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Tactic:
rw [Measure.map_of_not_aemeasurable]

Result:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x => f x.2) 0

case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω => (X ω, ω)) μ

Proof state:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (fun ω => (X ω, ω)) μ

Tactic:
contrapose! hX

Result:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable (fun ω => (X ω, ω)) μ
⊢ AEMeasurable X μ

Proof state:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Tactic:
have hf := hf_int.1.comp_snd_map_prod_mk X (mΩ := mΩ) (mβ := mβ)

Result:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Proof state:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ HasFiniteIntegral (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Tactic:
rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prod_mk aemeasurable_id)]

Result:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ⊤

Proof state:
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Tactic:
by_cases hX : AEMeasurable X μ

Result:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Proof state:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Tactic:
refine ⟨hf, ?_⟩

Result:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ HasFiniteIntegral (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)

Proof state:
case pos
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf : AEStronglyMeasurable (fun x => f x.2) (Measure.map (fun ω => (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ⊤

Tactic:
exact hf_int.2

Result:
no goals

Proof state:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ Integrable (fun x => f x.2) 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
β : Type u_2
F : Type u_4
inst✝ : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable (fun ω => (X ω, ω)) μ
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.comp_aemeasurable hX

Result:
no goals