awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
have rwa : ∀
  (h :
    Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
      (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))),
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: rwa [← hs_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have h_right : Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
  (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: have h_right : Tendsto (fun i => ∫ x in S i ∩ s, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) := by
    have h :=
      tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
        (L1.integrable_coeFn f).integrableOn
    rwa [← hs_eq] at h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
have h : Tendsto.{0, u_3} (β := F')
  (fun (i : ℕ) ↦
    ∫ (x : α) in S i ∩ s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
  atTop
  (𝓝
    (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: have h := tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
      (L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h :
  Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in ⋃ (n : ℕ), S n ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
have rwa : ∀
  (h :
    Tendsto.{0, u_3} (β := F')
      (fun (i : ℕ) ↦
        ∫ (x : α) in S i ∩ s,
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
      atTop
      (𝓝
        (∫ (x : α) in s,
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))),
  Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: rwa [← hs_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have h_left : Tendsto.{0, u_3} (β := F')
  (fun (i : ℕ) ↦
    ∫ (x : α) in S i ∩ s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
  atTop
  (𝓝 (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: have h_left : Tendsto (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) atTop
      (𝓝 (∫ x in s, condExpL1CLM F' hm μ f x ∂μ)) := by
    have h := tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
      (L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn
    rwa [← hs_eq] at h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h_left :
  Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)
have h_left₁ : Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
  (𝓝 (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
Tactic: rw [h_eq_forall] at h_left
Cleared hypotheses: h_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ
have refine_1 : ∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (fun (f : ↥(Lp F' 1 μ)) ↦
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
    (↑(simpleFunc.indicatorConst 1 (s := s) hs sorry c) : ↥(Lp F' 1 μ))
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ) ?_ ?_ ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
refine_1 :
  ∀ (c : F') {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        AEStronglyMeasurable.{u_1, u_3} (β := F')
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
      (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 μ))
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ
have refine_2 : ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
  Disjoint (Function.support f) (Function.support g) →
    (fun (f : ↥(Lp F' 1 μ)) ↦
          AEStronglyMeasurable.{u_1, u_3} (β := F')
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
        (MemLp.toLp f hf) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp g hg) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp f hf + MemLp.toLp g hg)
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ) ?_ ?_ ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
refine_1 :
  ∀ (c : F') {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        AEStronglyMeasurable.{u_1, u_3} (β := F')
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
      (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 μ))
refine_2 :
  ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp f hf) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
              AEStronglyMeasurable.{u_1, u_3} (β := F')
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
            (MemLp.toLp g hg) →
          (fun (f : ↥(Lp F' 1 μ)) ↦
              AEStronglyMeasurable.{u_1, u_3} (β := F')
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
            (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ
have refine_3 : IsClosed (X := ↥(Lp F' 1 μ))
  {f : ↥(Lp F' 1 μ) |
    (fun (f : ↥(Lp F' 1 μ)) ↦
        AEStronglyMeasurable.{u_1, u_3} (β := F')
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
      f}
Tactic: refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
    (fun f : α →₁[μ] F' => AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ) ?_ ?_ ?_ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 μ))) :
          α →ₘ[μ] F') :
      α → F')
    μ
have refine_1 : AEStronglyMeasurable.{u_1, u_3} (β := F')
  (↑(↑((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c) : α →ₘ[μ] F') : α → F') μ
Tactic: rw [condExpL1CLM_indicatorConst hs hμs.ne c]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hfm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf)) : α →ₘ[μ] F') : α → F') μ
hgm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg)) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf + MemLp.toLp g hg)) : α →ₘ[μ] F') :
      α → F')
    μ
have refine_2 : AEStronglyMeasurable
  (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf) : ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg) : ↥(Lp F' 1 μ))) :
        α →ₘ[μ] F') :
    α → F')
  μ
Tactic: rw [(condExpL1CLM F' hm μ).map_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
⊢ IsClosed (X := ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      (fun (f : ↥(Lp F' 1 μ)) ↦
          AEStronglyMeasurable.{u_1, u_3} (β := F')
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
        f}
have this : Eq (α := Set ↥(Lp F' 1 μ))
  {f : ↥(Lp F' 1 μ) |
    AEStronglyMeasurable.{u_1, u_3} (β := F')
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
  (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
Tactic: have : {f : Lp F' 1 μ | AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ} =
        condExpL1CLM F' hm μ ⁻¹' {f | AEStronglyMeasurable[m] f μ} := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
this :
  Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
⊢ IsClosed (X := ↥(Lp F' 1 μ))
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
have refine_3 : IsClosed (X := ↥(Lp F' 1 μ)) {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ}
Tactic: refine IsClosed.preimage (condExpL1CLM F' hm μ).continuous ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (↑f : ↥(Lp F' 1 μ)) = (↑f : ↥(Lp F' 1 μ))
have hfg : f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
Tactic: have hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g := by
    simp only [g, LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
inst_3 : CompleteSpace F'
f : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (↑f : ↥(Lp F' 1 μ)) = (↑f : ↥(Lp F' 1 μ))
have rw : Eq (α := ↥(Lp F' 1 μ))
  ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          g) :
      ↥(Lp F' 1 μ)))
  (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
        g) :
    ↥(Lp F' 1 μ))
Tactic: rw [hfg]