∀ (a : ℤ) (b : ℕ),
  fastJacobiSym✝ a b =
    if hb0 : b = 0 then 1
    else
      if x : b % 2 = 0 then
        if a % 2 = 0 then 0
        else
          have this := ⋯;
          fastJacobiSym✝ a (b / 2)
      else if b = 1 then 1 else if hab : a % ↑b = 0 then 0 else fastJacobiSymAux✝ (a % ↑b).natAbs b false ⋯