awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)
rw : 0 ≤ HPow.hPow (β := ℕ) J(r.valMinAbs | b) 2
⊢ LE.le (α := ℤ) 0 (-1)

Tactic:
rw [← h, mod_left, ha, ← mod_left, pow_left]

Premises used: jacobiSym.mod_left, jacobiSym.pow_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)
⊢ 0 ≤ HPow.hPow (β := ℕ) J(r.valMinAbs | b) 2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
rw : legendreSym p a = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
⊢ J(a | p) = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
rw [← legendreSym.to_jacobiSym]

Premises used: jacobiSym.legendreSym.to_jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
legendreSym.eq_neg_one_iff p

Premises used: legendreSym.eq_neg_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
exact legendreSym.eq_neg_one_iff p

Premises used: legendreSym.eq_neg_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
h : J(a | p) = 1
rw : ¬Eq (α := ℤ) 1 (-1)
⊢ ¬¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]

Premises used: ZMod.nonsquare_iff_jacobiSym_eq_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬Eq (α := ℤ) 1 (-1)

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
⊢ J(-1 | b) = (χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4)

Tactic:
value_at (-1) χ₄.toMonoidHom (fun p pp => @legendreSym.at_neg_one p ⟨pp⟩) hb

Premises used: ZMod.χ₄, jacobiSym.value_at, legendreSym.at_neg_one, MulChar.toMonoidHom, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
hb : Odd b
rw : J(-1 * a | b) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)
rw₁ : J(-1 | b) * J(a | b) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)
rw₂ rw₃ :
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b) =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)
⊢ J(-a | b) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)

Tactic:
rw [neg_eq_neg_one_mul, mul_left, at_neg_one hb]

Premises used: jacobiSym.mul_left, neg_eq_neg_one_mul, jacobiSym.at_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
⊢ J(2 | b) = (χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8)

Tactic:
value_at 2 χ₈.toMonoidHom (fun p pp => @legendreSym.at_two p ⟨pp⟩) hb

Premises used: ZMod.χ₈, legendreSym.at_two, jacobiSym.value_at, MulChar.toMonoidHom, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
⊢ J(-2 | b) = (χ₈' : (a : ZMod 8) → ℤ) (↑b : ZMod 8)

Tactic:
value_at (-2) χ₈'.toMonoidHom (fun p pp => @legendreSym.at_neg_two p ⟨pp⟩) hb

Premises used: jacobiSym.value_at, MulChar.toMonoidHom, legendreSym.at_neg_two, ZMod.χ₈', OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
ha4 : a % 4 = 0
hb2 : b % 2 = 1
obtain : ∀ (a : ℤ) (ha4 : 4 * a % 4 = 0), J(4 * a / 4 | b) = J(4 * a | b)
⊢ J(a / 4 | b) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4

Premises used: Int.dvd_of_emod_eq_zero, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
rw : Nat.gcd 2 b = 1
rw₁ : Nat.gcd 2 (b % 2 + 2 * (b / 2)) = 1
rw₂ : Nat.gcd 2 (1 + 2 * (b / 2)) = 1
rw₃ : Nat.gcd 2 1 = 1
rw₄ rw₅ : Eq (α := ℕ) 1 1
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1

Tactic:
rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]

Premises used: Nat.gcd_one_right, Nat.mod_add_div, Nat.gcd_add_mul_left_right, Int.gcd_natCast_natCast, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1

Tactic:
have : Int.gcd (2 : ℕ) b = 1 := by
    rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
⊢ Ne (α := ℤ) 4 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
⊢ 4 = HPow.hPow (α := ℤ) (β := ℕ) (↑2 : ℤ) 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
rw : J(a | b) = J(4 * a | b)
rw₁ : J(a | b) = J(4 | b) * J(a | b)
rw₂ : J(a | b) = J(HPow.hPow (α := ℤ) (β := ℕ) (↑2 : ℤ) 2 | b) * J(a | b)
rw₃ : J(a | b) = 1 * J(a | b)
rw₄ rw₅ : J(a | b) = J(a | b)
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Tactic:
rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
    (by decide : (4 : ℤ) = (2 : ℕ) ^ 2), jacobiSym.sq_one' this, one_mul]

Premises used: jacobiSym.mul_left, Int.mul_ediv_cancel_left, jacobiSym.sq_one', one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
⊢ HMod.hMod (α := ℤ) 4 4 = 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
⊢ J(4 | b) = J(4 / 4 | b)

Tactic:
have : J((4 : ℤ) | b) = J((4 : ℤ) / 4 | b) :=
    (div_four_left (by decide) (Nat.odd_iff.mp hb)).symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : Odd b
this : J(4 | b) = J(4 / 4 | b)
⊢ J(4 | b) = 1

