α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
⊢ bind (pure a) f = f a
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
⊢ bind (pure a) f = f a
have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by
  split_ifs with h <;> simp; subst h; simp
case h
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
b : β
⊢ ↑(bind (pure a) f) b = ↑(f a) b
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
⊢ bind (pure a) f = f a
ext b
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
b : β
⊢ ↑(bind (pure a) f) b = ↑(f a) b
simp [this]
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
⊢ (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
split_ifs with h <;> simp
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
f : α → Pmf β
b : β
a' : α
⊢ ↑(f a') b = ↑(f a') b
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
subst h
no goals
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.56970
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
f : α → Pmf β
b : β
a' : α
⊢ ↑(f a') b = ↑(f a') b
simp