-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞)
    (((if
                Membership.mem (γ := Set (α × β))
                  (preimage (β := ℝ≥0∞)
                    (fun (a : α × β) ↦
                      (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  (a_1, a) then
              (η : (a : α × β) → Measure ℝ) (a_1, a)
            else
              ((deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel (α × β) ℝ) :
                  (a : α × β) → Measure ℝ)
                (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((piecewise (s :=
                  preimage (β := ℝ≥0∞)
                    (fun (a : α × β) ↦
                      (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  ⋯ η
                  (deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
have h₂ : Membership.mem (γ := Set (α × β))
  (preimage (β := ℝ≥0∞)
    (fun (a : α × β) ↦ (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
    {0})
  (a_1, a)
Tactic: classical
  rw [piecewise_apply, if_pos]
  exact ha