α : Type u_1
β : Type ?u.85918
γ : Type ?u.85921
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
⊢ p = q
α : Type u_1
β : Type ?u.85918
γ : Type ?u.85921
inst✝¹ : MeasurableSpace α
p : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure
intro p q h
case h
α : Type u_1
β : Type ?u.85918
γ : Type ?u.85921
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
x : α
⊢ ↑p x = ↑q x
α : Type u_1
β : Type ?u.85918
γ : Type ?u.85921
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
⊢ p = q
ext x
no goals
case h
α : Type u_1
β : Type ?u.85918
γ : Type ?u.85921
inst✝¹ : MeasurableSpace α
p✝ : Pmf α
s t : Set α
inst✝ : MeasurableSingletonClass α
p q : Pmf α
h : toMeasure p = toMeasure q
x : α
⊢ ↑p x = ↑q x
rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
  ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]