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)
c : ℝ
x : G
hs : ¬MeasurableSet s
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have neg : 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
Tactic: simp_rw [condExpIndL1_of_not_measurableSet hs]
-- 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)
c : ℝ
x : G
hs : ¬MeasurableSet s
⊢ 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
have neg : Eq (α := ↥(Lp G 1 μ)) 0 0
Tactic: rw [smul_zero]
-- 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)
c : ℝ
x : G
hs : MeasurableSet s
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have pos : ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hμs : μ s = ∞
-- 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)
c : ℝ
x : G
hs : MeasurableSet s
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have neg : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hμs : μ s = ∞
-- 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)
c : ℝ
x : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have pos : 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
Tactic: simp_rw [condExpIndL1_of_measure_eq_top hμs]
-- 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)
c : ℝ
x : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
have pos : Eq (α := ↥(Lp G 1 μ)) 0 0
Tactic: rw [smul_zero]
-- 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)
c : ℝ
x : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
have neg : condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
Tactic: simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
-- 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
c : 𝕜
x : F
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have pos : ∀ (hs : MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hs : MeasurableSet s
-- 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
c : 𝕜
x : F
pos : ∀ (hs : MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have neg : ∀ (hs : ¬MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hs : MeasurableSet s
-- 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
c : 𝕜
x : F
hs : ¬MeasurableSet s
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have neg : 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
Tactic: simp_rw [condExpIndL1_of_not_measurableSet hs]
-- 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
c : 𝕜
x : F
hs : ¬MeasurableSet s
⊢ 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
have neg : Eq (α := ↥(Lp F 1 μ)) 0 0
Tactic: rw [smul_zero]
-- 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
c : 𝕜
x : F
hs : MeasurableSet s
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have pos : ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hμs : μ s = ∞
-- 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
c : 𝕜
x : F
hs : MeasurableSet s
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have neg : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
Tactic: by_cases hμs : μ s = ∞
-- 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
c : 𝕜
x : F
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have pos : 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
Tactic: simp_rw [condExpIndL1_of_measure_eq_top hμs]
-- 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
c : 𝕜
x : F
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
have pos : Eq (α := ↥(Lp F 1 μ)) 0 0
Tactic: rw [smul_zero]
-- 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
c : 𝕜
x : F
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)
have neg : condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
Tactic: simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]
-- 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)
x : G
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have pos : ∀ (hs : MeasurableSet s), norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
Tactic: by_cases hs : MeasurableSet s
-- 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)
x : G
pos : ∀ (hs : MeasurableSet s), norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have neg : ∀ (hs : ¬MeasurableSet s), norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
Tactic: by_cases hs : MeasurableSet s
-- 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)
x : G
hs : ¬MeasurableSet s
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have neg : norm (E := ↥(Lp G 1 μ)) 0 ≤ μ.real s * ‖x‖
Tactic: simp_rw [condExpIndL1_of_not_measurableSet hs]
-- 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)
x : G
hs : ¬MeasurableSet s
⊢ norm (E := ↥(Lp G 1 μ)) 0 ≤ μ.real s * ‖x‖
have neg : 0 ≤ μ.real s * ‖x‖
Tactic: rw [Lp.norm_zero]
-- 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)
x : G
hs : MeasurableSet s
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have pos : ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
Tactic: by_cases hμs : μ s = ∞
-- 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)
x : G
hs : MeasurableSet s
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have neg : ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
Tactic: by_cases hμs : μ s = ∞
-- 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)
x : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have pos : 0 ≤ μ.real s * ‖x‖
Tactic: rw [condExpIndL1_of_measure_eq_top hμs x, Lp.norm_zero]
-- 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)
x : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖
have neg : norm (E := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖
Tactic: rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_4
inst : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
⊢ condExpIndL1 hm μ (s ∪ t) x = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ t x)
have hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμst : μ (s ∪ t) ≠ ∞ :=
    ((measure_union_le s t).trans_lt (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
x : G
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1 hm μ (s ∪ t) x = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ t x)
have rw : condExpIndL1Fin (s := s ∪ t) hm sorry hμst x =
  HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)
Tactic: rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x,
    condExpIndL1_of_measurableSet_of_measure_ne_top ht hμt x,
    condExpIndL1_of_measurableSet_of_measure_ne_top (hs.union ht) hμst x]
-- 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
⊢ (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
have grw : (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G)
Tactic: grw [← condExpIndL1Fin_ae_eq_condExpIndSMul]
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
⊢ Eq (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ ∅) 0
have h : ∀ (x : G),
  EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
Tactic: ext x
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
have h : (↑(↑(condExpIndSMul (s := ∅) hm sorry sorry x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
Tactic: grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
h :
  (↑(↑(condExpIndSMul (s := ∅) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
have h₁ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G)
  (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
Tactic: grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
h :
  (↑(↑(condExpIndSMul (s := ∅) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₁ :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
have h₂ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G) (↑(↑0 : α →ₘ[μ] G) : α → G)
Tactic: grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
h :
  (↑(↑(condExpIndSMul (s := ∅) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₁ :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₂ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G) (↑(↑0 : α →ₘ[μ] G) : α → G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
have h₃ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) 0 (↑(↑0 : α →ₘ[μ] G) : α → G)
Tactic: grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
-- 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 α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
x : G
h :
  (↑(↑(condExpIndSMul (s := ∅) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₁ :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
h₂ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑0 : α →ₘ[μ] G) : α → G) (↑(↑0 : α →ₘ[μ] G) : α → G)
h₃ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) 0 (↑(↑0 : α →ₘ[μ] G) : α → G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ) (↑(↑((condExpInd G hm μ ∅ : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
    (↑(↑((0 : (a : G) → ↥(Lp G 1 μ)) x) : α →ₘ[μ] G) : α → G)
have h₄ : EventuallyEq.{u_1, u_4} (β := G) (ae μ) 0 0
Tactic: grw [condExpInd_ae_eq_condExpIndSMul hm MeasurableSet.empty (by simp), condExpIndSMul_empty,
    zero_apply, Lp.coeFn_zero, Lp.coeFn_zero]
-- 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 t : Set α
inst_1 : NormedSpace ℝ G
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
⊢ condExpInd G hm μ (s ∪ t) = HAdd.hAdd (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ s) (condExpInd G hm μ t)
have h : ∀ (x : G),
  Eq (α := ↥(Lp G 1 μ)) ((condExpInd G hm μ (s ∪ t) : (a : G) → ↥(Lp G 1 μ)) x : ↥(Lp G 1 μ))
    ((HAdd.hAdd (α := G →L[ℝ] ↥(Lp G 1 μ)) (condExpInd G hm μ s) (condExpInd G hm μ t) : (a : G) → ↥(Lp G 1 μ)) x :
      ↥(Lp G 1 μ))
Tactic: ext1 x
-- 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 : G
⊢ Eq (α := ↥(Lp G 1 μ)) ((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c : ↥(Lp G 1 μ))
    (indicatorConstLp (s := s) 1 ⋯ hμs c : ↥(Lp G 1 μ))
have h : (↑(↑((condExpInd G hm μ s : (a : G) → ↥(Lp G 1 μ)) c) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
  (↑(↑(indicatorConstLp (s := s) 1 sorry hμs c) : α →ₘ[μ] G) : α → G)
Tactic: ext1