awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
inr :
  ∀ (ha₂ : a = HPow.hPow (α := ℕ) (β := ℕ) 2 0 * a'),
    HPow.hPow (α := ℤ) (β := ℕ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) 0 =
      HPow.hPow (α := ℤ) (β := ℕ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) 0
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e
have inr₁ : ∀ (e : ℕ) (ha₂ : a = HPow.hPow (α := ℕ) 2 (e + 1) * a'),
  HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) (e + 1) =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) (e + 1)
Tactic: rcases e with - | e
Cleared hypotheses: e, ha₂
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = HPow.hPow (α := ℕ) 2 (e + 1) * a'
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) (e + 1) =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) (e + 1)
have inr : 8 ∣ 4 * a
Tactic: rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = HPow.hPow (α := ℕ) 2 (e + 1) * a'
⊢ 8 ∣ 4 * a
have h : 4 * a = 8 * (HPow.hPow (α := ℕ) 2 e * a')
Tactic: use 2 ^ e * a'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = HPow.hPow (α := ℕ) 2 (e + 1) * a'
⊢ 4 * a = 8 * (HPow.hPow (α := ℕ) 2 e * a')
have h : 4 * (HPow.hPow (α := ℕ) 2 e * 2 * a') = 8 * (HPow.hPow (α := ℕ) 2 e * a')
Tactic: rw [ha₂, Nat.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
⊢ J(a | b) = J(a | b % (4 * a.natAbs))
have inl : ∀ (ha : a = (↑a.natAbs : ℤ)), J(a | b) = J(a | b % (4 * a.natAbs))
Tactic: rcases Int.natAbs_eq a with ha | ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
inl : ∀ (ha : a = (↑a.natAbs : ℤ)), J(a | b) = J(a | b % (4 * a.natAbs))
⊢ J(a | b) = J(a | b % (4 * a.natAbs))
have inr : ∀ (ha : a = -(↑a.natAbs : ℤ)), J(a | b) = J(a | b % (4 * a.natAbs))
Tactic: rcases Int.natAbs_eq a with ha | ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
⊢ J(a | b) = J(a | b % (4 * a.natAbs))
have inr : J(a | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: nth_rw 2 [ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = (↑a.natAbs : ℤ)
⊢ J(a | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inl : J((↑a.natAbs : ℤ) | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: nth_rw 1 [ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
⊢ J(a | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr : J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: nth_rw 1 [ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have hb' : Odd (b % (4 * a.natAbs))
Tactic: have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by decide) _)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
  J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
inr :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr₁ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
    J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
inr :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₁ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr₂ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
    J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
inr :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₁ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₂ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr₃ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
    J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
inr :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₁ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₂ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₃ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr₄ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs) % 4) : ZMod 4) : ℤ)
    J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
hb' : Odd (b % (4 * a.natAbs))
inr :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₁ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₂ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₃ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs)) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
inr₄ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a.natAbs) % 4) : ZMod 4) : ℤ)
      J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
have inr₅ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs)) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) : ℤ) J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
Tactic: rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
      χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]
-- 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
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have ind : (if ha4 : a % 4 = 0 then fastJacobiSymAux (a / 4) b flip sorry
  else
    if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) sorry
    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) sorry) =
  if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
Tactic: unfold fastJacobiSymAux
-- 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
⊢ (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)
have ind : ∀ (h : a % 4 = 0), fastJacobiSymAux (a / 4) b 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
ind : ∀ (h : a % 4 = 0), fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
⊢ (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)
have ind₁ : ¬a % 4 = 0 →
  (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) sorry
    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) 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
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have ind : (if flip = true then -J((↑(a / 4) : ℤ) | b) else J((↑(a / 4) : ℤ) | b)) =
  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]
-- 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
⊢ (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)
have ind : ∀ (h : a % 2 = 0),
  fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ 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
ind :
  ∀ (h : a % 2 = 0),
    fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ =
      if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
⊢ (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)
have ind₁ : ¬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) 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
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ =
    if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
have ind : (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: rw [IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1]
-- 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 (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)
have 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)
Tactic: simp only [Int.natCast_ediv, Nat.cast_ofNat, ← even_odd (a := a) (mod_cast 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
⊢ (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)
have 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)
Tactic: by_cases h : b % 8 = 3 ∨ b % 8 = 5
-- 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
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)
⊢ (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)
have 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)
Tactic: by_cases h : b % 8 = 3 ∨ b % 8 = 5
-- 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
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)
have 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)
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
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (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)
have 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)
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
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)
⊢ (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)
have 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)
Tactic: cases flip
Cleared hypotheses: flip