awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
Tactic: have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
⊢ Eq (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑a : ZMod p)
have norm_cast : Eq (α := ZMod p) (↑a : ZMod p) (↑a : ZMod p)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
Tactic: rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have rw₁ : HPow.hPow (α := ℤ) (-1)
    #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) =
  HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
Tactic: rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₁ :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have rw₂ : HPow.hPow (α := ℤ) (-1)
    (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) % 2) =
  HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
Tactic: rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₁ :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₂ :
  HPow.hPow (α := ℤ) (-1)
      (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) % 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have rw₃ : HPow.hPow (α := ℤ) (-1)
    (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) % 2) =
  HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
Tactic: rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
hp' : Fact (p % 2 = 1)
ha0' : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
rw : legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₁ :
  HPow.hPow (α := ℤ) (-1)
      #({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₂ :
  HPow.hPow (α := ℤ) (-1)
      (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑(↑a : ℤ) : ZMod p) (↑x : ZMod p)).val}) % 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
rw₃ :
  HPow.hPow (α := ℤ) (-1)
      (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (HMul.hMul (α := ZMod p) (↑a : ZMod p) (↑x : ZMod p)).val}) % 2) =
    HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
⊢ legendreSym p (↑a : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (-1) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p)
have rw₄ : HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2) =
  HPow.hPow (α := ℤ) (-1) (HMod.hMod (α := ℕ) (∑ x ∈ Ico 1 (p / 2).succ, x * a / p) 2)
Tactic: rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)
have rw : HMul.hMul (α := ℤ)
    (List.prod (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₁.primeFactorsList sorry))
    (List.prod (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₂.primeFactorsList sorry)) =
  J(a | b₁) * J(a | b₂)
Tactic: rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append,
    List.prod_append]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
rw :
  HMul.hMul (α := ℤ)
      (List.prod (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₁.primeFactorsList ⋯))
      (List.prod
        (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b₂.primeFactorsList ⋯)) =
    J(a | b₁) * J(a | b₂)
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)
have rw₁ : ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a
Tactic: rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append,
    List.prod_append]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
⊢ {0, 1, -1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)
have rw : {0, -1, 1} = (↑(MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) : Set ℤ)
Tactic: rw [Set.pair_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
x : ℤ
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯) x
⊢ Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯) x
have rcases : ∀ (p : ℕ) (hp : p ∈ b.primeFactorsList)
  (ha' :
    Membership.mem (γ := List ℤ)
      (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList sorry)
      (legendreSym p a)),
  Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} sorry)
    (legendreSym p a)
Tactic: rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
Cleared hypotheses: x, ha'
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (hypothesis)
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯)
    (legendreSym p a)
