have : sgn p * sgn q ≃ 0 := calc
  sgn p * sgn q ≃ _ := Rel.symm sgn_compat_mul
  sgn (p * q)   ≃ _ := sgn_zero.mp ‹p * q ≃ 0›
  0             ≃ _ := Rel.refl
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
p q : ℚ
x✝ : p * q ≃ 0
this : sgn p * sgn q ≃ 0
⊢ p ≃ 0 ∨ q ≃ 0