Lean/Mathlib: IsConj gives units; use isConj_iff before rcases

In a group, IsConj a b unfolds to ∃ c : Gˣ, SemiconjBy ↑c a b, so obtain ⟨c, hc⟩ := h gives a unit c and a SemiconjBy, and rewrites like ← hc.eq fail to match. Use obtain ⟨c, rfl⟩ := isConj_iff.1 h to get c : G with b = c * a * c⁻¹. Related: in ext y; simp only [...] for an equality of Finset filters, Lean may elaborate {x | P x} on the right-hand side as a Set and coerce the left side. Writing univ.filter P explicitly avoids that.