Theorem: arg_equal_implies_fn_equal (MLIR/Dialects/BuiltinModel.lean)

State before:
α β : Type
x y : α
f : α → β
EQ : x = y
⊢ f x = f y
Tactic:
simp [EQ]
State after:
no goals