awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (μ.trim hm)]
    -(↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

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

Premises used: MeasureTheory.StronglyMeasurable.neg, 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 : ↥(lpMeasSubgroup F m p μ)
h :
  (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    -(↑(↑(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:
refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg
    ?_

Premises used: MeasureTheory.StronglyMeasurable.neg, 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 : ↥(lpMeasSubgroup F m p μ)
h : (↑(↑(↑(-f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(-f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    -(↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

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

Premises used: MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.Lp.coeFn_neg
-- 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 μ)
⊢ (↑(↑(↑(-f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(-f) : ↥(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 g : ↥(lpMeasSubgroup F m p μ)
rw : lpMeasSubgroupToLpTrim F p μ hm (f + -g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
rw₁ : lpMeasSubgroupToLpTrim F p μ hm (f + -g) = lpMeasSubgroupToLpTrim F p μ hm f + -lpMeasSubgroupToLpTrim F p μ hm g
rw₂ :
  lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm (-g) =
    lpMeasSubgroupToLpTrim F p μ hm f + -lpMeasSubgroupToLpTrim F p μ hm g
rw₃ rw₄ :
  lpMeasSubgroupToLpTrim F p μ hm f + -lpMeasSubgroupToLpTrim F p μ hm g =
    lpMeasSubgroupToLpTrim F p μ hm f + -lpMeasSubgroupToLpTrim F p μ hm g
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, lpMeasSubgroupToLpTrim_add,
    lpMeasSubgroupToLpTrim_neg]

Premises used: MeasureTheory.lpMeasSubgroupToLpTrim_neg, sub_eq_add_neg, MeasureTheory.lpMeasSubgroupToLpTrim_add
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h :
  (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(c • lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ lpMeasToLpTrim F 𝕜 p μ hm (c • f) = c • lpMeasToLpTrim F 𝕜 p μ hm f

Tactic:
ext1
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h :
  (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    (↑(↑(c • lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [Lp.coeFn_smul]

Premises used: MeasureTheory.Lp.coeFn_smul
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.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
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h : StronglyMeasurable (c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F))
h₁ :
  (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.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
𝕜 : Type u_3
p : ℝ≥0∞
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ StronglyMeasurable (c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F))

Tactic:
(Lp.stronglyMeasurable _).const_smul c

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.const_smul
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
⊢ StronglyMeasurable (c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F))

Tactic:
exact (Lp.stronglyMeasurable _).const_smul c

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.const_smul
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h :
  (↑(↑(↑(c • f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [lpMeasToLpTrim_ae_eq]

Premises used: MeasureTheory.lpMeasToLpTrim_ae_eq
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h :
  (↑(↑(c • (↑f : ↥(Lp F p μ))) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
⊢ (↑(↑(↑(c • f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
push_cast
-- 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
c : 𝕜
f : ↥(lpMeas F 𝕜 m p μ)
h :
  c • (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
h₁ h₂ : c • (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] c • (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(c • (↑f : ↥(Lp F p μ))) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)

Tactic:
grw [Lp.coeFn_smul, lpMeasToLpTrim_ae_eq]

Premises used: MeasureTheory.Lp.coeFn_smul, MeasureTheory.lpMeasToLpTrim_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 α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
rw : ‖(↑f : ↥(Lp F p μ))‖ = ‖f‖
⊢ ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖

Tactic:
rw [Lp.norm_def, eLpNorm_trim hm (Lp.stronglyMeasurable _),
    eLpNorm_congr_ae (lpMeasSubgroupToLpTrim_ae_eq hm _), ← Lp.norm_def]

Premises used: MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.eLpNorm_trim, MeasureTheory.eLpNorm_congr_ae, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ‖(↑f : ↥(Lp F p μ))‖ = ‖f‖

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
rw : ‖lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g‖ = dist f g
rw₁ : ‖lpMeasSubgroupToLpTrim F p μ hm (f - g)‖ = dist f g
rw₂ : ‖f - g‖ = dist f g
rw₃ rw₄ : ‖f - g‖ = ‖f - g‖
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g

Tactic:
rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
      dist_eq_norm]

Premises used: dist_eq_norm, MeasureTheory.lpMeasSubgroupToLpTrim_sub, MeasureTheory.lpMeasSubgroupToLpTrim_norm_map
-- 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 : Fact (m ≤ m0)
inst_3 : CompleteSpace F
hp : Fact (1 ≤ p)
rw : CompleteSpace ↥(Lp F p (μ.trim ⋯))
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
rw [(lpMeasSubgroupToLpTrimIso F p μ hm.elim).completeSpace_iff]

Premises used: MeasureTheory.lpMeasSubgroupToLpTrimIso, IsometryEquiv.completeSpace_iff, Fact.elim
-- 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 : Fact (m ≤ m0)
inst_3 : CompleteSpace F
hp : Fact (1 ≤ p)
⊢ CompleteSpace ↥(Lp F p (μ.trim ⋯))

Tactic:
infer_instance
-- 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 : Fact (m ≤ m0)
inst_3 : CompleteSpace F
hp : Fact (1 ≤ p)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst_1 : CompleteSpace F
hm : m ≤ m0
rw : CompleteSpace (↑{f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ} : Type (max u_1 u_2))
⊢ IsComplete (α := ↥(Lp F p μ)) {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}

Tactic:
rw [← completeSpace_coe_iff_isComplete]

Premises used: completeSpace_coe_iff_isComplete
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst_1 : CompleteSpace F
hm : m ≤ m0
⊢ Fact (m ≤ m0)

Tactic:
haveI : Fact (m ≤ m0) := ⟨hm⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
inst_1 : CompleteSpace F
hm : m ≤ m0
this : Fact (m ≤ m0)
⊢ CompleteSpace ↥(lpMeasSubgroup F m p μ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : CompleteSpace F
hm : m ≤ m0
⊢ IsClosed (X := ↥(Lp F p μ)) {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}

Tactic:
IsComplete.isClosed (isComplete_aestronglyMeasurable hm)

Premises used: IsComplete.isClosed, MeasureTheory.isComplete_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 α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeas F 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ∃ (g : α → F), FinStronglyMeasurable g (μ.trim hm) ∧ (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] g

Tactic:
⟨lpMeasSubgroupToLpTrim F p μ hm f, Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top,
    (lpMeasSubgroupToLpTrim_ae_eq hm f).symm⟩

Premises used: MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq, MeasureTheory.Lp.finStronglyMeasurable, MeasureTheory.AEEqFun.cast, MeasureTheory.lpMeasSubgroupToLpTrim, And.intro, Exists.intro, Subtype.val, 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 α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
h :
  (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (indicatorConstLp (s := s) p hs hμs c)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
⊢ Eq (α := ↥(Lp F p μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (indicatorConstLp (s := s) p hs hμs c)) :
      ↥(Lp F p μ))
    (indicatorConstLp (s := s) p ⋯ ⋯ c)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
h :
  (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (indicatorConstLp (s := s) p hs hμs c)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)

Tactic:
change
    lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c) =ᵐ[μ]
      (indicatorConstLp p _ _ c : α → F)

Premises used: Real, MeasureTheory.lpTrimToLpMeas, MeasureTheory.indicatorConstLp, MeasureTheory.AEEqFun.cast, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : F
h :
  (↑(↑(indicatorConstLp (s := s) p hs hμs c) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
h₁ : (s.indicator fun (x : α) ↦ c) =ᶠ[ae μ] (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)
h₂ h₃ : EventuallyEq.{u_1, u_2} (β := F) (ae μ) (s.indicator fun (x : α) ↦ c) (s.indicator fun (x : α) ↦ c)
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp (s := s) p hs hμs c)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(indicatorConstLp (s := s) p ⋯ ⋯ c) : α →ₘ[μ] F) : α → F)

Tactic:
grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim indicatorConstLp_coeFn, indicatorConstLp_coeFn]

Premises used: MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.lpTrimToLpMeas_ae_eq, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
h :
  (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (MemLp.toLp f hf)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
⊢ (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ)) =
    MemLp.toLp 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 α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
h :
  (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
⊢ (↑(↑(↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  (MemLp.toLp f hf)) :
              ↥(Lp F p μ)) :
          α →ₘ[μ] F) :
      α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)

Tactic:
change lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf) =ᵐ[μ] (MemLp.toLp f _ : α → F)

Premises used: Real, MeasureTheory.lpTrimToLpMeas, MeasureTheory.AEEqFun.cast, MeasureTheory.MemLp.toLp, 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 α
one_le_p : Fact (1 ≤ p)
inst_1 : NormedSpace ℝ F
hm : m ≤ m0
f : α → F
hf : MemLp f p (μ.trim hm)
h : (↑(↑(MemLp.toLp f hf) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ] (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
h₁ : f =ᶠ[ae μ] (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)
h₂ h₃ : f =ᶠ[ae μ] f
⊢ (↑(↑(↑(lpTrimToLpMeas F ℝ p μ hm (MemLp.toLp f hf)) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    (↑(↑(MemLp.toLp f ⋯) : α →ₘ[μ] F) : α → F)

Tactic:
grw [lpTrimToLpMeas_ae_eq, ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp hf), MemLp.coeFn_toLp]

Premises used: MeasureTheory.ae_eq_of_ae_eq_trim, MeasureTheory.lpTrimToLpMeas_ae_eq, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
let : P f
⊢ P f

Tactic:
let f' := (⟨f, hf⟩ : lpMeas F ℝ m p μ)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
Goal:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst_1 : Fact (1 ≤ p)
inst_2 : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    P (↑(simpleFunc.indicatorConst p (s := s) ⋯ ⋯ c) : ↥(Lp F p μ))
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed (X := ↥(lpMeas F ℝ m p μ)) {f : ↥(lpMeas F ℝ m p μ) | P (↑f : ↥(Lp F p μ))}
f : ↥(Lp F p μ)
hf : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ
f' : ↥(lpMeas F ℝ m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp F p μ)) ↦ Membership.mem (γ := Submodule ℝ ↥(Lp F p μ)) (lpMeas F ℝ m p μ) x) f hf
g : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
⊢ f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g

Tactic:
simp only [f', g, LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply