Theorem: MLIR.AST.AttrDict.find_next (MLIR/AST.lean)

State before:
α σ : Type
ε : σ → Type
n n' : String
δ : Dialect α σ ε
v : AttrValue δ
l : List (AttrEntry δ)
⊢ find (mk (AttrEntry.mk n v :: l)) n' = if (n == n') = true then some v else find (mk l) n'
Tactic:
cases H: n == n' <;>
simp [AttrDict.find, List.find?, AttrEntry.key, AttrEntry.value, H]
State after:
no goals