awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : ContinuousENorm F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
⊢ Integrable Y μ

Tactic:
hXY.symm.integrable_left_of_integrable_op (Function.swap B) c hc (fun y x ↦ ?_)
    h'XY hY hX h'X

Premises used: Function.swap, ProbabilityTheory.IndepFun.symm, ProbabilityTheory.IndepFun.integrable_left_of_integrable_op
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : ContinuousENorm F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
refine : ∀ (y : F) (x : E), (↑c : ℝ≥0∞) * ‖y‖ₑ * ‖x‖ₑ ≤ ‖Function.swap (φ := fun (a : E) (a_1 : F) ↦ G) B y x‖ₑ
⊢ Integrable Y μ

Tactic:
refine hXY.symm.integrable_left_of_integrable_op (Function.swap B) c hc (fun y x ↦ ?_)
    h'XY hY hX h'X

Premises used: Function.swap, ProbabilityTheory.IndepFun.symm, ProbabilityTheory.IndepFun.integrable_left_of_integrable_op
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
inst_3 : TopologicalSpace F
inst_4 : ContinuousENorm F
inst_5 : MeasurableSpace F
inst_6 : OpensMeasurableSpace F
inst_7 : TopologicalSpace G
inst_8 : ContinuousENorm G
X : Ω → E
Y : Ω → F
hXY : X ⟂ᵢ[μ] Y
B : E → F → G
c : ℝ≥0
hc : c ≠ 0
hB : ∀ (x : E) (y : F), (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ
h'XY : Integrable.{u_7, u_1} (ε := G) (fun (ω : Ω) ↦ B (X ω) (Y ω)) μ
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
h'X : ¬X =ᶠ[ae μ] 0
y : F
x : E
grw : (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ ‖Function.swap (φ := fun (a : E) (a_1 : F) ↦ G) B y x‖ₑ
grw₁ grw₂ : ‖B x y‖ₑ ≤ ‖B x y‖ₑ
⊢ (↑c : ℝ≥0∞) * ‖y‖ₑ * ‖x‖ₑ ≤ ‖Function.swap (φ := fun (a : E) (a_1 : F) ↦ G) B y x‖ₑ

Tactic:
grw [mul_right_comm, hB]

Premises used: mul_right_comm
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
pos :
  ∀ (h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0),
    Eq.{u_7 + 1} (α := G)
      (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
neg :
  ∀ (h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0),
    Eq.{u_7 + 1} (α := G)
      (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
by_cases h : ∀ᵐ ω ∂μ, f (X ω) = 0
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h₁ :
  ∀ (ω : Ω) (hω : f (X ω) = 0),
    Eq.{u_7 + 1} (α := G) ((((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) : G) (0 : G)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq.{u_7 + 1} (α := G) ((((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) : G) (0 : G)

Tactic:
filter_upwards [h] with ω hω
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
ω : Ω
hω : f (X ω) = 0
⊢ Eq.{u_7 + 1} (α := G) ((((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) : G) (0 : G)

Tactic:
simp [hω]
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq.{u_7 + 1} (α := G) ((((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) : G) (0 : G)

Tactic:
have h1 : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h] with ω hω
      simp [hω]
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h1 :
  ∀ᵐ (ω : Ω) ∂μ,
    Eq.{u_7 + 1} (α := G) ((((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) : G) (0 : G)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
simp [integral_congr_ae h1, integral_congr_ae h]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E F
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this :
  let this := borel E;
  BorelSpace E
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize E F
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ :=
    (hf.comp_aemeasurable hX).isProbabilityMeasure_of_indepFun (f ∘ X) (g ∘ Y) h
      (hXY.comp₀ hX hY hf.1.aemeasurable hg.1.aemeasurable)
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : MeasurableSpace F := borel F
this_4 : BorelSpace F
this : IsProbabilityMeasure μ
⊢ AEMeasurable (β := 𝓧 × 𝓨) (fun (ω : Ω) ↦ (X ω, Y ω)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : MeasurableSpace F := borel F
this_4 : BorelSpace F
this : IsProbabilityMeasure μ
neg :
  AEStronglyMeasurable (β := G) (m₀ := Prod.instMeasurableSpace)
    (fun (z : 𝓧 × 𝓨) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ)
⊢ Eq.{u_7 + 1} (α := G) (∫ (ω : Ω), (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω)) ∂μ : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)

Tactic:
rw [← integral_map (f := fun z ↦ B (f z.1) (g z.2)) (φ := fun ω ↦ (X ω, Y ω)) (by fun_prop),
    hXY.map_prod_eq_prod_map_map hX hY, integral_prod_bilin _ hf hg, integral_map hX hf.1,
    integral_map hY hg.1]

Premises used: MeasureTheory.integral_prod_bilin, MeasureTheory.integral_map, And.left, ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : MeasurableSpace F := borel F
this_4 : BorelSpace F
this : IsProbabilityMeasure μ
neg :
  AEStronglyMeasurable (β := G) (m₀ := Prod.instMeasurableSpace)
    (fun (z : 𝓧 × 𝓨) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (Measure.prod (Measure.map X μ) (Measure.map Y μ))
⊢ AEStronglyMeasurable (β := G) (m₀ := Prod.instMeasurableSpace)
    (fun (z : 𝓧 × 𝓨) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (Measure.map (fun (ω : Ω) ↦ (X ω, Y ω)) μ)

Tactic:
rw [hXY.map_prod_eq_prod_map_map hX hY]

Premises used: ProbabilityTheory.IndepFun.map_prod_eq_prod_map_map
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : MeasurableSpace F := borel F
this_4 : BorelSpace F
this : IsProbabilityMeasure μ
⊢ Continuous (X := E × F) (Y := G)
    (Function.uncurry fun (x1 : E) (x2 : F) ↦ (((B : (a : E) → F →L[𝕜] G) x1 : F →L[𝕜] G) : (a : F) → G) x2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
hg : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : MeasurableSpace F := borel F
this_4 : BorelSpace F
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (β := G) (m₀ := Prod.instMeasurableSpace)
    (fun (z : 𝓧 × 𝓨) ↦ (((B : (a : E) → F →L[𝕜] G) (f z.1) : F →L[𝕜] G) : (a : F) → G) (g z.2))
    (Measure.prod (Measure.map X μ) (Measure.map Y μ))

Tactic:
exact Continuous.comp_aestronglyMeasurable₂ (g := (B · ·)) (by fun_prop)
    hf.1.comp_fst hg.1.comp_snd

Premises used: And.left, MeasureTheory.AEStronglyMeasurable.comp_fst, MeasureTheory.AEStronglyMeasurable.comp_snd, Continuous.comp_aestronglyMeasurable₂
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ) * ‖x‖ * ‖y‖ ≤ norm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E F
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ) * ‖x‖ * ‖y‖ ≤ norm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
this :
  let this := borel E;
  BorelSpace E
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize E F
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ) * ‖x‖ * ‖y‖ ≤ norm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
⊢ (f ∘ X) ⟂ᵢ[μ] g ∘ Y

Tactic:
have hfXgY := (hXY.comp₀ hX hY hf.aemeasurable hg.aemeasurable)
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
inst_6 : CompleteSpace E
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : CompleteSpace F
inst_11 : NormedAddCommGroup G
inst_12 : NormedSpace ℝ G
inst_13 : NormedSpace 𝕜 G
inst_14 : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := inst_1) f (Measure.map X μ)
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
c : ℝ≥0
hc : c ≠ 0
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ) * ‖x‖ * ‖y‖ ≤ norm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
this_2 : MeasurableSpace F := borel F
this_3 : BorelSpace F
hfXgY : (f ∘ X) ⟂ᵢ[μ] g ∘ Y
⊢ AEStronglyMeasurable (f ∘ X) μ

Tactic:
have hfX := (hf.comp_aemeasurable hX)