awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h₂ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) sorry) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h₃ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₃ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h₄ : (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ)) (condExpIndSMul (s := s) hm hs hμs x) (condExpIndSMul (s := s) hm hs hμs y)) :
        α →ₘ[μ] G) :
    α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x y : G
h :
  (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) : α → G)
h₃ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
h₄ :
  (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ)) (condExpIndSMul (s := s) hm hs hμs x) (condExpIndSMul (s := s) hm hs hμs y)) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs (x + y)) : α →ₘ[μ] G) : α → G) ⋯) : α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) ⋯ +
              MemLp.toLp (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) ⋯) :
          α →ₘ[μ] G) :
      α → G)
have h₅ : (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
    (↑(↑(condExpIndSMul (s := s) hm hs hμs y) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
    Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
have h : (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
have h : (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
have h₁ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
have h₂ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
have h₃ : (↑(↑(HSMul.hSMul (β := ↥(Lp G 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ
x : G
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
h₃ :
  (↑(↑(HSMul.hSMul (β := ↥(Lp G 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] G) : α → G)
have h₄ : c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
have h : (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
have h : (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
have h₁ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
have h₂ : (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
have h₃ : (↑(↑(HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_6
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
inst_4 : NormedSpace ℝ F
inst_5 : SMulCommClass ℝ 𝕜 F
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : 𝕜
x : F
h :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₁ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₂ :
  (↑(↑(condExpIndSMul (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
h₃ :
  (↑(↑(HSMul.hSMul (β := ↥(Lp F 2 μ)) c (condExpIndSMul (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(condExpIndL1Fin (s := s) hm hs hμs (c • x)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)) : α →ₘ[μ] F) : α → F)
have h₄ : c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndSMul_smul, Lp.coeFn_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖
have rw : ∫⁻ (x_1 : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖ₑ ∂μ ≤
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal ‖x‖)
Tactic: rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), measureReal_def,
    ← ENNReal.toReal_mul,
    ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),
    ofReal_integral_norm_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
rw :
  ∫⁻ (x_1 : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) x_1‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal ‖x‖)
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖
have rw₁ : Integrable (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) μ
Tactic: rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), measureReal_def,
    ← ENNReal.toReal_mul,
    ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),
    ofReal_integral_norm_eq_lintegral_enorm]