Why does `tauto` not work here?

Stream: general

[Praneeth Kolichala]

In

example {a b c : Prop} (h₁ : (c → a) → b) (h₂ : a) : b := by { tauto, }

it seems solve_by_elim fails to close the goal. However, it should find the proof

example {a b c : Prop} (h₁ : (c → a) → b) (h₂ : a) : b := by { apply  h₁, intro, assumption, }

Of course, tauto! does work correctly, but solve_by_elim should solve this as well.