awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (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) μ
⊢ 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 hgY : AEStronglyMeasurable (g ∘ Y) μ
Tactic: have hgY := (hg.comp_aemeasurable hY)
-- 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 :
  ∀ (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) μ
⊢ 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'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)
Tactic: by_cases h'X : ∀ᵐ ω ∂μ, f (X ω) = 0
-- 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 :
  ∀ (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)
⊢ 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'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)
Tactic: by_cases h'X : ∀ᵐ ω ∂μ, f (X ω) = 0
-- 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 :
  ∀ (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)
have 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)
Tactic: filter_upwards [h'X] with ω hω
-- 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 :
  ∀ (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)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have 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)
Tactic: have h' : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h'X] with ω hω
      simp [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 :
  ∀ (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)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have 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)
Tactic: by_cases h'Y : ∀ᵐ ω ∂μ, g (Y ω) = 0
-- 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 :
  ∀ (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)
⊢ 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'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)
Tactic: by_cases h'Y : ∀ᵐ ω ∂μ, g (Y ω) = 0
-- 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 :
  ∀ (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)
have 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)
Tactic: filter_upwards [h'Y] with ω hω
-- 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 :
  ∀ (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)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have 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)
Tactic: have h' : ∀ᵐ ω ∂μ, B (f (X ω)) (g (Y ω)) = 0 := by
      filter_upwards [h'Y] with ω hω
      simp [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 :
  ∀ (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‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
have 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
Tactic: rw [← toReal_le_toReal]
-- 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 :
  ∀ (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
⊢ (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
have ha : (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≠ ∞
Tactic: rw [← toReal_le_toReal]
-- 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 :
  ∀ (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‖ₑ ≠ ∞
⊢ (↑c : ℝ≥0∞) * ‖x‖ₑ * ‖y‖ₑ ≤ enorm.{u_7} (E := G) ((((B : (a : E) → F →L[𝕜] G) x : F →L[𝕜] G) : (a : F) → G) y : G)
have hb : 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]
-- 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 :
  ∀ (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)
    (((B : (a : E) → F →L[𝕜] G) (∫ (ω : Ω), f (X ω) ∂μ) : (a : F) → G) (∫ (ω : Ω), g (Y ω) ∂μ) : G)
have 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)
Tactic: have hB x y : c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ := by
    rw [← toReal_le_toReal]
    · simpa using hB x y
    all_goals finiteness