Tactic:
simpa [one_left]

Premises used: jacobiSym.one_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
ha2 : a % 2 = 0
hb2 : b % 2 = 1
obtain :
  ∀ (a : ℤ) (ha2 : 2 * a % 2 = 0),
    (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2

Premises used: Int.dvd_of_emod_eq_zero, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ Ne (α := ℤ) 2 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
rw : (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)

Tactic:
rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
    jacobiSym.at_two (Nat.odd_iff.mpr hb2), ZMod.χ₈_nat_eq_if_mod_eight,
    if_neg (Nat.mod_two_ne_zero.mpr hb2)]

Premises used: Iff.mpr, jacobiSym.mul_left, Int.mul_ediv_cancel_left, jacobiSym.at_two, ZMod.χ₈_nat_eq_if_mod_eight, Nat.mod_two_ne_zero, if_neg, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)

Tactic:
grind
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
rw :
  J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
⊢ qrSign m n = HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2))

Tactic:
rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]

Premises used: qrSign, pow_mul, ZMod.χ₄_eq_neg_one_pow, Iff.mp, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
inl :
  ∀ (h : m % 4 = 1),
    J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) =
      HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
inr :
  ∀ (h : m % 4 = 3),
    J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) =
      HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)

Tactic:
rcases odd_mod_four_iff.mp (odd_iff.mp hm) with h | h

Premises used: Nat.odd_mod_four_iff, Iff.mp, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
inl : J(1 | n) = HPow.hPow (α := ℤ) 1 (n / 2)
inl₁ : 1 = HPow.hPow (α := ℤ) 1 (n / 2)
inl₂ inl₃ : Eq (α := ℤ) 1 1
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)

Tactic:
rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]

Premises used: one_pow, ZMod.χ₄_nat_one_mod_four, jacobiSym.one_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
inr : J(-1 | n) = HPow.hPow (α := ℤ) (-1) (n / 2)
inr₁ : J(-1 | n) = (χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4)
inr₂ inr₃ : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)

Tactic:
rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]

Premises used: ZMod.χ₄_nat_three_mod_four, ZMod.χ₄_eq_neg_one_pow, Iff.mp, jacobiSym.at_neg_one, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2))) 2 = 1
rw₁ : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2) * 2) = 1
rw₂ : HPow.hPow (α := ℤ) (-1) (2 * (m / 2 * (n / 2))) = 1
rw₃ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 2 ^ (m / 2 * (n / 2)) = 1
rw₄ : HPow.hPow (α := ℤ) 1 (m / 2 * (n / 2)) = 1
rw₅ rw₆ : Eq (α := ℤ) 1 1
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1

Tactic:
rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

Premises used: one_pow, neg_one_sq, qrSign.neg_one_pow, pow_mul, mul_comm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m₁ m₂ n : ℕ
simp_rw :
  J((χ₄ : (a : ZMod 4) → ℤ) (↑(m₁ * m₂) : ZMod 4) | n) =
    J((χ₄ : (a : ZMod 4) → ℤ) (↑m₁ : ZMod 4) | n) * J((χ₄ : (a : ZMod 4) → ℤ) (↑m₂ : ZMod 4) | n)
simp_rw₁ :
  J((χ₄ : (a : ZMod 4) → ℤ) (HMul.hMul (α := ZMod 4) (↑m₁ : ZMod 4) (↑m₂ : ZMod 4)) | n) =
    J((χ₄ : (a : ZMod 4) → ℤ) (↑m₁ : ZMod 4) | n) * J((χ₄ : (a : ZMod 4) → ℤ) (↑m₂ : ZMod 4) | n)
simp_rw₂ :
  J(HMul.hMul (α := ℤ) (β := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m₁ : ZMod 4) : ℤ)
        ((χ₄ : (a : ZMod 4) → ℤ) (↑m₂ : ZMod 4) : ℤ) |
      n) =
    J((χ₄ : (a : ZMod 4) → ℤ) (↑m₁ : ZMod 4) | n) * J((χ₄ : (a : ZMod 4) → ℤ) (↑m₂ : ZMod 4) | n)
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

Tactic:
simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]

Premises used: qrSign, jacobiSym.mul_left, map_mul, Nat.cast_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n₁ n₂ : ℕ
inst : NeZero n₁
inst_1 : NeZero n₂
⊢ qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂

Tactic:
jacobiSym.mul_right (χ₄ m) n₁ n₂

Premises used: jacobiSym.mul_right, ZMod.χ₄, qrSign, Nat.cast, DFunLike.coe
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
rw : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2)) = qrSign n m
rw₁ : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2)) = HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2))
rw₂ rw₃ : HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2)) = HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2))
⊢ qrSign m n = qrSign n m

