simp (config:={decide:=true}) only [ite_true, ite_false, h, mem_univ, not_true, IsEmpty.forall_iff, forall_const, not_false_eq_true,
  and_self, Prod.mk.eta, hn]
case h
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ (((if 0 = 0 then x.1 else x.2) * if 1 = 0 then x.1 else x.2) = n ∧ ¬n = 0) ∧
    (if 0 = 0 then x.1 else x.2, if 1 = 0 then x.1 else x.2) = x
no goals