awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
inl : ∀ (ha1 : a % 4 = 1), (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
inr : ∀ (ha3 : a % 4 = 3), (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)

Tactic:
rcases Nat.odd_mod_four_iff.mp ha2 with ha1 | ha3

Premises used: Nat.odd_mod_four_iff, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha1 : a % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)

Tactic:
simpa [ha1] using jacobiSym.quadratic_reciprocity_one_mod_four' (Nat.odd_iff.mpr hb2) ha1

Premises used: Iff.mpr, jacobiSym.quadratic_reciprocity_one_mod_four', Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
inr : ∀ (hb1 : b % 4 = 1), (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
inr₁ : ∀ (hb3 : b % 4 = 3), (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)

Tactic:
rcases Nat.odd_mod_four_iff.mp hb2 with hb1 | hb3

Premises used: Nat.odd_mod_four_iff, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb1 : b % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)

Tactic:
simpa [hb1] using jacobiSym.quadratic_reciprocity_one_mod_four hb1 (Nat.odd_iff.mpr ha2)

Premises used: Iff.mpr, jacobiSym.quadratic_reciprocity_one_mod_four, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
hb3 : b % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)

Tactic:
simpa [ha3, hb3] using (jacobiSym.quadratic_reciprocity_three_mod_four ha3 hb3).symm

Premises used: jacobiSym.quadratic_reciprocity_three_mod_four, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)
inr : ∀ (ha₀ : a ≠ 0), J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))

Tactic:
rcases eq_or_ne a 0 with (rfl | ha₀)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % 0)
inl₁ inl₂ : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b)
⊢ J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)

Tactic:
rw [mul_zero, mod_zero]

Premises used: Nat.mod_zero, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ Even (α := ℕ) 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ Odd (b % (4 * a))

Tactic:
have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by decide) _)
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
⊢ Ne (α := ℕ) 2 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
inr : ∀ (e a' : ℕ) (ha₁' : ¬2 ∣ a') (ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'), J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))

Tactic:
rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by simp) with ⟨e, a', ha₁', ha₂⟩

Premises used: Nat.exists_eq_pow_mul_and_not_dvd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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'
⊢ Odd a'

Tactic:
have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁')
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : J((↑a : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))

Tactic:
nth_rw 2 [ha₂]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
⊢ J((↑a : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))

Tactic:
nth_rw 1 [ha₂]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 :
  HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e * (qrSign b a' * J((↑b : ℤ) | a')) =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e *
      (qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a'))
⊢ J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))

Tactic:
rw [Nat.cast_mul, mul_left, mul_left, quadratic_reciprocity' ha₁ hb,
    quadratic_reciprocity' ha₁ hb', Nat.cast_pow, pow_left, pow_left, Nat.cast_two, at_two hb,
    at_two hb']

Premises used: jacobiSym.pow_left, jacobiSym.mul_left, Nat.cast_mul, jacobiSym.at_two, Nat.cast_pow, jacobiSym.quadratic_reciprocity', Nat.cast_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 :
  HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e
inr₁ : qrSign b a' * J((↑b : ℤ) | a') = qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a')
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e * (qrSign b a' * J((↑b : ℤ) | a')) =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e *
      (qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a'))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : qrSign b a' = qrSign (b % (4 * a)) a'
inr₁ : J((↑b : ℤ) | a') = J((↑(b % (4 * a)) : ℤ) | a')
⊢ qrSign b a' * J((↑b : ℤ) | a') = qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a')

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')
inr₁ :
  J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a) % 4) : ZMod 4) | a')
inr₂ inr₃ : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a')
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')

Tactic:
rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)]

Premises used: HMul.hMul, HMod.hMod, Nat.mod_mod_of_dvd, dvd_mul_right, ZMod.χ₄_nat_mod_four, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : Dvd.dvd (α := ℤ) (↑a' : ℤ) (↑(4 * a) : ℤ)
⊢ J((↑b : ℤ) | a') = J((↑(b % (4 * a)) : ℤ) | a')

Tactic:
rw [mod_left ↑(b % _), mod_left b, Int.natCast_mod, Int.emod_emod_of_dvd b]

Premises used: jacobiSym.mod_left, Nat.cast, HMod.hMod, Int.emod_emod_of_dvd, Int.natCast_mod
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : (↑a' : ℤ) ∣ HMul.hMul (α := ℤ) (↑4 : ℤ) (↑(HPow.hPow (α := ℕ) 2 e) : ℤ) * (↑a' : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑a' : ℤ) (↑(4 * a) : ℤ)

Tactic:
simp only [ha₂, Nat.cast_mul, ← mul_assoc]

Premises used: mul_assoc, Nat.cast_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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'
⊢ (↑a' : ℤ) ∣ HMul.hMul (α := ℤ) (↑4 : ℤ) (↑(HPow.hPow (α := ℕ) 2 e) : ℤ) * (↑a' : ℤ)

Tactic:
apply dvd_mul_left

Premises used: dvd_mul_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
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)
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e

Tactic:
rcases e with - | e
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
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

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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'
inr : 8 ∣ 4 * a
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) (e + 1) =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) (e + 1)

