no goals
ι : Type ?u.92215
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
h : indexOf a (b :: l) < length (b :: l)
⊢ get (b :: l) { val := indexOf a (b :: l), isLt := h } = a
by_cases h' : a = b <;>
  simp only [h', if_pos, if_false, indexOf_cons, get, @indexOf_get _ _ l]