-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
rw :
  Eq.{u_5 + 1} (α := Measure Ω)
    ((((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 Ω))) ⋯)
                    ⋯)).comapRight
              (f := embeddingReal Ω) ⋯ :
            Kernel α Ω) :
          (a : α) → Measure Ω)
        a :
      Measure Ω)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
      else
        Measure.comap (embeddingReal Ω)
          (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
      Measure Ω)
rw₁ :
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      ((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))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
rw₂ :
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Membership.mem (γ := Set α)
            (preimage (β := ℝ≥0∞)
              (fun (a : α) ↦
                (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
              {0})
            a then
        (η : (a : α) → Measure ℝ) a
      else
        ((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
              Kernel α ℝ) :
            (a : α) → Measure ℝ)
          a))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
rw₃ rw₄ rw₅ :
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Membership.mem (γ := Set α)
            (preimage (β := ℝ≥0∞)
              (fun (a : α) ↦
                (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
              {0})
            a then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
rw₆ :
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
⊢ Eq.{u_5 + 1} (α := Measure Ω) (((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
      else
        Measure.comap (embeddingReal Ω)
          (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
      Measure Ω)

Tactic:
classical
  rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]
  simp only [mem_preimage, mem_singleton_iff]
  split_ifs <;> rfl

Premises used: ProbabilityTheory.Kernel.deterministic_apply, ProbabilityTheory.Kernel.piecewise_apply, ProbabilityTheory.Kernel.borelMarkovFromReal, Set.mem_singleton_iff, ProbabilityTheory.Kernel.comapRight_apply, Set.mem_preimage