Tactic:
rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]

Premises used: HMul.hMul, ZMod.χ₈_nat_mod_eight, HMod.hMod, Nat.mod_mod_of_dvd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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'
h : 4 * a = 8 * (HPow.hPow (α := ℕ) 2 e * a')
⊢ 8 ∣ 4 * a

Tactic:
use 2 ^ e * a'
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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'
h : 4 * (HPow.hPow (α := ℕ) 2 e * 2 * a') = 8 * (HPow.hPow (α := ℕ) 2 e * a')
⊢ 4 * a = 8 * (HPow.hPow (α := ℕ) 2 e * a')

Tactic:
rw [ha₂, Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 * (HPow.hPow (α := ℕ) 2 e * 2 * a') = 8 * (HPow.hPow (α := ℕ) 2 e * a')

Tactic:
ring
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
inl : ∀ (ha : a = (↑a.natAbs : ℤ)), J(a | b) = J(a | b % (4 * a.natAbs))
inr : ∀ (ha : a = -(↑a.natAbs : ℤ)), J(a | b) = J(a | b % (4 * a.natAbs))
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

Tactic:
rcases Int.natAbs_eq a with ha | ha

Premises used: Int.natAbs_eq
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
inr : J(a | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

Tactic:
nth_rw 2 [ha]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = (↑a.natAbs : ℤ)
inl : J((↑a.natAbs : ℤ) | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(a | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))

Tactic:
nth_rw 1 [ha]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
inr : J(-(↑a.natAbs : ℤ) | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))
⊢ J(a | b) = J(-(↑a.natAbs : ℤ) | b % (4 * a.natAbs))

Tactic:
nth_rw 1 [ha]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = (↑a.natAbs : ℤ)
⊢ J((↑a.natAbs : ℤ) | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))

Tactic:
mod_right' a.natAbs hb

Premises used: jacobiSym.mod_right', Int.natAbs
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = (↑a.natAbs : ℤ)
⊢ J((↑a.natAbs : ℤ) | b) = J((↑a.natAbs : ℤ) | b % (4 * a.natAbs))

Tactic:
exact mod_right' a.natAbs hb

Premises used: jacobiSym.mod_right', Int.natAbs
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
⊢ Even (α := ℕ) 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -(↑a.natAbs : ℤ)
⊢ Odd (b % (4 * a.natAbs))

Tactic:
have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by decide) _)
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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))
inr₅ 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))
⊢ 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 _)]

Premises used: HMul.hMul, jacobiSym.neg, HMod.hMod, Nat.mod_mod_of_dvd, jacobiSym.mod_right', dvd_mul_right, ZMod.χ₄_nat_mod_four, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : a % 4 = 0
⊢ LT.lt (α := ℕ) 0 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : a % 4 = 0
⊢ LT.lt (α := ℕ) 1 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : a % 4 = 0
⊢ a / 4 < a

Tactic:
exact a.div_lt_self ha0 (by decide)

Premises used: Nat.div_lt_self
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ a / 2 < a

Tactic:
exact a.div_lt_self ha0 (by decide)

Premises used: Nat.div_lt_self
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
⊢ b % a < a

Tactic:
b.mod_lt ha0

Premises used: Nat.mod_lt
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
⊢ b % a < a

Tactic:
exact b.mod_lt ha0

Premises used: Nat.mod_lt
-- 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
ind :
  (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)
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)

Tactic:
unfold fastJacobiSymAux

Premises used: _private.0.fastJacobiSymAux
-- 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
ind : ∀ (h : a % 4 = 0), fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J((↑a : ℤ) | b) else J((↑a : ℤ) | b)
ind₁ :
  ¬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)
⊢ (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
-- 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
⊢ LT.lt (α := ℕ) 1 4

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
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)
⊢ 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]

Premises used: HDiv.hDiv, Nat.div_lt_self, OfNat.ofNat
-- 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
⊢ (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:
simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]

Premises used: Nat.cast_ofNat, Int.natCast_ediv, congrArg, cast, jacobiSym.div_four_left, Nat.cast, HMod.hMod, Nat.cast_inj._simp_1, Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Eq.trans
-- 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
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)
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) ⋯) =
      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)

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
⊢ LT.lt (α := ℕ) 1 2

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
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)
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ =
    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]

Premises used: HDiv.hDiv, Nat.div_lt_self, OfNat.ofNat