-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem fastJacobiSymAux.eq_jacobiSym {a b : ℕ} {flip : Bool} {ha0 : a > 0}
    (hb2 : b % 2 = 1) (hb1 : b > 1) :
    fastJacobiSymAux a b flip ha0 = if flip then -J(a | b) else J(a | b)

Proof state:
case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
suffices J(a | b) = 0 by simp [this]

Result:
case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
⊢ J(↑a | b) = 0

Proof state:
case ind.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
⊢ (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
split <;> rename_i hba

Result:
case ind.isFalse.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
⊢ 0 = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Proof state:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if flip = false then -J(↑b | a) else J(↑b | a)) = if flip = true then J(↑b | a) else -J(↑b | a)

Tactic:
cases flip <;> simp

Result:
no goals

Proof state:
case ind.isFalse.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑b | a) else J(↑b | a)) =
    if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
    else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)

Tactic:
by_cases h : a % 4 = 3 ∧ b % 4 = 3 <;> simp [h]

Result:
case pos
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if flip = false then -J(↑b | a) else J(↑b | a)) = if flip = true then J(↑b | a) else -J(↑b | a)

Proof state:
case ind
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
⊢ (if ha4 : a % 4 = 0 then fastJacobiSymAux (a / 4) b flip ⋯
    else
      if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
      else
        if ha1 : a = 1 then if flip = true then -1 else 1
        else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
split <;> rename_i ha4

Result:
case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Proof state:
case ind
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
unfold fastJacobiSymAux

Result:
case ind
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
⊢ (if ha4 : a % 4 = 0 then fastJacobiSymAux (a / 4) b flip ⋯
    else
      if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
      else
        if ha1 : a = 1 then if flip = true then -1 else 1
        else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Proof state:
case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rw [IH (a / 4) (a.div_lt_self ha0 (by decide)) hb2 hb1]

Result:
case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ (if flip = true then -J(↑(a / 4) | b) else J(↑(a / 4) | b)) = if flip = true then -J(↑a | b) else J(↑a | b)