refactor(group_theory/solvable): simp -> assumption (#6120)

Co-authors: `lean-gptf`, Stanislas Polu

This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.

src/group_theory/solvable.lean

@@ -228,7 +228,7 @@ begin
 end
 
 lemma is_solvable_of_top_eq_bot (h : (⊤ : subgroup G) = ⊥) : is_solvable G :=
-⟨⟨0, by simp *⟩⟩
+⟨⟨0, h⟩⟩
 
 @[priority 100]
 instance is_solvable_of_subsingleton [subsingleton G] : is_solvable G :=