-- 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'
hfg :
  f' = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ)) g
refine_1 :
  ∀ (c : F) {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (g : ↥(Lp F p (μ.trim hm))) ↦
        P
          (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                  (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                g) :
            ↥(Lp F p μ)))
      (↑(simpleFunc.indicatorConst p (s := s) hs ⋯ c) : ↥(Lp F p (μ.trim hm)))
refine_2 :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p (μ.trim hm)) (hg : MemLp g p (μ.trim hm)),
    Disjoint (Function.support f) (Function.support g) →
      (fun (g : ↥(Lp F p (μ.trim hm))) ↦
            P
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                      (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                    g) :
                ↥(Lp F p μ)))
          (MemLp.toLp f hf) →
        (fun (g : ↥(Lp F p (μ.trim hm))) ↦
              P
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                        (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                      g) :
                  ↥(Lp F p μ)))
            (MemLp.toLp g hg) →
          (fun (g : ↥(Lp F p (μ.trim hm))) ↦
              P
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                        (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                      g) :
                  ↥(Lp F p μ)))
            (MemLp.toLp f hf + MemLp.toLp g hg)
refine_3 :
  IsClosed (X := ↥(Lp F p (μ.trim hm)))
    {f : ↥(Lp F p (μ.trim hm)) |
      (fun (g : ↥(Lp F p (μ.trim hm))) ↦
          P
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) :
                    (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
                  g) :
              ↥(Lp F p μ)))
        f}
⊢ P
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F ℝ p μ hm) : (a : ↥(Lp F p (μ.trim hm))) → ↥(lpMeas F ℝ m p μ))
          g) :
      ↥(Lp F p μ))

Tactic:
refine
    @Lp.induction α F m _ p (μ.trim hm) _ hp_ne_top
      (fun g => P ((lpMeasToLpTrimLie F ℝ p μ hm).symm g)) ?_ ?_ ?_ g

Premises used: Real, LinearIsometryEquiv.symm, MeasureTheory.lpMeasToLpTrimLie, MeasureTheory.Lp.induction, Subtype.val, DFunLike.coe