Tactic:
rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]

Premises used: qrSign.neg_one_pow, HDiv.hDiv, mul_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
⊢ qrSign m n * x = y ↔ x = qrSign m n * y

Tactic:
⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩

Premises used: Iff.intro, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
refine_1 : ∀ (h' : qrSign m n * x = y), x = qrSign m n * y
refine_2 : ∀ (h : x = qrSign m n * y), qrSign m n * x = y
⊢ qrSign m n * x = y ↔ x = qrSign m n * y

Tactic:
refine
      ⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := ⋯
refine_1 : x = qrSign m n * (qrSign m n * x)
refine_1₁ : x = qrSign m n * qrSign m n * x
refine_1₂ : x = HPow.hPow (β := ℕ) (qrSign m n) 2 * x
refine_1₃ : x = 1 * x
refine_1₄ refine_1₅ : x = x
⊢ x = qrSign m n * y

Tactic:
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

Premises used: pow_two, mul_assoc, qrSign.sq_eq_one, one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
refine_2 : qrSign m n * (qrSign m n * y) = y
refine_2₁ : qrSign m n * qrSign m n * y = y
refine_2₂ : HPow.hPow (β := ℕ) (qrSign m n) 2 * y = y
refine_2₃ : 1 * y = y
refine_2₄ refine_2₅ : y = y
⊢ qrSign m n * x = y

Tactic:
rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]

Premises used: pow_two, mul_assoc, qrSign.sq_eq_one, one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ qrSign 1 a * 1 = qrSign 1 a

Tactic:
mul_one (M := ℤ) _

Premises used: mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
h : 1 = J((↑1 : ℤ) | a)
h₁ : qrSign 1 a = 1
⊢ qrSign 1 a * J((↑1 : ℤ) | a) = 1

Tactic:
convert! ← mul_one (M := ℤ) _

Premises used: mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
h : J((↑1 : ℤ) | a) = 1
⊢ 1 = J((↑1 : ℤ) | a)

Tactic:
symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
h : J((↑1 : ℤ) | a) = 1
⊢ 1 = J((↑1 : ℤ) | a)

Tactic:
on_goal 1 => symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ J((↑1 : ℤ) | a) = 1

Tactic:
apply one_left

Premises used: jacobiSym.one_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ qrSign 1 a = 1

Tactic:
apply one_left

Premises used: jacobiSym.one_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a x y : ℕ
simp_rw :
  qrSign x a * qrSign y a * J((↑(x * y) : ℤ) | a) = qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
simp_rw₁ :
  qrSign x a * qrSign y a * J(HMul.hMul (α := ℤ) (↑x : ℤ) (↑y : ℤ) | a) =
    qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
simp_rw₂ :
  qrSign x a * qrSign y a * (J((↑x : ℤ) | a) * J((↑y : ℤ) | a)) =
    qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
⊢ qrSign (x * y) a * J((↑(x * y) : ℤ) | a) = qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))

Tactic:
simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]

Premises used: mul_mul_mul_comm, jacobiSym.mul_left, Nat.cast_mul, qrSign.mul_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
⊢ ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)

Tactic:
have rhs_apply : ∀ a b : ℕ, rhs a b = qrSign b a * J(b | a) := fun a b => rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
⊢ J((↑a : ℤ) | b) = qrSign b a * J((↑b : ℤ) | a)

Tactic:
value_at a (rhs a) (fun p pp hp => Eq.symm ?_) hb

Premises used: Nat.cast, jacobiSym.value_at, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
refine : ∀ (p : ℕ) (pp : Nat.Prime p) (hp : p ≠ 2), (rhs a : (a : ℕ) → ℤ) (↑p : ℕ) = legendreSym p (↑a : ℤ)
⊢ J((↑a : ℤ) | b) = qrSign b a * J((↑b : ℤ) | a)

Tactic:
refine value_at a (rhs a) (fun p pp hp => Eq.symm ?_) hb

Premises used: Nat.cast, jacobiSym.value_at, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
⊢ Odd p

Tactic:
have hpo := pp.eq_two_or_odd'.resolve_left hp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
rw : J((↑p : ℤ) | a) = qrSign a p * J((↑a : ℤ) | p)
⊢ (rhs a : (a : ℕ) → ℤ) (↑p : ℕ) = legendreSym p (↑a : ℤ)

Tactic:
rw [@legendreSym.to_jacobiSym p ⟨pp⟩, rhs_apply, Nat.cast_id, qrSign.eq_iff_eq hpo ha,
    qrSign.symm hpo ha]

Premises used: Nat.cast_id, jacobiSym.legendreSym.to_jacobiSym, qrSign.symm, qrSign.eq_iff_eq
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J((↑p : ℤ) | a) = qrSign a p * J((↑a : ℤ) | p)

