-- 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 α
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_1 : ↥(Lp F p μ)
hf_1 : AEStronglyMeasurable (↑(↑f_1 : α →ₘ[μ] 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_1 hf_1
g_1 : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm : (a : ↥(lpMeas F ℝ m p μ)) → ↥(Lp F p (μ.trim hm))) f'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g_1
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F p μ))
hgP :
  P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F p μ))
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
    (↑((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 ⋯
⊢ P
    (HAdd.hAdd (α := ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F p μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
have refine_2 : ∀ (hfP : P (MemLp.toLp f sorry))
  (hgP :
    P
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
  (h_eq :
    ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)),
      (↑((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 sorry),
  P
    (MemLp.toLp f sorry +
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F p μ)))
Tactic: rw [h_eq f hf] at hfP ⊢
Cleared hypotheses: hfP, hgP, h_eq