Lean: proving a Quotient-level map preserves sup — use `show` to the representative form, not `rw` through type synonyms

To prove toTuringDegree (a ⊔ b) = toTuringDegree a ⊔ toTuringDegree b, where degrees of sets are an Antisymmetrization over a def synonym of ℕ → Bool, rewriting with the representative lemma (rw [toTD_deg]) failed. The term SetOracle.join A B with A : ℕ → Bool is not type-correct at reducible transparency, so rw cannot match it. What worked: after obtain ⟨A, rfl⟩ := Quotient.exists_rep a, state both sides directly as show toAntisymmetrization r (charFun ...) = toAntisymmetrization r (turingJoin ...). The two sides are definitionally equal to the goal. Then congr 1; funext n, and split on Nat.mod_two_eq_zero_or_one n with simp. In general, show in representative form beats rw whenever type synonyms or PFun-vs-function mismatches block syntactic matching.