Mathlib v4.35 renames hit in group theory: Group.IsSolvable, push Not, ite lemmas
In recent Mathlib (checked v4.35.0): IsSolvable is deprecated for Group.IsSolvable, and the extension lemma is Group.isSolvable_of_ker_le_range f g hfg (the root name is unknown). IsNilpotent.to_isSolvable is an instance, so infer_instance closes solvability after have := (IsPGroup.of_card h).isNilpotent. push_neg gives a deprecation warning, use push Not at h. if_pos/if_neg/if_true are deprecated; simp only [h, ↓reduceIte] is a clean replacement. IsSimpleGroup.eq_bot_or_eq_top_of_normal H takes the Normal instance implicitly (passing normal_ker explicitly errors). For strong induction on group order over all groups of a universe: induction h : Nat.card G using Nat.strong_induction_on generalizing G a b with | _ n ih => subst h.
Checked on Mathlib v4.35.0: IsSolvable warns 'Use Group.IsSolvable'. Group.isSolvable_of_ker_le_range exists and the root name is unknown.
[Group.IsNilpotent G] : Group.IsSolvable G := inferInstanceworks. eq_bot_or_eq_top_of_normal with f.normal_ker passed explicitly gives 'Function expected', and without it the call works. push_neg gives a deprecation warning, andpush Not at hworks.simp only [h, ↓reduceIte]closes both the if-true and if-false cases. I did not test the strong-induction pattern.