awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → 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)
have pos : ∀
  (h :
    Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (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: by_cases h : Integrable (fun ω ↦ B (f (X ω)) (g (Y ω))) μ
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
pos :
  ∀
    (h :
      Integrable.{u_7, u_1} (ε := G)
        (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (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)
⊢ 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)
have neg : ∀
  (h :
    ¬Integrable.{u_7, u_1} (ε := G)
        (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (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: by_cases h : Integrable (fun ω ↦ B (f (X ω)) (g (Y ω))) μ
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (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)
have h1 : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
Tactic: have h1 : Integrable f (μ.map X) := (integrable_map_measure hf hX).2 <|
      hfXgY.integrable_left_of_integrable_op (B · ·) c hc hB h hfX hgY h'Y
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  Integrable.{u_7, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
h1 : @Integrable _ _ _ _ inst_1 f (Measure.map X μ)
⊢ 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)
have h2 : @Integrable _ _ _ _ inst_2 g (Measure.map Y μ)
Tactic: have h2 : Integrable g (μ.map Y) := (integrable_map_measure hg hY).2 <|
      hfXgY.integrable_right_of_integrable_op (B · ·) c hc hB h hfX hgY h'X
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (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)
have neg : Eq.{u_7 + 1} (α := G) (0 : G)
  (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
Tactic: rw [integral_undef h]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
⊢ Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have neg : ∀ (h : ¬Integrable.{u_5, u_1} (ε := E) (fun (ω : Ω) ↦ f (X ω)) μ),
  Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
Tactic: obtain h | h : ¬(Integrable (fun ω ↦ f (X ω)) μ) ∨ ¬(Integrable (fun ω ↦ g (Y ω)) μ) :=
      not_and_or.1 fun ⟨HX, HY⟩ ↦ h (hfXgY.integrable_bilin HX HY B)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
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_1 :
  ∀ (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
hB :
  ∀ (x : E) (y : F),
    (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
h :
  ¬Integrable.{u_7, u_1} (ε := G)
      (fun (ω : Ω) ↦ (((B : (a : E) → F →L[𝕜] G) (f (X ω)) : F →L[𝕜] G) : (a : F) → G) (g (Y ω))) μ
neg :
  ∀ (h : ¬Integrable.{u_5, u_1} (ε := E) (fun (ω : Ω) ↦ f (X ω)) μ),
    Eq.{u_7 + 1} (α := G) (0 : G)
      (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
⊢ Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have neg₁ : ∀ (h : ¬Integrable.{u_6, u_1} (ε := F) (fun (ω : Ω) ↦ g (Y ω)) μ),
  Eq.{u_7 + 1} (α := G) (0 : G)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
Tactic: obtain h | h : ¬(Integrable (fun ω ↦ f (X ω)) μ) ∨ ¬(Integrable (fun ω ↦ g (Y ω)) μ) :=
      not_and_or.1 fun ⟨HX, HY⟩ ↦ h (hfXgY.integrable_bilin HX HY B)
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
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 μ)
⊢ ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
have pos : ∀ (hE : CompleteSpace E),
  ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
inst_1 : MeasurableSpace 𝓧
inst_2 : MeasurableSpace 𝓨
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace 𝕜 E
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → 𝕜
g : 𝓨 → E
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 μ)
pos :
  ∀ (hE : CompleteSpace E),
    ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
      HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
⊢ ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E),
  ∫ (ω : Ω), f (X ω) • g (Y ω) ∂μ =
    HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (ω : Ω), f (X ω) ∂μ) (∫ (ω : Ω), g (Y ω) ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have pos : ∀ (hE : CompleteSpace E),
  ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
pos :
  ∀ (hE : CompleteSpace E),
    ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
have neg : ∀ (hE : ¬CompleteSpace E),
  ∫ (x : Ω), (X • Y) x ∂μ = HSMul.hSMul.{u_2, u_5, u_5} (α := 𝕜) (β := E) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ f ⟂ᵢ[μ] g ↔
    ∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
have refine : (∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
  f ⟂ᵢ[μ] g
Tactic: refine ⟨fun hfg _ _ hφ hψ _ _ => hfg.integral_comp_mul_comp
      hfm.aemeasurable hgm.aemeasurable hφ.aestronglyMeasurable hψ.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
⊢ (∀ {φ : β → ℝ} {ψ : β' → ℝ},
      Measurable φ →
        Measurable ψ →
          Integrable (φ ∘ f) μ →
            Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
    f ⟂ᵢ[μ] g
have rw : (∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)) →
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞)
Tactic: rw [IndepFun_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
h :
  ∀ {φ : β → ℝ} {ψ : β' → ℝ},
    Measurable φ →
      Measurable ψ →
        Integrable (φ ∘ f) μ →
          Integrable (ψ ∘ g) μ → integral μ (φ ∘ f * ψ ∘ g) = integral μ (φ ∘ f) * integral μ (ψ ∘ g)
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A ∩ g ⁻¹' B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞)
have h₁ : integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
  HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))
Tactic: specialize
    h (measurable_one.indicator hA) (measurable_one.indicator hB)
      ((integrable_const 1).indicator (hfm.comp measurable_id hA))
      ((integrable_const 1).indicator (hgm.comp measurable_id hB))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
β : Type u_3
β' : Type u_4
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f : Ω → β
g : Ω → β'
hfm : Measurable f
hgm : Measurable g
A : Set β
hA : MeasurableSet A
B : Set β'
hB : MeasurableSet B
h :
  integral μ (HMul.hMul (α := Ω → ℝ) (A.indicator 1 ∘ f) (B.indicator 1 ∘ g)) =
    HMul.hMul (α := ℝ) (integral μ (A.indicator 1 ∘ f)) (integral μ (B.indicator 1 ∘ g))
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A ∩ g ⁻¹' B) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞)
have rwa : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' B) : ℝ≥0∞) ≠
  ∞
Tactic: rwa [← toReal_eq_toReal_iff' (measure_ne_top μ _), toReal_mul, ← measureReal_def,
    ← measureReal_def, ← measureReal_def, ← integral_indicator_one ((hfm hA).inter (hgm hB)),
    ← integral_indicator_one (hfm hA), ← integral_indicator_one (hgm hB), Set.inter_indicator_one]
-- Lean 4 proof step from Mathlib.Probability.Independence.Integration (goal)
Goal:
Ω : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst_1 : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun (β := 𝓧) X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (m₀ := m𝓧 i) (f i) (Measure.map (X i) μ)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : Ω), (∏ i : ι, f i ∘ X i) x ∂μ) (∏ i : ι, ∫ (x : Ω), (f i ∘ X i) x ∂μ)
have h : ∀ (x : Ω), Eq.{u_2 + 1} (α := 𝕜) ((∏ i : ι, f i ∘ X i) x) (∏ i : ι, f i (X i x))
Tactic: convert! hX.integral_fun_prod_comp mX hf
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
⊢ iIndepSets π κ μ ↔ iIndepSets π η μ
have h₁ : ∀ (a : Finset ι) (a_1 : ι → Set Ω),
  (∀ i ∈ a, a_1 i ∈ π i) →
    ((∀ᵐ (a_3 : α) ∂μ,
        Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
          (∏ i ∈ a, (((κ : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞)) ↔
      ∀ᵐ (a_3 : α) ∂μ,
        Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ a, a_1 i) : ℝ≥0∞)
          (∏ i ∈ a, (((η : (a : α) → Measure Ω) a_3 : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (a_1 i) : ℝ≥0∞))
Tactic: peel 3