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

State before:
α : Sort u_1
β : Type u_2
a' a : α
b : β
inst✝ : DecidableEq α
f : α ⇀ β
h : autoParam (a' ≠ a) _auto✝
⊢ insert f a b a' = f a'
Tactic:
simp [insert, h]
State after:
no goals