⊢ Membership.mem (γ := Submonoid ℤ)
    (Submonoid.copy (MonoidHom.mrange (F := SignType →* ℤ) (↑SignType.castHom : SignType →* ℤ)) {0, 1, -1} ⋯)
    (legendreSym p a)
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
z : ℤ
hz :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p 1) b.primeFactorsList ⋯) z
⊢ z = 1
have let : ∀ (p : ℕ) (hp : p ∈ b.primeFactorsList) (he : legendreSym p 1 = z), z = 1
Tactic: let ⟨p, hp, he⟩ := List.mem_pmap.1 hz
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
z : ℤ
hz :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p 1) b.primeFactorsList ⋯) z
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ z = 1
have rw : legendreSym p 1 = 1
Tactic: rw [← he, legendreSym.at_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
z : ℤ
hz :
  Membership.mem (γ := List ℤ)
    (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p 1) b.primeFactorsList ⋯) z
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
rw : legendreSym p 1 = 1
⊢ z = 1
have rw₁ : Eq (α := ℤ) 1 1
Tactic: rw [← he, legendreSym.at_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a₁ a₂ : ℤ
b : ℕ
⊢ J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)
have simp_rw : List.prod
    (List.map (fun (x : { x : ℕ // x ∈ b.primeFactorsList }) ↦ legendreSym (↑x : ℕ) a₁ * legendreSym (↑x : ℕ) a₂)
      b.primeFactorsList.attach) =
  HMul.hMul (α := ℤ)
    (List.prod
      (List.map (fun (x : { x : ℕ // x ∈ b.primeFactorsList }) ↦ legendreSym (↑x : ℕ) a₁) b.primeFactorsList.attach))
    (List.prod
      (List.map (fun (x : { x : ℕ // x ∈ b.primeFactorsList }) ↦ legendreSym (↑x : ℕ) a₂) b.primeFactorsList.attach))
Tactic: simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
⊢ Membership.mem (γ := List ℤ)
      (List.pmap (P := Nat.Prime) (fun (p : ℕ) (pp : Nat.Prime p) ↦ legendreSym p a) b.primeFactorsList ⋯) 0 ↔
    a.gcd (↑b : ℤ) ≠ 1
have rw : (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
  ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
Tactic: rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw : (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
  ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₁ : (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
  ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₁ :
  (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₂ : (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
  ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₁ :
  (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₂ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₃ : (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
  ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₁ :
  (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₂ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₃ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₄ : (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₁ :
  (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₂ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₃ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
simp_rw₄ : (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₅ : (∃ (a_1 : ℕ), (Nat.Prime a_1 ∧ a_1 ∣ b) ∧ (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
inst : NeZero b
simp_rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), Eq (α := ZMod a_1) (↑a : ZMod a_1) 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₁ :
  (∃ (a_1 : ℕ) (_ : a_1 ∈ b.primeFactorsList), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₂ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
simp_rw₃ :
  (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑b : ℤ)
simp_rw₄ : (∃ (a_1 : ℕ) (_ : Nat.Prime a_1 ∧ a_1 ∣ b), (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
simp_rw₅ : (∃ (a_1 : ℕ), (Nat.Prime a_1 ∧ a_1 ∣ b) ∧ (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
⊢ (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑b : ℤ)
have simp_rw₆ : (∃ (a_1 : ℕ), Nat.Prime a_1 ∧ a_1 ∣ b ∧ (↑a_1 : ℤ) ∣ a) ↔ ∃ (p : ℕ), Nat.Prime p ∧ (↑p : ℤ) ∣ a ∧ p ∣ b
Tactic: simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd,
        mem_primeFactorsList (NeZero.ne b), ← Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop,
        and_assoc, _root_.and_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
⊢ J(a | b) ≠ 0
have inl : ∀ (hb : b = 0), J(a | b) ≠ 0
Tactic: rcases eq_zero_or_neZero b with hb | _
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
inl : ∀ (hb : b = 0), J(a | b) ≠ 0
⊢ J(a | b) ≠ 0
have inr : NeZero b → J(a | b) ≠ 0
Tactic: rcases eq_zero_or_neZero b with hb | _
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
hb : b = 0
⊢ J(a | b) ≠ 0
have inl : Ne (α := ℤ) 1 0
Tactic: rw [hb, zero_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h_1 : NeZero b
⊢ J(a | b) ≠ 0
have inr : ∀ (h : J(a | b) = 0), a.gcd (↑b : ℤ) ≠ 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ Int.gcd 0 (↑b : ℤ) ≠ 1
have rw : b ≠ 1
Tactic: rw [Int.gcd_zero_left, Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b : ℕ
⊢ J(a ^ zero | b) = J(a | b) ^ zero
have rw : J(1 | b) = J(a | b) ^ zero
Tactic: rw [_root_.pow_zero, _root_.pow_zero, one_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b : ℕ
rw : J(1 | b) = J(a | b) ^ zero
⊢ J(a ^ zero | b) = J(a | b) ^ zero
have rw₁ : J(1 | b) = 1
Tactic: rw [_root_.pow_zero, _root_.pow_zero, one_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b : ℕ
rw : J(1 | b) = J(a | b) ^ zero
rw₁ : J(1 | b) = 1
⊢ J(a ^ zero | b) = J(a | b) ^ zero
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [_root_.pow_zero, _root_.pow_zero, one_left]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b x : ℕ
ih : J(a ^ x | b) = J(a | b) ^ x
⊢ J(a ^ x.succ | b) = J(a | b) ^ x.succ
have rw : J(a ^ x * a | b) = J(a | b) ^ x.succ
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b x : ℕ
ih : J(a ^ x | b) = J(a | b) ^ x
rw : J(a ^ x * a | b) = J(a | b) ^ x.succ
⊢ J(a ^ x.succ | b) = J(a | b) ^ x.succ
have rw₁ : J(a ^ x * a | b) = J(a | b) ^ x * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b x : ℕ
ih : J(a ^ x | b) = J(a | b) ^ x
rw : J(a ^ x * a | b) = J(a | b) ^ x.succ
rw₁ : J(a ^ x * a | b) = J(a | b) ^ x * J(a | b)
⊢ J(a ^ x.succ | b) = J(a | b) ^ x.succ
have rw₂ : J(a ^ x | b) * J(a | b) = J(a | b) ^ x * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
e b x : ℕ
ih : J(a ^ x | b) = J(a | b) ^ x
rw : J(a ^ x * a | b) = J(a | b) ^ x.succ
rw₁ : J(a ^ x * a | b) = J(a | b) ^ x * J(a | b)
rw₂ : J(a ^ x | b) * J(a | b) = J(a | b) ^ x * J(a | b)
⊢ J(a ^ x.succ | b) = J(a | b) ^ x.succ
have rw₃ : J(a | b) ^ x * J(a | b) = J(a | b) ^ x * J(a | b)
Tactic: rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
⊢ J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
have zero : J(a | 1) = HPow.hPow (β := ℕ) J(a | b) 0
Tactic: rw [Nat.pow_zero, _root_.pow_zero, one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
zero : J(a | 1) = HPow.hPow (β := ℕ) J(a | b) 0
⊢ J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
have zero₁ : J(a | 1) = 1
Tactic: rw [Nat.pow_zero, _root_.pow_zero, one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b : ℕ
zero : J(a | 1) = HPow.hPow (β := ℕ) J(a | b) 0
zero₁ : J(a | 1) = 1
⊢ J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
have zero₂ : Eq (α := ℤ) 1 1
Tactic: rw [Nat.pow_zero, _root_.pow_zero, one_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ : ∀ (hb : b = 0), J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
Tactic: rcases eq_zero_or_neZero b with hb | _
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol (goal)
Goal:
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
succ : ∀ (hb : b = 0), J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ₁ : NeZero b → J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
Tactic: rcases eq_zero_or_neZero b with hb | _
-- 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
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
have succ : J(a | HPow.hPow (α := ℕ) 0 (e + 1)) = J(a | 0) ^ (e + 1)
Tactic: rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]