-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                    (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                ↥(Lp ℝ 2 μ)) :
                            α →ₘ[μ] ℝ) :
                        α → ℝ)
                      x =
                    AEStronglyMeasurable.mk
                      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                    (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                ↥(Lp ℝ 2 μ)) :
                            α →ₘ[μ] ℝ) :
                        α → ℝ)
                      h x)
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  x ∈ t →
                    AEStronglyMeasurable.mk
                        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                  ↥(Lp ℝ 2 μ)) :
                              α →ₘ[μ] ℝ) :
                          α → ℝ)
                        h x =
                      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                                      (indicatorConstLp (s := s) 2 hs hμs 1)) :
                                  ↥(Lp ℝ 2 μ)) :
                              α →ₘ[μ] ℝ) :
                          α → ℝ)
                        x)
                x}
            x}
      a
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
have h₂ : ∀ (a : α),
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a =
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h a →
    a ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h a =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a
Tactic: filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.symm