import proveit
from proveit import defaults
theory = proveit.Theory() # the theorem's theory
%proving num_ket_eq
defaults.assumptions = num_ket_eq.all_conditions()
j_eq_k = defaults.assumptions[0]
j_ket = num_ket_eq.instance_expr.instance_expr.lhs
j_eq_k.substitution(j_ket)
%qed