awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind :
  (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then
      -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J((↑(a / 2) : ℤ) | b) else J((↑(a / 2) : ℤ) | b)) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
simp only [Int.natCast_ediv, Nat.cast_ofNat, ← even_odd (a := a) (mod_cast ha2) hb2]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, congrArg, cast, Nat.cast, HMod.hMod, Nat.cast_inj._simp_1, Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Eq.trans, jacobiSym.even_odd
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
pos :
  ∀ (h : b % 8 = 3 ∨ b % 8 = 5),
    (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
      else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
      if flip = true then
        -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
      else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
neg :
  ∀ (h : ¬(b % 8 = 3 ∨ b % 8 = 5)),
    (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
      else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
      if flip = true then
        -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
      else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then
      -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
by_cases h : b % 8 = 3 ∨ b % 8 = 5
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
h : b % 8 = 3 ∨ b % 8 = 5
pos :
  (if flip = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then
      -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
h : ¬(b % 8 = 3 ∨ b % 8 = 5)
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then
      -if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
h : b % 8 = 3 ∨ b % 8 = 5
pos :
  (if false = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if false = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
pos₁ :
  (if true = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if true = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)
⊢ (if flip = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if flip = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
cases flip
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
      fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if false = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if false = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
      fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b)
b : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if true = false then -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)) =
    if true = true then J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b) else -J(HDiv.hDiv (α := ℤ) (↑a : ℤ) 2 | b)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind : a = 1 → (if flip = true then -1 else 1) = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
ind₁ :
  ¬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)
⊢ (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind :
  ∀
    (IH :
      ∀ m < 1,
        ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
          fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b))
    {ha0 : GT.gt (α := ℕ) 1 0} (ha4 : ¬HMod.hMod (α := ℕ) 1 4 = 0) (ha2 : ¬HMod.hMod (α := ℕ) 1 2 = 0),
    (if flip = true then -1 else 1) = if flip = true then -J((↑1 : ℤ) | b) else J((↑1 : ℤ) | b)
⊢ (if flip = true then -1 else 1) = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
subst ha1
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
flip : Bool
hb2 : b % 2 = 1
hb1 : b > 1
IH :
  ∀ m < 1,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
      fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b)
ha0 : GT.gt (α := ℕ) 1 0
ha4 : ¬HMod.hMod (α := ℕ) 1 4 = 0
ha2 : ¬HMod.hMod (α := ℕ) 1 2 = 0
⊢ (if flip = true then -1 else 1) = if flip = true then -J((↑1 : ℤ) | b) else J((↑1 : ℤ) | b)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind : b % a = 0 → 0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
ind₁ :
  ∀ (h : ¬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)
⊢ (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
this : J((↑a : ℤ) | b) = 0
⊢ 0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
simp [this]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind : J((↑a : ℤ) | b) = 0
⊢ 0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
suffices J(a | b) = 0 by simp [this]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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 : b = 0
⊢ ¬GT.gt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind : Int.gcd (↑a : ℤ) (↑b : ℤ) ≠ 1
⊢ J((↑a : ℤ) | b) = 0

Tactic:
refine eq_zero_iff.mpr ⟨fun h ↦ absurd (h ▸ hb1) (by decide), ?_⟩

Premises used: Iff.mpr, absurd, And.intro, jacobiSym.eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind : a.gcd b ≠ 1
ind₁ ind₂ ind₃ ind₄ : a ≠ 1
⊢ Int.gcd (↑a : ℤ) (↑b : ℤ) ≠ 1

Tactic:
rwa [Int.gcd_natCast_natCast, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero hba)]

Premises used: Nat.gcd_eq_left, Nat.dvd_of_mod_eq_zero, Int.gcd_natCast_natCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind :
  (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J((↑(b % a) : ℤ) | a) else J((↑(b % a) : ℤ) | a)) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
rw [IH (b % a) (b.mod_lt ha0) (Nat.mod_two_ne_zero.mp ha2) (lt_of_le_of_ne ha0 (Ne.symm ha1))]

Premises used: Ne.symm, Nat.mod_lt, HMod.hMod, Iff.mp, Nat.mod_two_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind :
  (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J((↑(b % a) : ℤ) | a) else J((↑(b % a) : ℤ) | a)) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
simp only [Int.natCast_mod, ← mod_left]

Premises used: jacobiSym.mod_left, Int.natCast_mod
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
ind :
  (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)
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
rw [← quadratic_reciprocity_if (Nat.mod_two_ne_zero.mp ha2) hb2]

