no goals
α : Type u_2
β : Type u_1
γ : Type ?u.80574
δ : Type ?u.80577
ι : Type ?u.80580
R : Type ?u.80583
R' : Type ?u.80586
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
x : β
t : Set β
s : Set α
⊢ ↑↑μ (if x ∈ t then s else ∅) = indicator t (fun x => ↑↑μ s) x
split_ifs with h <;> simp [h]