awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
rw : f ∈ (↑(lpMeas F 𝕜 m p μ) : Set ↥(Lp F p μ)) ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₁ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (Submodule.toAddSubmonoid (lpMeas F 𝕜 m p μ)))) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₂ :
  Membership.mem (γ := Set ↥(Lp F p μ))
      (AddSubsemigroup.carrier
        (AddSubmonoid.toAddSubsemigroup
          (Submodule.toAddSubmonoid (R := 𝕜)
            { carrier := {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}, add_mem' := ⋯,
              zero_mem' := ⋯, smul_mem' := ⋯ })))
      f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw₃ rw₄ : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ ↔ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) f ↔
    AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ

Tactic:
rw [← SetLike.mem_coe, ← Submodule.mem_carrier, lpMeas, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, MeasureTheory.lpMeas, SetLike.mem_coe, Submodule.mem_carrier
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m x : MeasurableSpace α
μ : Measure α
f : ↥(lpMeas F 𝕜 m p μ)
⊢ AEStronglyMeasurable (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) μ

Tactic:
mem_lpMeas_iff_aestronglyMeasurable.mp f.mem

Premises used: MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, Subtype.mem, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m0 : MeasurableSpace α
μ : Measure α
f : ↥(Lp F p μ)
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m0 p μ) f

Tactic:
mem_lpMeas_iff_aestronglyMeasurable.mpr (Lp.aestronglyMeasurable f)

Premises used: Iff.mpr, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
hm : m ≤ m0
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
⊢ Membership.mem (γ := Submodule 𝕜 ↥(Lp F p μ)) (lpMeas F 𝕜 m p μ) (indicatorConstLp (s := s) p ⋯ hμs c)

Tactic:
⟨s.indicator fun _ : α => c, (@stronglyMeasurable_const _ _ m _ _).indicator hs,
    indicatorConstLp_coeFn⟩

Premises used: MeasureTheory.stronglyMeasurable_const, Set.Mem, Set.indicator, setOf, MeasureTheory.StronglyMeasurable.indicator, And.intro, Exists.intro, MeasureTheory.indicatorConstLp_coeFn, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
⊢ AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ

Tactic:
have hf : AEStronglyMeasurable[m] f μ :=
    mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
change : MemLp (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm)
⊢ MemLp (Exists.choose (p := fun (g : α → F) ↦ StronglyMeasurable g ∧ (↑(↑f : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] g) ⋯) p
    (μ.trim hm)

Tactic:
change MemLp (hf.mk f) p (μ.trim hm)

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.Measure.trim, MeasureTheory.MemLp, MeasureTheory.AEStronglyMeasurable.mk, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ MemLp (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm)

Tactic:
⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.MemLp, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, And.intro
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
refine : eLpNorm (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm) < ∞
⊢ MemLp (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm)

Tactic:
refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
rw : eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) p μ < ∞
⊢ eLpNorm (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm) < ∞

Tactic:
rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]

Premises used: MeasureTheory.eLpNorm_trim, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) p μ < ∞

Tactic:
Lp.eLpNorm_lt_top f

Premises used: MeasureTheory.Lp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p μ)
hf_meas : Membership.mem (γ := AddSubgroup ↥(Lp F p μ)) (lpMeasSubgroup F m p μ) f
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
⊢ eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) p μ < ∞

Tactic:
exact Lp.eLpNorm_lt_top f

Premises used: MeasureTheory.Lp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) p μ := ⋯
⊢ AEStronglyMeasurable (↑(↑(MemLp.toLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) ⋯) : α →ₘ[μ] F) : α → F) μ

Tactic:
AEStronglyMeasurable.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) p μ := ⋯
refine : AEStronglyMeasurable (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) μ
⊢ AEStronglyMeasurable (↑(↑(MemLp.toLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) ⋯) : α →ₘ[μ] F) : α → F) μ

Tactic:
refine AEStronglyMeasurable.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.MemLp.coeFn_toLp, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) p μ := ⋯
⊢ AEStronglyMeasurable (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) μ

Tactic:
(Lp.aestronglyMeasurable f).of_trim hm

Premises used: MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.of_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) p μ := ⋯
⊢ AEStronglyMeasurable (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) μ

Tactic:
exact (Lp.aestronglyMeasurable f).of_trim hm

Premises used: MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.of_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
(ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp (memLp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem))).trans
    (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp f.mem).choose_spec.2.symm

Premises used: MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable, Exists.choose_spec, Filter.EventuallyEq.trans, And.right, MeasureTheory.ae_eq_of_ae_eq_trim, Subtype.mem, Iff.mp, MeasureTheory.MemLp.coeFn_toLp, Subtype.val, MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ (↑(↑(↑(lpTrimToLpMeasSubgroup F p μ hm f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
MemLp.coeFn_toLp (memLp_of_memLp_trim hm (Lp.memLp f))

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.memLp_of_memLp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeas F 𝕜 m p μ)
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ] (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
(ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp (memLp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem))).trans
    (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp f.mem).choose_spec.2.symm

Premises used: MeasureTheory.mem_lpMeasSubgroup_iff_aestronglyMeasurable, Exists.choose_spec, Filter.EventuallyEq.trans, And.right, MeasureTheory.ae_eq_of_ae_eq_trim, Subtype.mem, Iff.mp, MeasureTheory.MemLp.coeFn_toLp, Subtype.val, MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ (↑(↑(↑(lpTrimToLpMeas F 𝕜 p μ hm f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
MemLp.coeFn_toLp (memLp_of_memLp_trim hm (Lp.memLp f))

Premises used: MeasureTheory.Lp.memLp, MeasureTheory.MemLp.coeFn_toLp, MeasureTheory.memLp_of_memLp_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) :
      α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)
⊢ lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f) = f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) :
      α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
(Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) :
      α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
refine
    (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
(lpMeasSubgroupToLpTrim_ae_eq hm _).trans (lpTrimToLpMeasSubgroup_ae_eq hm _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
exact (lpMeasSubgroupToLpTrim_ae_eq hm _).trans (lpTrimToLpMeasSubgroup_ae_eq hm _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
a : (↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) = (↑f : ↥(Lp F p μ))
⊢ lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f) = f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
a :
  (↑(↑(↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) : α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
⊢ (↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) = (↑f : ↥(Lp F p μ))

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ (↑(↑(↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) : α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
(lpTrimToLpMeasSubgroup_ae_eq hm _).trans (lpMeasSubgroupToLpTrim_ae_eq hm _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ (↑(↑(↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) : α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
exact (lpTrimToLpMeasSubgroup_ae_eq hm _).trans (lpMeasSubgroupToLpTrim_ae_eq hm _)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.lpTrimToLpMeasSubgroup_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)
⊢ lpMeasSubgroupToLpTrim F p μ hm (f + g) = lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [Lp.coeFn_add]

Premises used: MeasureTheory.Lp.coeFn_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
(Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
h :
  StronglyMeasurable
    ((↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F))
h₁ :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ StronglyMeasurable
    ((↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F))

Tactic:
(Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ StronglyMeasurable
    ((↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F))

Tactic:
exact (Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
h : (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq,
    ← Lp.coeFn_add]

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(-lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ lpMeasSubgroupToLpTrim F p μ hm (-f) = -lpMeasSubgroupToLpTrim F p μ hm f

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    -(↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(-lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [Lp.coeFn_neg]

Premises used: MeasureTheory.Lp.coeFn_neg