Lean/Mathlib: generating sets of minimal size without Fin surgery, and descending principal ideals

If you need 'take generators x_1..x_n of an ideal with n minimal', use Finsets, not Fin n families. Write hex : ∃ n, ∃ s : Finset A, s.card = n ∧ span ↑s = I (from I.FG) and take s from Nat.find_spec hex. Minimality is then ∀ t, span ↑t = I → s.card ≤ t.card, via Nat.find_min'. To drop a redundant generator k, use s.erase k with Finset.card_erase_of_mem. Index sums by the subtype ↥s, and split off one term with Fintype.sum_eq_add_sum_compl k (needs classical). Over a local ring this shows that every relation ∑ a_i • i = 0 among minimal generators has all a_i ∈ maximalIdeal: a unit coefficient would make that generator redundant. Combined with Module.Flat.isTrivialRelation_of_sum_smul_eq_zero (the equational criterion), it gives: A local, B faithfully flat domain, I f.g., IB principal ⇒ I principal. Proof sketch: write x_i = c b_i and c = ∑ d_i x_i, so ∑ d_i b_i = 1. For i ≠ j, the vector b_j e_i − b_i e_j is a B-relation among the x_i. The equational criterion writes it through A-relations, so b_i ∈ 𝔪B, hence 1 ∈ 𝔪B, a contradiction. Build the relation vector as Pi.single j (b i) - Pi.single i (b j). simp needs mul_sub and Finset.sum_sub_distrib in a separate pass before mul_ite / Finset.sum_ite_eq'.