unfolding definitions

Stream: general

[Guy Leroy]

I have the following def:

def jacobi_sym : ℤ → ℤ → ℤ
| a          1 := 1
| a          b := if b % 2 = 1 then jacobi_sym_aux a b else 0

local notation {a|b} := jacobi_sym a b

and I am trying to prove

h : ¬n = 1
⊢ {a|n} = ite (quadratic_res a n ∧ ¬n ∣ a) 1 (ite (¬quadratic_res a n) (-1) 0)

How can I unfold jacoby_sym such that it shows if b % 2 = 1 then jacobi_sym_aux a b else 0 ?
If I write unfold jacobi_sym the tactic fails

[Kenny Lau]

MWE please

[Kenny Lau]

but rw [jacobi_sym.equations._eqn_2 a n h] should work

[Kenny Lau]

but a better solution would be to not use the equation compiler to define jacobi_sym, but rather use ite

[Guy Leroy]

Thank you very much!

[Simon Hudon]

Out of curiosity, have you tried dunfold? It is based on dsimp which is more careful about preserving definitional equality.