Premises used: Iff.mp, jacobiSym.quadratic_reciprocity_if, Nat.mod_two_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
pos :
  ∀ (h : a % 4 = 3 ∧ b % 4 = 3),
    (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)
neg :
  ∀ (h : ¬(a % 4 = 3 ∧ b % 4 = 3)),
    (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)
⊢ (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
pos :
  (if flip = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if flip = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
⊢ (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:
simp [h]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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 (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:
simp [h]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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
pos :
  (if false = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if false = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
pos₁ :
  (if true = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if true = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
⊢ (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
      fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b)
b : ℕ
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 false = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if false = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : b > 1),
      fastJacobiSymAux m b flip ha0 = if flip = true then -J((↑m : ℤ) | b) else J((↑m : ℤ) | b)
b : ℕ
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 true = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if true = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ind :
  ∀ (a : ℕ)
    (IH :
      ∀ m < a,
        ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0} (hb2 : b % 2 = 1) (hb1 : 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)
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
induction a using Nat.strongRecOn generalizing b flip with | ind a IH =>
  unfold fastJacobiSymAux
  split <;> rename_i ha4
  · rw [IH (a / 4) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]
  split <;> rename_i ha2
  · rw [IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, ← even_odd (a := a) (mod_cast ha2) hb2]
    by_cases h : b % 8 = 3 ∨ b % 8 = 5 <;> simp [h]; cases flip <;> simp
  split <;> rename_i ha1
  · subst ha1; simp
  split <;> rename_i hba
  · suffices J(a | b) = 0 by simp [this]
    refine eq_zero_iff.mpr ⟨fun h ↦ absurd (h ▸ hb1) (by decide), ?_⟩
    rwa [Int.gcd_natCast_natCast, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero hba)]
  rw [IH (b % a) (b.mod_lt ha0) (Nat.mod_two_ne_zero.mp ha2) (lt_of_le_of_ne ha0 (Ne.symm ha1))]
  simp only [Int.natCast_mod, ← mod_left]
  rw [← quadratic_reciprocity_if (Nat.mod_two_ne_zero.mp ha2) hb2]
  by_cases h : a % 4 = 3 ∧ b % 4 = 3 <;> simp [h]; cases flip <;> simp

Premises used: _private.0.fastJacobiSymAux, Iff.mpr, Nat.cast_ofNat, Int.natCast_ediv, jacobiSym.mod_left, absurd, And.intro, Int.gcd_natCast_natCast, jacobiSym.eq_zero_iff, Int.natCast_mod
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
h : ∀ (a : ℤ) (b : ℕ), J(a | b) = fastJacobiSym a b
⊢ jacobiSym = fastJacobiSym

Tactic:
ext a b
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
h :
  J(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 ⋯
⊢ J(a | b) = fastJacobiSym a b

Tactic:
unfold fastJacobiSym

Premises used: _private.0.fastJacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
pos : ∀ (hb0 : b = 0), J(a | b) = 1
pos₁ : ∀ (hb0 : ¬b = 0) (hb2 : b % 2 = 0) (ha2 : a % 2 = 0), J(a | b) = 0
neg :
  ∀ (hb0 : ¬b = 0) (hb2 : b % 2 = 0) (ha2 : ¬a % 2 = 0),
    J(a | b) =
      have this := ⋯;
      fastJacobiSym a (b / 2)
pos₂ : ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : b = 1), J(a | b) = 1
pos₃ : ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : ¬b = 1) (hab : a % (↑b : ℤ) = 0), J(a | b) = 0
neg₁ :
  ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : ¬b = 1) (hab : ¬a % (↑b : ℤ) = 0),
    J(a | b) = fastJacobiSymAux (a % (↑b : ℤ)).natAbs b false ⋯
⊢ J(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 ⋯

Tactic:
split_ifs with hb0 hb2 ha2 hb1 hab
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : b = 0
pos : J(a | 0) = 1
pos₁ pos₂ : Eq (α := ℤ) 1 1
⊢ J(a | b) = 1

Tactic:
rw [hb0, zero_right]

Premises used: jacobiSym.zero_right
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ J(a | b) = 0

Tactic:
eq_zero_iff.mpr ⟨hb0, ne_of_gt ?_⟩

Premises used: Iff.mpr, ne_of_gt, And.intro, jacobiSym.eq_zero_iff