awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
succ : J(a | HPow.hPow (α := ℕ) 0 (e + 1)) = J(a | 0) ^ (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₁ : J(a | 0) = J(a | 0) ^ (e + 1)
Tactic: rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
succ : J(a | HPow.hPow (α := ℕ) 0 (e + 1)) = J(a | 0) ^ (e + 1)
succ₁ : J(a | 0) = J(a | 0) ^ (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₂ : 1 = HPow.hPow (α := ℤ) 1 (e + 1)
Tactic: rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
succ : J(a | HPow.hPow (α := ℕ) 0 (e + 1)) = J(a | 0) ^ (e + 1)
succ₁ : J(a | 0) = J(a | 0) ^ (e + 1)
succ₂ : 1 = HPow.hPow (α := ℤ) 1 (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₃ : Eq (α := ℤ) 1 1
Tactic: rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ : J(a | b ^ e * b) = J(a | b) ^ (e + 1)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h : NeZero b
succ : J(a | b ^ e * b) = J(a | b) ^ (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₁ : J(a | b ^ e * b) = J(a | b) ^ e * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h : NeZero b
succ : J(a | b ^ e * b) = J(a | b) ^ (e + 1)
succ₁ : J(a | b ^ e * b) = J(a | b) ^ e * J(a | b)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₂ : J(a | b ^ e) * J(a | b) = J(a | b) ^ e * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h : NeZero b
succ : J(a | b ^ e * b) = J(a | b) ^ (e + 1)
succ₁ : J(a | b ^ e * b) = J(a | b) ^ e * J(a | b)
succ₂ : J(a | b ^ e) * J(a | b) = J(a | b) ^ e * J(a | b)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₃ : J(a | b) ^ e * J(a | b) = J(a | b) ^ e * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
⊢ J(a | b ^ e) = J(a | b) ^ e
have zero : J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
Tactic: induction e with
  | zero => rw [Nat.pow_zero, _root_.pow_zero, one_right]
  | succ e ih =>
    rcases eq_zero_or_neZero b with hb | _
    · rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
    · rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
zero : J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
⊢ J(a | b ^ e) = J(a | b) ^ e
have succ : ∀ (e : ℕ) (ih : J(a | b ^ e) = J(a | b) ^ e), J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
Tactic: induction e with
  | zero => rw [Nat.pow_zero, _root_.pow_zero, one_right]
  | succ e ih =>
    rcases eq_zero_or_neZero b with hb | _
    · rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
    · rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1
have inl : ∀ (h₁ : J(a | b) = 1), HPow.hPow (β := ℕ) J(a | b) 2 = 1
Tactic: rcases eq_one_or_neg_one h with h₁ | h₁
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
inl : ∀ (h₁ : J(a | b) = 1), HPow.hPow (β := ℕ) J(a | b) 2 = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1
have inr : ∀ (h₁ : J(a | b) = -1), HPow.hPow (β := ℕ) J(a | b) 2 = 1
Tactic: rcases eq_one_or_neg_one h with h₁ | h₁
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1
have inl : HPow.hPow (α := ℤ) (β := ℕ) 1 2 = 1
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = -1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1
have inr : HPow.hPow (α := ℤ) (β := ℕ) (-1) 2 = 1
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
⊢ J(HPow.hPow (β := ℕ) a 2 | b) = 1
have rw : HPow.hPow (β := ℕ) J(a | b) 2 = 1
Tactic: rw [pow_left, sq_one h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
rw : HPow.hPow (β := ℕ) J(a | b) 2 = 1
⊢ J(HPow.hPow (β := ℕ) a 2 | b) = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [pow_left, sq_one h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁ h₂ : Nat.Prime p
| legendreSym p (a % (↑b : ℤ))
have rw : legendreSym p a
Tactic: rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁ h₂ : Nat.Prime p
⊢ legendreSym p a = legendreSym p (a % (↑b : ℤ))
have conv_rhs : legendreSym p a = legendreSym p (a % (↑b : ℤ))
Tactic: conv_rhs =>
          rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁ h₂ : Nat.Prime p
conv_rhs : legendreSym p a = legendreSym p (a % (↑b : ℤ))
⊢ legendreSym p a = legendreSym p (a % (↑b : ℤ))
have conv_rhs₁ : legendreSym p a = legendreSym p a
Tactic: conv_rhs =>
          rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % (↑b : ℤ) = a₂ % (↑b : ℤ)
⊢ J(a₁ | b) = J(a₂ | b)
have rw : J(a₁ % (↑b : ℤ) | b) = J(a₂ | b)
Tactic: rw [mod_left, h, ← mod_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % (↑b : ℤ) = a₂ % (↑b : ℤ)
rw : J(a₁ % (↑b : ℤ) | b) = J(a₂ | b)
⊢ J(a₁ | b) = J(a₂ | b)
have rw₁ : J(a₂ % (↑b : ℤ) | b) = J(a₂ | b)
Tactic: rw [mod_left, h, ← mod_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % (↑b : ℤ) = a₂ % (↑b : ℤ)
rw : J(a₁ % (↑b : ℤ) | b) = J(a₂ | b)
rw₁ : J(a₂ % (↑b : ℤ) | b) = J(a₂ | b)
⊢ J(a₁ | b) = J(a₂ | b)
have rw₂ : J(a₂ | b) = J(a₂ | b)
Tactic: rw [mod_left, h, ← mod_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = -1
x y : ℤ
hxy : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2
⊢ (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y
have rw : ∀ (h : legendreSym p a = -1) {x y : ℤ} (hxy : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2),
  (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y
Tactic: rw [← legendreSym.to_jacobiSym] at h
Cleared hypotheses: h, x, y, hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
n_1 : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))
have cons : J((n :: l').prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
n_1 : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
cons : J((n :: l').prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))
have cons₁ : J(n * l'.prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
n_1 : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
cons : J((n :: l').prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
cons₁ : J(n * l'.prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))
have cons₂ : J(n * l'.prod | n_1) = J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
n_1 : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
cons : J((n :: l').prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
cons₁ : J(n * l'.prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
cons₂ : J(n * l'.prod | n_1) = J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))
have cons₃ : J(n | n_1) * J(l'.prod | n_1) = J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
n_1 : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
cons : J((n :: l').prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
cons₁ : J(n * l'.prod | n_1) = (J(n | n_1) :: List.map (fun (a : ℤ) ↦ J(a | n_1)) l').prod
cons₂ : J(n * l'.prod | n_1) = J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
cons₃ : J(n | n_1) * J(l'.prod | n_1) = J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))
have cons₄ : J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l') =
  J(n | n_1) * List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
l : List ℤ
n : ℕ
⊢ J(l.prod | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) l)
have nil : J(List.prod [] | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) [])
Tactic: induction l with
  | nil => simp only [List.prod_nil, List.map_nil, one_left]
  | cons n l' ih => rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
l : List ℤ
n : ℕ
nil : J(List.prod [] | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) [])
⊢ J(l.prod | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) l)
have cons : ∀ (n_1 : ℤ) (l' : List ℤ) (ih : J(l'.prod | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) l')),
  J((n_1 :: l').prod | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) (n_1 :: l'))
Tactic: induction l with
  | nil => simp only [List.prod_nil, List.map_nil, one_left]
  | cons n l' ih => rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have hn : n ≠ 0
Tactic: have hn := hl n List.mem_cons_self
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have hl' : l'.prod ≠ 0
Tactic: have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
Tactic: have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have cons : J(a | (n :: l').prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
cons : J(a | (n :: l').prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have cons₁ : J(a | n * l'.prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
cons : J(a | (n :: l').prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
cons₁ : J(a | n * l'.prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have cons₂ : J(a | n * l'.prod) = J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
cons : J(a | (n :: l').prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
cons₁ : J(a | n * l'.prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
cons₂ : J(a | n * l'.prod) = J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have cons₃ : J(a | n) * J(a | l'.prod) = J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
l' : List ℕ
ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0
cons : J(a | (n :: l').prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
cons₁ : J(a | n * l'.prod) = (J(a | n) :: List.map (fun (n : ℕ) ↦ J(a | n)) l').prod
cons₂ : J(a | n * l'.prod) = J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
cons₃ : J(a | n) * J(a | l'.prod) = J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
have cons₄ : J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l') =
  J(a | n) * List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l')
Tactic: rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
l : List ℕ
hl : ∀ n ∈ l, n ≠ 0
⊢ J(a | l.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l)
have nil : ∀ (hl : ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n ≠ 0),
  J(a | List.prod []) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) [])
Tactic: induction l with
  | nil => simp only [List.prod_nil, one_right, List.map_nil]
  | cons n l' ih =>
    have hn := hl n List.mem_cons_self
    -- `n ≠ 0`
    have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
    -- `l'.prod ≠ 0`
    have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
    -- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
    rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
l : List ℕ
hl : ∀ n ∈ l, n ≠ 0
nil :
  ∀ (hl : ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n ≠ 0),
    J(a | List.prod []) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) [])
⊢ J(a | l.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l)
have cons : ∀ (n : ℕ) (l' : List ℕ)
  (ih : ∀ (hl : ∀ n ∈ l', n ≠ 0), J(a | l'.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) l'))
  (hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0), J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))
Tactic: induction l with
  | nil => simp only [List.prod_nil, one_right, List.map_nil]
  | cons n l' ih =>
    have hn := hl n List.mem_cons_self
    -- `n ≠ 0`
    have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
    -- `l'.prod ≠ 0`
    have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
    -- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
    rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
h : J(a | 0) = -1
⊢ False
have h₁ : Eq (α := ℤ) 1 0
Tactic: rw [zero_right, CharZero.eq_neg_self_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
have hn₀ : n ≠ 0
Tactic: have hn₀ : n ≠ 0 := by
    rintro rfl
    rw [zero_right, CharZero.eq_neg_self_iff] at h
    exact one_ne_zero h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
have hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
Tactic: have hf₀ (p) (hp : p ∈ n.primeFactorsList) : p ≠ 0 := (Nat.pos_of_mem_primeFactorsList hp).ne.symm
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
have h₁ : Eq (α := ℤ) (List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) n.primeFactorsList)) (-1)
Tactic: rw [← Nat.prod_primeFactorsList hn₀, list_prod_right hf₀] at h
Cleared hypotheses: h, hn₀, hf₀
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
n : ℕ
h : Eq (α := ℤ) (List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) n.primeFactorsList)) (-1)
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
have obtain : ∀ (p : ℕ) (hmem : p ∈ n.primeFactorsList) (hj : J(a | p) = -1), ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
Tactic: obtain ⟨p, hmem, hj⟩ := List.mem_map.mp (List.neg_one_mem_of_prod_eq_neg_one h)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : (↑a : ZMod b) = r * r
⊢ False
have ha₁ : a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)
Tactic: rw [← r.coe_valMinAbs, ← Int.cast_mul, intCast_eq_intCast_iff', ← sq] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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 : ℤ)
⊢ False
have apply : LE.le (α := ℤ) 0 (-1)
Tactic: apply (by simp : ¬(0 : ℤ) ≤ -1)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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 : ℤ)
⊢ LE.le (α := ℤ) 0 (-1)
have rw : 0 ≤ HPow.hPow (β := ℕ) J(r.valMinAbs | b) 2
Tactic: rw [← h, mod_left, ha, ← mod_left, pow_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
⊢ J(a | p) = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
have rw : legendreSym p a = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
Tactic: rw [← legendreSym.to_jacobiSym]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
p : ℕ
inst : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬¬IsSquare (α := ZMod p) (↑a : ZMod p)
have rw : ¬Eq (α := ℤ) 1 (-1)
Tactic: rw [← nonsquare_iff_jacobiSym_eq_neg_one, h]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
⊢ J(-a | b) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)
have rw : J(-1 * 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
hb : Odd b
rw : J(-1 * 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)
have rw₁ : J(-1 | 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
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)
⊢ J(-a | b) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) J(a | b)
have rw₂ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑b : ZMod 4) : ℤ) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
ha4 : a % 4 = 0
hb2 : b % 2 = 1
⊢ J(a / 4 | b) = J(a | b)
have obtain : ∀ (a : ℤ) (ha4 : 4 * a % 4 = 0), J(4 * a / 4 | b) = J(4 * a | b)
Tactic: obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4
Cleared hypotheses: a, ha4