split at mem <;> try simp [Node.inBounds] at *
node : Node
j k : ℕ
c : Char
inBounds : node.inBounds k
mem :
  j ∈
    match node with
    | Node.char c' next => if (c == c') = true then {next} else ∅
    | Node.sparse cs next => if c ∈ cs then {next} else ∅
    | x => ∅
⊢ j < k
case h_1
j k : ℕ
c : Char
n✝ : Node
c'✝ : Char
next✝ : ℕ
inBounds : next✝ < k
mem : c = c'✝ ∧ j = next✝
⊢ j < k

case h_2
j k : ℕ
c : Char
n✝ : Node
cs✝ : Data.Classes
next✝ : ℕ
inBounds : next✝ < k
mem : c ∈ cs✝ ∧ j = next✝
⊢ j < k