awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have refine : eLpNorm (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm) < ∞
Tactic: refine ⟨hf.stronglyMeasurable_mk.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 (AEStronglyMeasurable.mk (↑(↑f : α →ₘ[μ] F) : α → F) hf) p (μ.trim hm) < ∞
have rw : eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) p μ < ∞
Tactic: rw [eLpNorm_trim hm hf.stronglyMeasurable_mk, eLpNorm_congr_ae hf.ae_eq_mk.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) μ
have refine : AEStronglyMeasurable (↑(↑f : α →ₘ[μ.trim hm] F) : α → F) μ
Tactic: refine AEStronglyMeasurable.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = f
have h : (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) :
    α → F) =ᶠ[ae (μ.trim hm)]
  (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (lpTrimToLpMeasSubgroup F p μ hm f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
  (↑(↑f : α →ₘ[μ.trim hm] F) : α → F)
Tactic: refine
    (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = f
have a : (↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) = (↑f : ↥(Lp F p μ))
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 : ↥(Lp F p μ))
have a : (↑(↑(↑(lpTrimToLpMeasSubgroup F p μ hm (lpMeasSubgroupToLpTrim F p μ hm f)) : ↥(Lp F p μ)) : α →ₘ[μ] F) :
    α → F) =ᶠ[ae μ]
  (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 + lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)
have 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)
Tactic: grw [Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : StronglyMeasurable
  ((↑(↑(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 ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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))
⊢ (↑(↑(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)
have 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)
Tactic: refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ]
    (↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F) +
      (↑(↑(lpMeasSubgroupToLpTrim F p μ hm g) : α →ₘ[μ.trim hm] F) : α → F)
have h : (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(f + g) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq,
    ← Lp.coeFn_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = -lpMeasSubgroupToLpTrim F p μ hm f
have h : (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
  (↑(↑(-lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : (↑(↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : (↑(↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
  -(↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg
    ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ]
    -(↑(↑(lpMeasSubgroupToLpTrim F p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
have h : (↑(↑(↑(-f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] (↑(↑(↑(-f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
Tactic: grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
have rw : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
have rw₁ : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
have rw₂ : lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm (-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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ lpMeasSubgroupToLpTrim F p μ hm (f - g) = lpMeasSubgroupToLpTrim F p μ hm f - lpMeasSubgroupToLpTrim F p μ hm g
have rw₃ : lpMeasSubgroupToLpTrim F p μ hm f + -lpMeasSubgroupToLpTrim F p μ hm 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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) = c • lpMeasToLpTrim F 𝕜 p μ hm f
have h : (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
  (↑(↑(c • lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : (↑(↑(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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h : StronglyMeasurable (c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F))
Tactic: refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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))
⊢ (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae (μ.trim hm)]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
have h₁ : (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm (c • f)) : α →ₘ[μ.trim hm] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
have h : (↑(↑(↑(c • f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: grw [lpMeasToLpTrim_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ)
⊢ (↑(↑(↑(c • f) : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
have h : (↑(↑(c • (↑f : ↥(Lp F p μ))) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
  c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ)
⊢ (↑(↑(c • (↑f : ↥(Lp F p μ))) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ]
    c • (↑(↑(lpMeasToLpTrim F 𝕜 p μ hm f) : α →ₘ[μ.trim hm] F) : α → F)
have h : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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)
have h₁ : c • (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F) =ᶠ[ae μ] c • (↑(↑(↑f : ↥(Lp F p μ)) : α →ₘ[μ] F) : α → F)
Tactic: grw [Lp.coeFn_smul, lpMeasToLpTrim_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ)
⊢ ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖
have rw : ‖(↑f : ↥(Lp F p μ))‖ = ‖f‖
Tactic: rw [Lp.norm_def, eLpNorm_trim hm (Lp.stronglyMeasurable _),
    eLpNorm_congr_ae (lpMeasSubgroupToLpTrim_ae_eq hm _), ← Lp.norm_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ)
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g
have rw : ‖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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g
have rw₁ : ‖lpMeasSubgroupToLpTrim F p μ hm (f - g)‖ = dist f g
Tactic: rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
      dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g
have rw₂ : ‖f - g‖ = dist f g
Tactic: rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
      dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g
have rw₃ : ‖f - g‖ = ‖f - g‖
Tactic: rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
      dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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 μ)
have rw : CompleteSpace ↥(Lp F p (μ.trim sorry))
Tactic: rw [(lpMeasSubgroupToLpTrimIso F p μ hm.elim).completeSpace_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ IsComplete (α := ↥(Lp F p μ)) {f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ}
have rw : CompleteSpace (↑{f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ} : Type (max u_1 u_2))
Tactic: rw [← completeSpace_coe_iff_isComplete]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (hypothesis)
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
⊢ CompleteSpace (↑{f : ↥(Lp F p μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F) : α → F) μ} : Type (max u_1 u_2))
have this : Fact (m ≤ m0)
Tactic: haveI : Fact (m ≤ m0) := ⟨hm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable (goal)
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
⊢ 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)
have 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 sorry sorry c) : α →ₘ[μ] F) : α → F)
Tactic: ext1