Tactic:
value_at p (rhs p) (fun q pq hq => ?_) ha

Premises used: Nat.cast, jacobiSym.value_at
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
refine : ∀ (q : ℕ) (pq : Nat.Prime q) (hq : q ≠ 2), legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
⊢ J((↑p : ℤ) | a) = qrSign a p * J((↑a : ℤ) | p)

Tactic:
refine value_at p (rhs p) (fun q pq hq => ?_) ha

Premises used: Nat.cast, jacobiSym.value_at
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
⊢ Odd q

Tactic:
have hqo := pq.eq_two_or_odd'.resolve_left hq
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun (a : ℕ) ↦ { toFun := fun (x : ℕ) ↦ qrSign x a * J((↑x : ℤ) | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a : (a : ℕ) → ℤ) b = qrSign b a * J((↑b : ℤ) | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
rw : legendreSym q (↑p : ℤ) = qrSign (↑q : ℕ) p * J((↑(↑q : ℕ) : ℤ) | p)
rw₁ : legendreSym q (↑p : ℤ) = qrSign q p * J((↑q : ℤ) | p)
rw₂ : legendreSym q (↑p : ℤ) = qrSign q p * legendreSym p (↑q : ℤ)
rw₃ : legendreSym q (↑p : ℤ) = qrSign p q * legendreSym p (↑q : ℤ)
rw₄ : legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
rw₅ rw₆ :
  HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ) =
    HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)

Tactic:
rw [rhs_apply, Nat.cast_id, ← @legendreSym.to_jacobiSym p ⟨pp⟩, qrSign.symm hqo hpo,
    qrSign.neg_one_pow hpo hqo, @legendreSym.quadratic_reciprocity' p q ⟨pp⟩ ⟨pq⟩ hp hq]

Premises used: Nat.cast_id, jacobiSym.legendreSym.to_jacobiSym, qrSign.neg_one_pow, legendreSym.quadratic_reciprocity', qrSign.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rw : J((↑a : ℤ) | b) = qrSign a b * J((↑b : ℤ) | a)
rw₁ : J((↑a : ℤ) | b) = qrSign b a * J((↑b : ℤ) | a)
rw₂ rw₃ : qrSign b a * J((↑b : ℤ) | a) = qrSign b a * J((↑b : ℤ) | a)
⊢ J((↑a : ℤ) | b) = HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a)

Tactic:
rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]

Premises used: qrSign.neg_one_pow, qrSign.symm, jacobiSym.quadratic_reciprocity'
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : a % 4 = 1
hb : Odd b
rw : HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
rw₁ : HPow.hPow (α := ℤ) (-1) (a / 2) ^ (b / 2) * J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
rw₂ : HPow.hPow (α := ℤ) 1 (b / 2) * J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
rw₃ : 1 * J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
rw₄ rw₅ : J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)

Tactic:
rw [quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, pow_mul,
    neg_one_pow_div_two_of_one_mod_four ha, one_pow, one_mul]

Premises used: Iff.mpr, one_pow, ZMod.neg_one_pow_div_two_of_one_mod_four, Nat.odd_of_mod_four_eq_one, pow_mul, jacobiSym.quadratic_reciprocity, Nat.odd_iff, one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : Odd a
hb : b % 4 = 1
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)

Tactic:
(quadratic_reciprocity_one_mod_four hb ha).symm

Premises used: jacobiSym.quadratic_reciprocity_one_mod_four, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
ha₁ : Odd a
hb₁ : Odd b
⊢ J((↑a : ℤ) | b) = -J((↑b : ℤ) | a)

Tactic:
rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul]

Premises used: neg_one_mul, pow_mul, jacobiSym.quadratic_reciprocity
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
ha₁ : a % 2 = 1
ha₂ : Eq (α := ℕ) 1 1
ha₃ : a % 4 = 3
ha₄ : Eq (α := ℕ) 1 1
ha₅ ha₆ ha₇ : a % 4 = 3
⊢ Odd a

Tactic:
rwa [odd_iff, odd_of_mod_four_eq_three]

Premises used: Nat.odd_of_mod_four_eq_three, Nat.odd_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ} (hn : n % 4 = 3), HPow.hPow (α := ℤ) (-1) (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
hb₁ : b % 2 = 1
hb₂ : Eq (α := ℕ) 1 1
hb₃ : b % 4 = 3
hb₄ : Eq (α := ℕ) 1 1
hb₅ hb₆ hb₇ : b % 4 = 3
⊢ Odd b

Tactic:
rwa [odd_iff, odd_of_mod_four_eq_three]

Premises used: Nat.odd_of_mod_four_eq_three, Nat.odd_iff