-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem memLp_trim_of_mem_lpMeasSubgroup (hm : m ≤ m0) (f : Lp F p μ)
    (hf_meas : f ∈ lpMeasSubgroup F m p μ) :
    MemLp (mem_lpMeasSubgroup_iff_aeStronglyMeasurable.mp hf_meas).choose p (μ.trim hm)

Proof state:
α : 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 : f ∈ lpMeasSubgroup F m p μ
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Tactic:
have hf : AEStronglyMeasurable[m] f μ :=
  mem_lpMeasSubgroup_iff_aeStronglyMeasurable.mp hf_meas

Result:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Proof state:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Tactic:
change MemLp g p (μ.trim hm)

Result:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ MemLp g p (μ.trim hm)

Proof state:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ eLpNorm (Exists.choose hf) p μ = eLpNorm (↑↑f) p μ

Tactic:
exact eLpNorm_congr_ae hfg.symm

Result:
no goals

Proof state:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ eLpNorm g p (μ.trim hm) < ⊤

Tactic:
have h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm f p μ := by
  rw [eLpNorm_trim hm hg]
  exact eLpNorm_congr_ae hfg.symm

Result:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ
⊢ eLpNorm g p (μ.trim hm) < ⊤

Proof state:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ
⊢ eLpNorm g p (μ.trim hm) < ⊤

Tactic:
rw [h_eLpNorm_fg]

Result:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ
⊢ eLpNorm (↑↑f) p μ < ⊤

Proof state:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ MemLp g p (μ.trim hm)

Tactic:
refine ⟨hg.aestronglyMeasurable, ?_⟩

Result:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ eLpNorm g p (μ.trim hm) < ⊤

Proof state:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Tactic:
obtain ⟨hg, hfg⟩ := hf.choose_spec

Result:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Proof state:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Tactic:
let g := hf.choose

Result:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
⊢ MemLp (Exists.choose ⋯) p (μ.trim hm)

Proof state:
case intro
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ
⊢ eLpNorm (↑↑f) p μ < ⊤

Tactic:
exact Lp.eLpNorm_lt_top f

Result:
no goals

Proof state:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ eLpNorm g p (μ.trim hm) = eLpNorm (↑↑f) p μ

Tactic:
rw [eLpNorm_trim hm hg]

Result:
α : 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 : f ∈ lpMeasSubgroup F m p μ
hf : AEStronglyMeasurable (↑↑f) μ
g : α → F := Exists.choose hf
hg : StronglyMeasurable (Exists.choose hf)
hfg : ↑↑f =ᶠ[ae μ] Exists.choose hf
⊢ eLpNorm (Exists.choose hf) p μ = eLpNorm (↑↑f) p μ