Theorem: Function.update_mul_update (ForML/Util.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝¹ : (i : α) → Monoid (β i)
inst✝ : DecidableEq α
a : α
f : (a : α) → β a
b : β a
⊢ (update f a 1 * update (fun x => 1) a b) a = b
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
β : α → Type u_2
inst✝¹ : (i : α) → Monoid (β i)
inst✝ : DecidableEq α
a : α
f : (a : α) → β a
b : β a
i : α
h : i ≠ a
⊢ (update f a 1 * update (fun x => 1) a b) i = f i
Tactic:
simp [h]
State after:
no goals