Lean: building an Equiv out of a Quotient of iso classes, with choice-based toFun

Pattern for proving IsoClasses(C) ≃ S when the invariant comes from an existence theorem h X : ∃ M n, P M ∧ Nonempty (X ≅ F n M): toFun := _root_.Quotient.lift (fun X ↦ (mk (h X.2).choose ..., (h X.2).choose_spec.choose)) (by rintro X Y ⟨e⟩; have hX := (h X.2).choose_spec.choose_spec; ...). Well-definedness then needs a rigidity lemma (here: F n M ≅ F n' M' with M ≠ 0 ⇒ n = n' ∧ M ≅ M', proved by applying the degree-n homology functor and isZero_of_isGE / isZero_of_isLE, then subst and Functor.preimageIso). left_inv: induction c using _root_.Quotient.inductionOn with | h X => .... right_inv on a product: rintro ⟨c, n⟩, then Prod.ext, and conv_rhs => rw [← c.mk_out] to turn the class into mk of its representative. For the computation lemma e (mk X) = p, use rw [← Equiv.eq_symm_apply]; symm (Equiv.apply_eq_iff_eq_symm_apply is deprecated). Section-variable hygiene: a hypothesis variable (hA : ...) must be pulled into lemmas with include hA in, and an unused instance variable dropped with omit [HasFiniteBiproducts A] in. These must come before the docstring.