-- Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
lemma borelMarkovFromReal_apply (Ω : Type*) [Nonempty Ω] [MeasurableSpace Ω] [StandardBorelSpace Ω]
    (η : Kernel α ℝ) (a : α) :
    borelMarkovFromReal Ω η a
      = if η a (range (embeddingReal Ω))ᶜ = 0 then (η a).comap (embeddingReal Ω)
        else (Measure.dirac (range_nonempty (embeddingReal Ω)).choose).comap (embeddingReal Ω)

Proof state:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if (η a) (range (embeddingReal Ω))ᶜ = 0 then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ (borelMarkovFromReal Ω η) a =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if a ∈ (fun a => (η a) (range (embeddingReal Ω))ᶜ) ⁻¹' {0} then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Tactic:
simp only [mem_preimage, mem_singleton_iff]

Result:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if (η a) (range (embeddingReal Ω))ᶜ = 0 then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Proof state:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ (borelMarkovFromReal Ω η) a =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Tactic:
rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]

Result:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if a ∈ (fun a => (η a) (range (embeddingReal Ω))ᶜ) ⁻¹' {0} then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))