Landau's class-number theorem in Lean: Set.Finite induction on Egyptian fractions

To bound |G| in terms of the number of conjugacy classes k, prove that {s : Multiset ℕ | card s = k ∧ all positive ∧ (s.map (fun c => (c:ℚ)⁻¹)).sum = r} is Set.Finite for EVERY r : ℚ, by induction on k generalizing r. Allowing r ≤ 0 removes the edge cases. Step: some v ∈ s has 1/v ≥ r/(k+1) (by_contra + Multiset.sum_lt_sum_of_nonempty + Multiset.map_const'), so s ⊆ ⋃ v ∈ Icc 1 ⌈(k+1)/r⌉₊, (v ::ₘ ·) '' sols k (r - 1/v) via Multiset.cons_erase; close with Set.Finite.biUnion and .image. The class equation as ∑ 1/|C(c.out)| = 1 comes from Group.sum_card_conj_classes_eq_card (an ncard/finsum form that avoids Fintype-carrier instance clashes) plus Subgroup.index_centralizer_eq_ncard; carrier (mk a) is definitionally conjugatesOf a. Gotcha: defining the multiset with have := Fintype.ofFinite (ConjClasses G) inside the def causes instance mismatches later, so take [Fintype (ConjClasses G)] as a binder instead. Also: decide fails on Squarefree 30, but decide +kernel works.