awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ (rhs a : (a : ℕ) → ℤ) (↑p : ℕ) = legendreSym p (↑a : ℤ)
have rw : J((↑p : ℤ) | a) = qrSign a p * J((↑a : ℤ) | p)
Tactic: rw [@legendreSym.to_jacobiSym p ⟨pp⟩, rhs_apply, Nat.cast_id, qrSign.eq_iff_eq hpo ha,
    qrSign.symm hpo ha]
-- 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)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J((↑p : ℤ) | a) = qrSign a p * J((↑a : ℤ) | p)
have refine : ∀ (q : ℕ) (pq : Nat.Prime q) (hq : q ≠ 2), legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
Tactic: refine value_at p (rhs p) (fun q pq hq => ?_) ha
-- 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
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have hqo : Odd q
Tactic: have hqo := pq.eq_two_or_odd'.resolve_left hq
-- 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)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw : legendreSym q (↑p : ℤ) = qrSign (↑q : ℕ) p * J((↑(↑q : ℕ) : ℤ) | p)
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]
-- 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)
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)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw₁ : legendreSym q (↑p : ℤ) = qrSign q p * J((↑q : ℤ) | p)
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]
-- 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)
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)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw₂ : legendreSym q (↑p : ℤ) = qrSign q p * legendreSym p (↑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]
-- 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)
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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw₃ : legendreSym q (↑p : ℤ) = qrSign p q * legendreSym p (↑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]
-- 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)
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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw₄ : legendreSym q (↑p : ℤ) = HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑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]
-- 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)
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 : ℤ)
⊢ legendreSym q (↑p : ℤ) = (rhs p : (a : ℕ) → ℤ) (↑q : ℕ)
have rw₅ : HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑q : ℤ) =
  HPow.hPow (α := ℤ) (-1) (p / 2 * (q / 2)) * legendreSym p (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
⊢ J((↑a : ℤ) | b) = HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a)
have rw : J((↑a : ℤ) | b) = qrSign a b * J((↑b : ℤ) | a)
Tactic: rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha : Odd a
hb : Odd b
rw : J((↑a : ℤ) | b) = qrSign a b * J((↑b : ℤ) | a)
⊢ J((↑a : ℤ) | b) = HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a)
have rw₁ : J((↑a : ℤ) | b) = qrSign b a * J((↑b : ℤ) | a)
Tactic: rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((↑a : ℤ) | b) = HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a)
have rw₂ : qrSign b a * J((↑b : ℤ) | a) = qrSign b a * J((↑b : ℤ) | a)
Tactic: rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)
have rw : HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha : a % 4 = 1
hb : Odd b
rw : HPow.hPow (α := ℤ) (-1) (a / 2 * (b / 2)) * J((↑b : ℤ) | a) = J((↑b : ℤ) | a)
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)
have rw₁ : HPow.hPow (α := ℤ) (-1) (a / 2) ^ (b / 2) * J((↑b : ℤ) | a) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)
have rw₂ : HPow.hPow (α := ℤ) 1 (b / 2) * J((↑b : ℤ) | a) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)
have rw₃ : 1 * J((↑b : ℤ) | a) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J((↑a : ℤ) | b) = J((↑b : ℤ) | a)
have rw₄ : J((↑b : ℤ) | a) = 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J((↑a : ℤ) | b) = -J((↑b : ℤ) | a)
have ha₁ : Odd a
Tactic: rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ J((↑a : ℤ) | b) = -J((↑b : ℤ) | a)
have hb₁ : Odd b
Tactic: rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Odd a
have ha₁ : a % 2 = 1
Tactic: rwa [odd_iff, odd_of_mod_four_eq_three]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Odd a
have ha₂ : Eq (α := ℕ) 1 1
Tactic: rwa [odd_iff, odd_of_mod_four_eq_three]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Odd b
have hb₁ : b % 2 = 1
Tactic: rwa [odd_iff, odd_of_mod_four_eq_three]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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
⊢ Odd b
have hb₂ : Eq (α := ℕ) 1 1
Tactic: rwa [odd_iff, odd_of_mod_four_eq_three]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
have inl : ∀ (ha1 : a % 4 = 1), (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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
have inr : ∀ (ha3 : a % 4 = 3), (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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha3 : a % 4 = 3
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
have inr : ∀ (hb1 : b % 4 = 1), (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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J((↑b : ℤ) | a) else J((↑b : ℤ) | a)) = J((↑a : ℤ) | b)
have inr₁ : ∀ (hb3 : b % 4 = 3), (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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)
Tactic: rcases eq_or_ne a 0 with (rfl | ha₀)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a b : ℕ
hb : Odd b
inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have inr : ∀ (ha₀ : a ≠ 0), J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
Tactic: rcases eq_or_ne a 0 with (rfl | ha₀)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb : Odd b
⊢ J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)
have inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % 0)
Tactic: rw [mul_zero, mod_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb : Odd b
inl : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % 0)
⊢ J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b % HMul.hMul (α := ℕ) 4 0)
have inl₁ : J((↑0 : ℤ) | b) = J((↑0 : ℤ) | b)
Tactic: rw [mul_zero, mod_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have hb' : Odd (b % (4 * a))
Tactic: have hb' : Odd (b % (4 * a)) := 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 ≠ 0
hb' : Odd (b % (4 * a))
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have inr : ∀ (e a' : ℕ) (ha₁' : ¬2 ∣ a') (ha₂ : a = HPow.hPow (α := ℕ) 2 e * 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₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
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'
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have ha₁ : Odd a'
Tactic: have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp 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))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
⊢ J((↑a : ℤ) | b) = J((↑a : ℤ) | b % (4 * a))
have inr : J((↑a : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
Tactic: nth_rw 2 [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))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
⊢ J((↑a : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
have inr : J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
Tactic: nth_rw 1 [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))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
⊢ J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b) = J((↑(HPow.hPow (α := ℕ) 2 e * a') : ℤ) | b % (4 * a))
have 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'))
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']
-- 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'
⊢ 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'))
have inr : HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
  HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e
Tactic: congr 1
-- 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 :
  HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e
⊢ 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'))
have inr₁ : qrSign b a' * J((↑b : ℤ) | a') = qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a')
Tactic: congr 1
-- 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'
⊢ qrSign b a' * J((↑b : ℤ) | a') = qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a')
have inr : qrSign b a' = qrSign (b % (4 * a)) a'
Tactic: congr 1
-- 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 : qrSign b a' = qrSign (b % (4 * a)) a'
⊢ qrSign b a' * J((↑b : ℤ) | a') = qrSign (b % (4 * a)) a' * J((↑(b % (4 * a)) : ℤ) | a')
have inr₁ : J((↑b : ℤ) | a') = J((↑(b % (4 * a)) : ℤ) | a')
Tactic: congr 1
-- 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'
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')
have inr : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : 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)]
-- 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 : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')
have inr₁ : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a) % 4) : ZMod 4) | a')
Tactic: rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 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))
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')
⊢ J((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % (4 * a)) : ZMod 4) | a')
have inr₂ : J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a') = J((χ₄ : (a : ZMod 4) → ℤ) (↑(b % 4) : ZMod 4) | a')
Tactic: rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 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))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
⊢ J((↑b : ℤ) | a') = J((↑(b % (4 * a)) : ℤ) | a')
have inr : Dvd.dvd (α := ℤ) (↑a' : ℤ) (↑(4 * a) : ℤ)
Tactic: rw [mod_left ↑(b % _), mod_left b, Int.natCast_mod, Int.emod_emod_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))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = HPow.hPow (α := ℕ) 2 e * a'
ha₁ : Odd a'
⊢ Dvd.dvd (α := ℤ) (↑a' : ℤ) (↑(4 * a) : ℤ)
have inr : (↑a' : ℤ) ∣ HMul.hMul (α := ℤ) (↑4 : ℤ) (↑(HPow.hPow (α := ℕ) 2 e) : ℤ) * (↑a' : ℤ)
Tactic: simp only [ha₂, Nat.cast_mul, ← mul_assoc]
-- 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'
⊢ HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑b : ZMod 8) : ℤ) e =
    HPow.hPow (α := ℤ) ((χ₈ : (a : ZMod 8) → ℤ) (↑(b % (4 * a)) : ZMod 8) : ℤ) e
have 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
Tactic: rcases e with - | e
Cleared hypotheses: e, ha₂