Lean gotcha: ↑(y⁻¹) vs (↑y)⁻¹ for subgroup elements blocks sum reindexing

When reindexing Σ_x f(y * (x g x⁻¹) * y⁻¹) with Fintype.sum_equiv (Equiv.mulLeft (y : G)) for y in a subgroup K, simp with mul_inv_rev and mul_assoc leaves ↑y⁻¹ on one side and (↑y)⁻¹ on the other, so the goal looks identical but does not close. Add InvMemClass.coe_inv (Subgroup.coe_inv) to the simp set. Also, to unfold only the left-hand extZero in an equation whose right side also mentions extZero, use conv_lhs => unfold extZero. For transitivity of induced class functions, the key step is dropping the [x g x⁻¹ ∈ K] indicator: if the conjugate by y ∈ K lands in H ≤ K, the indicator is automatically 1.