awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
pos :
  ∀ (hs : MeasurableSet s),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
neg :
  ∀ (hs : ¬MeasurableSet s),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : ¬MeasurableSet s
neg : 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)

Tactic:
simp_rw [condExpIndL1_of_not_measurableSet hs]

Premises used: MeasureTheory.condExpIndL1_of_not_measurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : ¬MeasurableSet s
neg neg₁ : Eq (α := ↥(Lp G 1 μ)) 0 0
⊢ 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
neg :
  ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)

Tactic:
by_cases hμs : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)

Tactic:
simp_rw [condExpIndL1_of_measure_eq_top hμs]

Premises used: MeasureTheory.condExpIndL1_of_measure_eq_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos pos₁ : Eq (α := ↥(Lp G 1 μ)) 0 0
⊢ 0 = HAdd.hAdd (α := ↥(Lp G 1 μ)) 0 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
neg :
  condExpIndL1Fin (s := s) hm hs hμs (x + y) =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)
⊢ condExpIndL1 hm μ s (x + y) = HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1 hm μ s y)

Tactic:
simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]

Premises used: MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (x + y) =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)

Tactic:
condExpIndL1Fin_add hs hμs x y

Premises used: MeasureTheory.condExpIndL1Fin_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 y : G
hs : MeasurableSet s
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (x + y) =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := s) hm hs hμs y)

Tactic:
exact condExpIndL1Fin_add hs hμs x y

Premises used: MeasureTheory.condExpIndL1Fin_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
pos : ∀ (hs : MeasurableSet s), condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)
neg : ∀ (hs : ¬MeasurableSet s), 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)

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg : 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_not_measurableSet hs]

Premises used: MeasureTheory.condExpIndL1_of_not_measurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg neg₁ : Eq (α := ↥(Lp G 1 μ)) 0 0
⊢ 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
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)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
by_cases hμs : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
pos : 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_measure_eq_top hμs]

Premises used: MeasureTheory.condExpIndL1_of_measure_eq_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
pos pos₁ : Eq (α := ↥(Lp G 1 μ)) 0 0
⊢ 0 = HSMul.hSMul (β := ↥(Lp G 1 μ)) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
neg :
  condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]

Premises used: MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
condExpIndL1Fin_smul hs hμs c x

Premises used: MeasureTheory.condExpIndL1Fin_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp G 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
exact condExpIndL1Fin_smul hs hμs c x

Premises used: MeasureTheory.condExpIndL1Fin_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
neg : ∀ (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)

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg : 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_not_measurableSet hs]

Premises used: MeasureTheory.condExpIndL1_of_not_measurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg neg₁ : Eq (α := ↥(Lp F 1 μ)) 0 0
⊢ 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
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)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
by_cases hμs : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
pos : 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_measure_eq_top hμs]

Premises used: MeasureTheory.condExpIndL1_of_measure_eq_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
pos pos₁ : Eq (α := ↥(Lp F 1 μ)) 0 0
⊢ 0 = HSMul.hSMul (β := ↥(Lp F 1 μ)) c 0

Tactic:
rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
neg :
  condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)
⊢ condExpIndL1 hm μ s (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1 hm μ s x)

Tactic:
simp_rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs]

Premises used: MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
condExpIndL1Fin_smul' hs hμs c x

Premises used: MeasureTheory.condExpIndL1Fin_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ condExpIndL1Fin (s := s) hm hs hμs (c • x) = HSMul.hSMul (β := ↥(Lp F 1 μ)) c (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
exact condExpIndL1Fin_smul' hs hμs c x

Premises used: MeasureTheory.condExpIndL1Fin_smul'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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‖
neg : ∀ (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‖

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg : norm (E := ↥(Lp G 1 μ)) 0 ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖

Tactic:
simp_rw [condExpIndL1_of_not_measurableSet hs]

Premises used: MeasureTheory.condExpIndL1_of_not_measurableSet
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
neg : 0 ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) 0 ≤ μ.real s * ‖x‖

Tactic:
rw [Lp.norm_zero]

Premises used: MeasureTheory.Lp.norm_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ 0 ≤ μ.real s * ‖x‖

Tactic:
mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Premises used: mul_nonneg, ENNReal.toReal_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ 0 ≤ μ.real s * ‖x‖

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Premises used: mul_nonneg, ENNReal.toReal_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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‖
neg :
  ∀ (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‖

Tactic:
by_cases hμs : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
pos : 0 ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖

Tactic:
rw [condExpIndL1_of_measure_eq_top hμs x, Lp.norm_zero]

Premises used: MeasureTheory.Lp.norm_zero, MeasureTheory.condExpIndL1_of_measure_eq_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ 0 ≤ μ.real s * ‖x‖

Tactic:
mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Premises used: mul_nonneg, ENNReal.toReal_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
⊢ 0 ≤ μ.real s * ‖x‖

Tactic:
exact mul_nonneg ENNReal.toReal_nonneg (norm_nonneg _)

Premises used: mul_nonneg, ENNReal.toReal_nonneg, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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∞)
neg : norm (E := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖
⊢ norm (E := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) ≤ μ.real s * ‖x‖

Tactic:
rw [condExpIndL1_of_measurableSet_of_measure_ne_top hs hμs x]

Premises used: MeasureTheory.condExpIndL1_of_measurableSet_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖

Tactic:
norm_condExpIndL1Fin_le hs hμs x

Premises used: MeasureTheory.norm_condExpIndL1Fin_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) ≤ μ.real s * ‖x‖

Tactic:
exact norm_condExpIndL1Fin_le hs hμs x

Premises used: MeasureTheory.norm_condExpIndL1Fin_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : G) ↦ condExpIndL1 hm μ s x

Tactic:
continuous_of_linear_of_bound condExpIndL1_add condExpIndL1_smul norm_condExpIndL1_le

Premises used: MeasureTheory.condExpIndL1_add, continuous_of_linear_of_bound, MeasureTheory.norm_condExpIndL1_le, MeasureTheory.condExpIndL1_smul