awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
have rw : Nat.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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
rw : Nat.gcd 2 b = 1
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
have rw₁ : Nat.gcd 2 (b % 2 + 2 * (b / 2)) = 1
Tactic: rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
have rw₂ : Nat.gcd 2 (1 + 2 * (b / 2)) = 1
Tactic: rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
have rw₃ : Nat.gcd 2 1 = 1
Tactic: rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
have rw₄ : Eq (α := ℕ) 1 1
Tactic: rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have this : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : Int.gcd (↑2 : ℤ) (↑b : ℤ) = 1
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have rw : J(a | 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have rw₁ : J(a | b) = J(4 | b) * J(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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have rw₂ : J(a | b) = J(HPow.hPow (α := ℤ) (β := ℕ) (↑2 : ℤ) 2 | b) * J(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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have rw₃ : J(a | b) = 1 * J(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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(4 * a / 4 | b) = J(4 * a | b)
have rw₄ : J(a | b) = J(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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
b : ℕ
hb : Odd b
⊢ J(4 | b) = 1
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
ha2 : a % 2 = 0
hb2 : b % 2 = 1
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)
have 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)
Tactic: obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2
Cleared hypotheses: a, ha2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb2 : b % 2 = 1
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)
have 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)
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2))
have rw : J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
Tactic: rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inl : ∀ (h : m % 4 = 1),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inr : ∀ (h : m % 4 = 3),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inl : J(1 | n) = HPow.hPow (α := ℤ) 1 (n / 2)
Tactic: rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
inl : J(1 | n) = HPow.hPow (α := ℤ) 1 (n / 2)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inl₁ : 1 = HPow.hPow (α := ℤ) 1 (n / 2)
Tactic: rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inl₂ : Eq (α := ℤ) 1 1
Tactic: rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inr : J(-1 | n) = HPow.hPow (α := ℤ) (-1) (n / 2)
Tactic: rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
inr : J(-1 | n) = HPow.hPow (α := ℤ) (-1) (n / 2)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inr₁ : J(-1 | n) = (χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4)
Tactic: rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) | n) = HPow.hPow (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑m : ZMod 4) : ℤ) (n / 2)
have inr₂ : Eq (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑n : ZMod 4) : ℤ)
Tactic: rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2))) 2 = 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2))) 2 = 1
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw₁ : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2) * 2) = 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw₂ : HPow.hPow (α := ℤ) (-1) (2 * (m / 2 * (n / 2))) = 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw₃ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 2 ^ (m / 2 * (n / 2)) = 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw₄ : HPow.hPow (α := ℤ) 1 (m / 2 * (n / 2)) = 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ HPow.hPow (β := ℕ) (qrSign m n) 2 = 1
have rw₅ : Eq (α := ℤ) 1 1
Tactic: rw [neg_one_pow hm hn, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m₁ m₂ n : ℕ
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
have 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)
Tactic: simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
have 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)
Tactic: simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
have 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)
Tactic: simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = qrSign n m
have rw : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2)) = qrSign n m
Tactic: rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
rw : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2)) = qrSign n m
⊢ qrSign m n = qrSign n m
have rw₁ : HPow.hPow (α := ℤ) (-1) (m / 2 * (n / 2)) = HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2))
Tactic: rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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))
⊢ qrSign m n = qrSign n m
have rw₂ : HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2)) = HPow.hPow (α := ℤ) (-1) (n / 2 * (m / 2))
Tactic: rw [neg_one_pow hm hn, neg_one_pow hn hm, mul_comm (m / 2)]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
⊢ qrSign m n * x = y ↔ x = qrSign m n * y
have refine_1 : ∀ (h' : qrSign m n * x = y), x = qrSign m n * y
Tactic: refine
      ⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
refine_1 : ∀ (h' : qrSign m n * x = y), x = qrSign m n * y
⊢ qrSign m n * x = y ↔ x = qrSign m n * y
have refine_2 : ∀ (h : x = qrSign m n * y), qrSign m n * x = y
Tactic: refine
      ⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := ⋯
⊢ x = qrSign m n * y
have refine_1 : x = qrSign m n * (qrSign m n * x)
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ x = qrSign m n * y
have refine_1₁ : x = qrSign m n * qrSign m n * x
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ x = qrSign m n * y
have refine_1₂ : x = HPow.hPow (β := ℕ) (qrSign m n) 2 * x
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ x = qrSign m n * y
have refine_1₃ : x = 1 * x
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ x = qrSign m n * y
have refine_1₄ : x = x
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y
have refine_2 : qrSign m n * (qrSign m n * y) = y
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ qrSign m n * x = y
have refine_2₁ : qrSign m n * qrSign m n * y = y
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ qrSign m n * x = y
have refine_2₂ : HPow.hPow (β := ℕ) (qrSign m n) 2 * y = y
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ qrSign m n * x = y
have refine_2₃ : 1 * y = y
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ qrSign m n * x = y
have refine_2₄ : y = y
Tactic: rw [h, ← mul_assoc, ← pow_two, sq_eq_one hm hn, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ qrSign 1 a * J((↑1 : ℤ) | a) = 1
have h : 1 = J((↑1 : ℤ) | a)
Tactic: convert! ← mul_one (M := ℤ) _
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
h : 1 = J((↑1 : ℤ) | a)
⊢ qrSign 1 a * J((↑1 : ℤ) | a) = 1
have h₁ : qrSign 1 a = 1
Tactic: convert! ← mul_one (M := ℤ) _
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ 1 = J((↑1 : ℤ) | a)
have h : J((↑1 : ℤ) | a) = 1
Tactic: symm
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a : ℕ
⊢ 1 = J((↑1 : ℤ) | a)
have h : J((↑1 : ℤ) | a) = 1
Tactic: on_goal 1 => symm
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a_1 b : ℕ
ha : Odd a_1
hb : Odd b
a x y : ℕ
⊢ qrSign (x * y) a * J((↑(x * y) : ℤ) | a) = qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
have simp_rw : qrSign x a * qrSign 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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))
⊢ qrSign (x * y) a * J((↑(x * y) : ℤ) | a) = qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
have 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))
Tactic: simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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))
⊢ qrSign (x * y) a * J((↑(x * y) : ℤ) | a) = qrSign x a * J((↑x : ℤ) | a) * (qrSign y a * J((↑y : ℤ) | a))
have 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))
Tactic: simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
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' := ⋯ }
⊢ J((↑a : ℤ) | b) = qrSign b a * J((↑b : ℤ) | a)
have rhs_apply : ∀ (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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
have refine : ∀ (p : ℕ) (pp : Nat.Prime p) (hp : p ≠ 2), (rhs a : (a : ℕ) → ℤ) (↑p : ℕ) = legendreSym p (↑a : ℤ)
Tactic: refine value_at a (rhs a) (fun p pp hp => Eq.symm ?_) hb
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
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
⊢ (rhs a : (a : ℕ) → ℤ) (↑p : ℕ) = legendreSym p (↑a : ℤ)
have hpo : Odd p
Tactic: have hpo := pp.eq_two_or_odd'.resolve_left hp