Theorem: Partial.insert_same (ReactorModel/Extensions.lean)

State before:
α : Sort u_1
β : Type u_2
a : α
b : β
inst✝ : DecidableEq α
f : α ⇀ β
⊢ insert f a b a = some b
Tactic:
simp [insert]
State after:
no goals