awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (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)
have ind : a = 1 → (if flip = true then -1 else 1) = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (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)
have ind₁ : ¬a = 1 →
  (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) sorry) =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (if flip = true then -1 else 1) = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have 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)
Tactic: subst ha1
Cleared hypotheses: a, IH, ha0, ha4, ha2, ha1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (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)
have ind : b % a = 0 → 0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (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)
have ind₁ : ∀ (h : ¬b % a = 0),
  fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) sorry =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
Tactic: split
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ 0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have ind : J((↑a : ℤ) | b) = 0
Tactic: suffices J(a | b) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J((↑a : ℤ) | b) = 0
have ind : Int.gcd (↑a : ℤ) (↑b : ℤ) ≠ 1
Tactic: refine eq_zero_iff.mpr ⟨fun h ↦ absurd (h ▸ hb1) (by decide), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Int.gcd (↑a : ℤ) (↑b : ℤ) ≠ 1
have ind : a.gcd b ≠ 1
Tactic: rwa [Int.gcd_natCast_natCast, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero hba)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Int.gcd (↑a : ℤ) (↑b : ℤ) ≠ 1
have ind₁ : a ≠ 1
Tactic: rwa [Int.gcd_natCast_natCast, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero hba)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have 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)
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))]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (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)
have 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)
Tactic: simp only [Int.natCast_mod, ← mod_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (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)
have 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)
Tactic: rw [← quadratic_reciprocity_if (Nat.mod_two_ne_zero.mp ha2) hb2]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ (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)
have 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)
Tactic: by_cases h : a % 4 = 3 ∧ b % 4 = 3
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (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)
have 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)
Tactic: by_cases h : a % 4 = 3 ∧ b % 4 = 3
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
have pos : (if flip = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = if flip = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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 flip = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if flip = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
have pos : (if false = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
  if false = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
Tactic: cases flip
Cleared hypotheses: flip
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (if flip = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) =
    if flip = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
have pos₁ : (if true = false then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = if true = true then J((↑b : ℤ) | a) else -J((↑b : ℤ) | a)
Tactic: cases flip
Cleared hypotheses: flip
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a 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)
have 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)
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
Cleared hypotheses: a, b, flip, ha0, hb2, hb1
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
⊢ jacobiSym = fastJacobiSym
have h : ∀ (a : ℤ) (b : ℕ), J(a | b) = fastJacobiSym a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
⊢ J(a | b) = fastJacobiSym a b
have 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 := sorry;
        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 sorry
Tactic: unfold fastJacobiSym
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
⊢ 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 ⋯
have pos : ∀ (hb0 : b = 0), J(a | b) = 1
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
pos : ∀ (hb0 : b = 0), J(a | b) = 1
⊢ 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 ⋯
have pos₁ : ∀ (hb0 : ¬b = 0) (hb2 : b % 2 = 0) (ha2 : a % 2 = 0), J(a | b) = 0
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ 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 ⋯
have neg : ∀ (hb0 : ¬b = 0) (hb2 : b % 2 = 0) (ha2 : ¬a % 2 = 0),
  J(a | b) =
    have this := sorry;
    fastJacobiSym a (b / 2)
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ 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 ⋯
have pos₂ : ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : b = 1), J(a | b) = 1
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ 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 ⋯
have pos₃ : ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : ¬b = 1) (hab : a % (↑b : ℤ) = 0), J(a | b) = 0
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ 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 ⋯
have neg₁ : ∀ (hb0 : ¬b = 0) (hb2 : ¬b % 2 = 0) (hb1 : ¬b = 1) (hab : ¬a % (↑b : ℤ) = 0),
  J(a | b) = fastJacobiSymAux (a % (↑b : ℤ)).natAbs b false sorry
Tactic: split_ifs with hb0 hb2 ha2 hb1 hab
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : b = 0
⊢ J(a | b) = 1
have pos : J(a | 0) = 1
Tactic: rw [hb0, zero_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : b = 0
pos : J(a | 0) = 1
⊢ J(a | b) = 1
have pos₁ : Eq (α := ℤ) 1 1
Tactic: rw [hb0, zero_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
have pos : 1 < a.gcd (↑b : ℤ)
Tactic: refine eq_zero_iff.mpr ⟨hb0, ne_of_gt ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ 1 < a.gcd (↑b : ℤ)
have pos : Nat.succ 1 ∣ a.gcd (↑b : ℤ)
Tactic: refine Nat.le_of_dvd (Int.gcd_pos_iff.mpr (mod_cast .inr hb0)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : a % 2 = 0
⊢ Nat.succ 1 ∣ a.gcd (↑b : ℤ)
have pos : Nat.succ 1 ∣ Int.natAbs (↑b : ℤ)
Tactic: refine Nat.dvd_gcd (Int.ofNat_dvd_left.mp (Int.dvd_of_emod_eq_zero ha2)) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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) = fastJacobiSym a (b / 2)
have neg : J(a | b) = J(a | b / 2)
Tactic: rw [← IH (b / 2) (b.div_lt_self (Nat.pos_of_ne_zero hb0) one_lt_two)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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) = J(a | b / 2)
have neg : ∀ (b : ℕ) (IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m) (hb0 : ¬2 * b = 0) (hb2 : 2 * b % 2 = 0),
  J(a | 2 * b) = J(a | 2 * b / 2)
Tactic: obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2
Cleared hypotheses: b, IH, hb0, hb2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg : J(a | 2) * J(a | b) = J(a | 2 * b / 2)
Tactic: rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
      b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,
      Int.emod_two_ne_zero.mp ha2, one_left, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
neg : J(a | 2) * J(a | b) = J(a | 2 * b / 2)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₁ : J(a | 2) * J(a | b) = J(a | b)
Tactic: rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
      b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,
      Int.emod_two_ne_zero.mp ha2, one_left, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
neg : J(a | 2) * J(a | b) = J(a | 2 * b / 2)
neg₁ : J(a | 2) * J(a | b) = J(a | b)
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
have neg₂ : J(a % (↑2 : ℤ) | 2) * J(a | b) = J(a | b)
Tactic: rw [mul_right' a (by decide) fun h ↦ hb0 (mul_eq_zero_of_right 2 h),
      b.mul_div_cancel_left (by decide), mod_left a 2, Nat.cast_ofNat,
      Int.emod_two_ne_zero.mp ha2, one_left, one_mul]