awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hfX : AEStronglyMeasurable (f ∘ X) μ
⊢ AEStronglyMeasurable (g ∘ Y) μ

Tactic:
have hgY := (hg.comp_aemeasurable hY)
-- 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
pos :
  ∀ (h'X : ∀ᵐ (ω : Ω) ∂μ, 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'X : ¬∀ᵐ (ω : Ω) ∂μ, 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'X : ∀ᵐ ω ∂μ, 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ∀ᵐ (ω : Ω) ∂μ, 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'X] 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ∀ᵐ (ω : Ω) ∂μ, 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ∀ᵐ (ω : Ω) ∂μ, 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 h' : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h'X] 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h' :
  ∀ᵐ (ω : Ω) ∂μ,
    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 h'X, 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
pos :
  ∀ (h'Y : ∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 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'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 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'Y : ∀ᵐ ω ∂μ, g (Y ω) = 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
h :
  ∀ (ω : Ω) (hω : g (Y ω) = 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'Y] 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
ω : Ω
hω : g (Y ω) = 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 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 h' : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h'Y] 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
h' :
  ∀ᵐ (ω : Ω) ∂μ,
    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 h'Y, 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 : 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
rw :
  ((↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ).toReal ≤
    (enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)).toReal
ha : (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≠ ∞
hb : enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G) ≠ ∞
⊢ (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)

Tactic:
rw [← toReal_le_toReal]

Premises used: ENNReal.toReal_le_toReal
-- 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
⊢ ((↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ).toReal ≤
    (enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)).toReal

Tactic:
simpa using hB x y
-- 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
⊢ (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≠ ∞

Tactic:
finiteness
-- 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
hfX : AEStronglyMeasurable (f ∘ X) μ
hgY : AEStronglyMeasurable (g ∘ Y) μ
h'X : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
h'Y : ¬∀ᵐ (ω : Ω) ∂μ, g (Y ω) = 0
x : E
y : F
⊢ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G) ≠ ∞

Tactic:
finiteness