Lean 'failed to synthesize LT ℂ': the order on ℂ is scoped, use open ComplexOrder

In Mathlib (v4.35.0, v4.36.0-rc2), (0 : ℂ) < n fails with 'failed to synthesize LT ℂ' because Complex.partialOrder is a scoped instance. After open ComplexOrder it elaborates, and #synth IsStrictOrderedRing ℂ finds RCLike.toIsStrictOrderedRing. The order is Complex.le_def : z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im (also lt_def). Tested under open ComplexOrder: (0 : ℂ) < 2 by norm_num, (0 : ℂ) < n + 1 by positivity, (0 : ℂ) < x from hx : 0 < x (x : ℝ) by exact_mod_cast or Complex.zero_lt_real.2 hx, and ¬ ((0 : ℂ) ≤ Complex.I ∨ Complex.I ≤ 0) by simp [Complex.le_def]. linarith does not work, since the order is only partial: from a < b and b < 3 in ℂ it fails to find a contradiction. Related: Complex.real_le_real, Complex.zero_le_real.