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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ MemLp (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ

Tactic:
Lp.memLp _

Premises used: MeasureTheory.Lp.memLp
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ MemLp (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) 1 μ

Tactic:
exact Lp.memLp _

Premises used: MeasureTheory.Lp.memLp
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
refine :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ)
    fun (a : α) ↦ ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ

Tactic:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
h :
  ∀ (z : α)
    (hz :
      (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z =
        (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z),
    ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
      ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ)
    fun (a : α) ↦ ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ

Tactic:
filter_upwards [condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x] with z hz

Premises used: MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
z : α
hz :
  (↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z =
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z
h h₁ :
  ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
    ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ
⊢ ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ =
    ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) z‖ₑ

Tactic:
rw [hz]
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ

Tactic:
have h_eq :
    ∫⁻ a, ‖condExpIndL1Fin hm hs hμs x a‖ₑ ∂μ = ∫⁻ a, ‖condExpIndSMul hm hs hμs x a‖ₑ ∂μ := by
    refine lintegral_congr_ae ?_
    filter_upwards [condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x] with z hz
    rw [hz]
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
h_eq :
  ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
rw :
  ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ‖x‖ₑ
⊢ ∫⁻ (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 [h_eq, ofReal_norm]

Premises used: ofReal_norm
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
h_eq :
  ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ‖x‖ₑ

Tactic:
lintegral_nnnorm_condExpIndSMul_le hm hs hμs x

Premises used: MeasureTheory.lintegral_nnnorm_condExpIndSMul_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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
h_eq :
  ∫⁻ (a : α), ‖(↑(↑(condExpIndL1Fin (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ =
    ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ
⊢ ∫⁻ (a : α), ‖(↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) a‖ₑ ∂μ ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ‖x‖ₑ

Tactic:
exact lintegral_nnnorm_condExpIndSMul_le hm hs hμs x

Premises used: MeasureTheory.lintegral_nnnorm_condExpIndSMul_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑(condExpIndL1Fin (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)) :
          α →ₘ[μ] G) :
      α → G)
⊢ condExpIndL1Fin (s := s ∪ t) hm ⋯ ⋯ x =
    HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑(condExpIndSMul (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndL1Fin (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(HAdd.hAdd (α := ↥(Lp G 1 μ)) (condExpIndL1Fin (s := s) hm hs hμs x) (condExpIndL1Fin (s := t) hm ht hμt x)) :
          α →ₘ[μ] G) :
      α → G)

Tactic:
grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
    condExpIndL1Fin_ae_eq_condExpIndSMul]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s ∪ t) 2 ⋯ ⋯ 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑(condExpIndSMul (s := s ∪ t) hm ⋯ ⋯ x) : α →ₘ[μ] G) : α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
rw [condExpIndSMul]

Premises used: MeasureTheory.condExpIndSMul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                    (HAdd.hAdd (α := ↥(Lp ℝ 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)
                      (indicatorConstLp (s := t) 2 ht hμt 1))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s ∪ t) 2 ⋯ ⋯ 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]

Premises used: OfNat.ofNat, MeasureTheory.indicatorConstLp_disjoint_union
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑(HAdd.hAdd (α := ↥(lpMeas ℝ ℝ m 2 μ)) (β := ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := s) 2 hs hμs 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := t) 2 ht hμt 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                    (HAdd.hAdd (α := ↥(Lp ℝ 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)
                      (indicatorConstLp (s := t) 2 ht hμt 1))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (HAdd.hAdd (α := ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (↑(HAdd.hAdd (α := ↥(lpMeas ℝ ℝ m 2 μ)) (β := ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := s) 2 hs hμs 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))
                    ((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := t) 2 ht hμt 1) :
                      ↥(lpMeas ℝ ℝ m 2 μ))) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
push_cast
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)
⊢ (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
              (HAdd.hAdd (α := ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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 :
  HAdd.hAdd (α := α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)
⊢ (↑(↑(HAdd.hAdd (α := ↥(Lp G 2 μ))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)))
              ((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ)))) :
          α →ₘ[μ] G) :
      α → G) =ᶠ[ae μ]
    (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] G) : α → G) +
      (↑(↑(condExpIndSMul (s := t) hm ht hμt x) : α →ₘ[μ] G) : α → G)

Tactic:
grw [Lp.coeFn_add]

Premises used: MeasureTheory.Lp.coeFn_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
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
⊢ HAdd.hAdd (α := α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G) =ᶠ[ae μ]
    HAdd.hAdd (α := α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)
      (↑(↑((compLpL 2 μ (toSpanSingleton ℝ x) : (a : ↥(Lp ℝ 2 μ)) → ↥(Lp G 2 μ))
                (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                      (indicatorConstLp (s := t) 2 ht hμt 1)) :
                  ↥(Lp ℝ 2 μ))) :
            α →ₘ[μ] G) :
        α → G)

Tactic:
rfl
-- 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)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ Eq (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) (condExpIndL1Fin (s := s) hm hs hμs x)

Tactic:
simp only [condExpIndL1, And.intro hs hμs, dif_pos, Ne, not_false_iff, and_self_iff]

Premises used: dif_pos, Ne, And.intro, and_self_iff, not_false_iff, MeasureTheory.condExpIndL1
-- 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)
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : G
⊢ Eq (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) 0

Tactic:
simp only [condExpIndL1, hμs, not_true, Ne, dif_neg, not_false_iff,
    and_false]

Premises used: Ne, dif_neg, not_true, and_false, not_false_iff, MeasureTheory.condExpIndL1
-- 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)
hs : ¬MeasurableSet s
x : G
⊢ Eq (α := ↥(Lp G 1 μ)) (condExpIndL1 hm μ s x) 0

Tactic:
simp only [condExpIndL1, hs, dif_neg, not_false_iff, false_and]

Premises used: false_and, dif_neg, not_false_iff, MeasureTheory.condExpIndL1