awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ z = 1

Tactic:
rw [← he, legendreSym.at_one]

Premises used: legendreSym.at_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a₁ a₂ : ℤ
b : ℕ
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))
⊢ J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b)

Tactic:
simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _]

Premises used: List.pmap_eq_map_attach, legendreSym.mul, jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a₁ a₂ : ℤ
b : ℕ
⊢ 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:
List.prod_map_mul (l := (primeFactorsList b).attach)
    (f := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₁)
    (g := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₂)

Premises used: List.prod_map_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a₁ a₂ : ℤ
b : ℕ
⊢ 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:
exact List.prod_map_mul (l := (primeFactorsList b).attach)
    (f := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₁)
    (g := fun x ↦ @legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₂)

Premises used: List.prod_map_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
inst : NeZero b
rw :
  (∃ (a_1 : ℕ) (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ Int.natAbs (↑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

Tactic:
rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]

Premises used: Ne, Int.gcd_eq_natAbs, List.mem_pmap, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
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 : ℤ)

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]

Premises used: and_comm, exists_prop, Nat.mem_primeFactorsList, ZMod.intCast_zmod_eq_zero_iff_dvd, legendreSym.eq_zero_iff, and_assoc, Int.natCast_dvd, Int.natCast_dvd_natCast, NeZero.ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
inl : ∀ (hb : b = 0), J(a | b) ≠ 0
inr : NeZero b → J(a | b) ≠ 0
⊢ J(a | b) ≠ 0

Tactic:
rcases eq_zero_or_neZero b with hb | _

Premises used: eq_zero_or_neZero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
hb : b = 0
inl : Ne (α := ℤ) 1 0
⊢ J(a | b) ≠ 0

Tactic:
rw [hb, zero_right]

Premises used: jacobiSym.zero_right
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
hb : b = 0
⊢ Ne (α := ℤ) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
hb : b = 0
⊢ Ne (α := ℤ) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h_1 : NeZero b
inr : ∀ (h : J(a | b) = 0), a.gcd (↑b : ℤ) ≠ 1
⊢ J(a | b) ≠ 0

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h_1 : NeZero b
h : J(a | b) = 0
⊢ a.gcd (↑b : ℤ) ≠ 1

Tactic:
eq_zero_iff_not_coprime.1 h

Premises used: jacobiSym.eq_zero_iff_not_coprime, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h_1 : NeZero b
h : J(a | b) = 0
⊢ a.gcd (↑b : ℤ) ≠ 1

Tactic:
exact eq_zero_iff_not_coprime.1 h

Premises used: jacobiSym.eq_zero_iff_not_coprime, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : 1 < b
rw : b ≠ 1
⊢ Int.gcd 0 (↑b : ℤ) ≠ 1

Tactic:
rw [Int.gcd_zero_left, Int.natAbs_natCast]

Premises used: Int.natAbs_natCast, Int.gcd_zero_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : 1 < b
⊢ b ≠ 1

Tactic:
hb.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
b : ℕ
hb : 1 < b
⊢ b ≠ 1

Tactic:
exact hb.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
⊢ J(a | b) = 1 ∨ J(a | b) = -1

Tactic:
(trichotomy a b).resolve_left <| jacobiSym.ne_zero h

Premises used: jacobiSym.trichotomy, jacobiSym.ne_zero, Or.resolve_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
e b : ℕ
rw : J(1 | b) = J(a | b) ^ zero
rw₁ : J(1 | b) = 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ J(a ^ zero | b) = J(a | b) ^ zero

Tactic:
rw [_root_.pow_zero, _root_.pow_zero, one_left]

Premises used: pow_zero, jacobiSym.one_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)
rw₃ rw₄ : J(a | b) ^ x * J(a | b) = J(a | b) ^ x * J(a | b)
⊢ J(a ^ x.succ | b) = J(a | b) ^ x.succ

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

Premises used: pow_succ, jacobiSym.mul_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
zero : J(a | 1) = HPow.hPow (β := ℕ) J(a | b) 0
zero₁ : J(a | 1) = 1
zero₂ zero₃ : Eq (α := ℤ) 1 1
⊢ J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0

Tactic:
rw [Nat.pow_zero, _root_.pow_zero, one_right]

Premises used: jacobiSym.one_right, pow_zero, Nat.pow_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)
succ₁ : NeZero b → J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rcases eq_zero_or_neZero b with hb | _

Premises used: eq_zero_or_neZero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)
succ₃ succ₄ : Eq (α := ℤ) 1 1
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]

Premises used: one_pow, Nat.succ_ne_zero, jacobiSym.zero_right, zero_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)
succ₃ 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)

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]

Premises used: jacobiSym.mul_right, pow_succ
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b e : ℕ
zero : J(a | HPow.hPow (β := ℕ) b 0) = HPow.hPow (β := ℕ) J(a | b) 0
succ : ∀ (e : ℕ) (ih : J(a | b ^ e) = J(a | b) ^ e), J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
⊢ J(a | b ^ e) = J(a | b) ^ e

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]

Premises used: one_pow, jacobiSym.mul_right, pow_succ, jacobiSym.one_right, pow_zero, Nat.pow_zero, Nat.succ_ne_zero, jacobiSym.zero_right, Nat.zero, Nat.succ, eq_zero_or_neZero, zero_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
inl : ∀ (h₁ : J(a | b) = 1), HPow.hPow (β := ℕ) J(a | b) 2 = 1
inr : ∀ (h₁ : J(a | b) = -1), HPow.hPow (β := ℕ) J(a | b) 2 = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1

Tactic:
rcases eq_one_or_neg_one h with h₁ | h₁

Premises used: jacobiSym.eq_one_or_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = 1
inl : HPow.hPow (α := ℤ) (β := ℕ) 1 2 = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1

Tactic:
rw [h₁]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = -1
inr : HPow.hPow (α := ℤ) (β := ℕ) (-1) 2 = 1
⊢ HPow.hPow (β := ℕ) J(a | b) 2 = 1

Tactic:
rw [h₁]
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) 1 2 = 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
h₁ : J(a | b) = -1
⊢ HPow.hPow (α := ℤ) (β := ℕ) (-1) 2 = 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : a.gcd (↑b : ℤ) = 1
rw : HPow.hPow (β := ℕ) J(a | b) 2 = 1
rw₁ rw₂ : Eq (α := ℤ) 1 1
⊢ J(HPow.hPow (β := ℕ) a 2 | b) = 1

Tactic:
rw [pow_left, sq_one h]

Premises used: jacobiSym.sq_one, jacobiSym.pow_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁ h₂ : Nat.Prime p
rw : legendreSym p a
| legendreSym p (a % (↑b : ℤ))

Tactic:
rw [legendreSym.mod, Int.emod_emod_of_dvd _ (Int.natCast_dvd_natCast.2 <|
            dvd_of_mem_primeFactorsList hp), ← legendreSym.mod]

Premises used: Iff.mpr, legendreSym.mod, Int.emod_emod_of_dvd, Int.natCast_dvd_natCast, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁ h₂ : Nat.Prime p
conv_rhs : legendreSym p a = legendreSym p (a % (↑b : ℤ))
conv_rhs₁ : legendreSym p a = legendreSym p a
⊢ 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]

Premises used: Iff.mpr, legendreSym.mod, Int.emod_emod_of_dvd, Int.natCast_dvd_natCast, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)
rw₂ rw₃ : J(a₂ | b) = J(a₂ | b)
⊢ J(a₁ | b) = J(a₂ | b)

Tactic:
rw [mod_left, h, ← mod_left]

Premises used: jacobiSym.mod_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
rw :
  ∀ (h : legendreSym p a = -1) {x y : ℤ} (hxy : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2),
    (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y
⊢ (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y

Tactic:
rw [← legendreSym.to_jacobiSym] at h

Premises used: jacobiSym.legendreSym.to_jacobiSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2
⊢ (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y

Tactic:
legendreSym.prime_dvd_of_eq_neg_one h hxy

Premises used: legendreSym.prime_dvd_of_eq_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : (↑p : ℤ) ∣ HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2
⊢ (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y

Tactic:
exact legendreSym.prime_dvd_of_eq_neg_one h hxy

Premises used: legendreSym.prime_dvd_of_eq_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
n : ℕ
⊢ J(List.prod [] | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) [])

Tactic:
simp only [List.prod_nil, List.map_nil, one_left]

Premises used: jacobiSym.one_left, List.prod_nil, List.map_nil
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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')
cons₄ 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')
⊢ J((n :: l').prod | n_1) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n_1)) (n :: l'))

Tactic:
rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

Premises used: List.map, jacobiSym.mul_left, List.prod_cons
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
l : List ℤ
n : ℕ
nil : J(List.prod [] | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) [])
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'))
⊢ J(l.prod | n) = List.prod (List.map (fun (a : ℤ) ↦ J(a | n)) 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]

Premises used: List.map, jacobiSym.mul_left, jacobiSym.one_left, List.prod_nil, List.prod_cons, List.map_nil
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
hl : ∀ (n : ℕ), Membership.mem (γ := List ℕ) [] n → n ≠ 0
⊢ J(a | List.prod []) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) [])

Tactic:
simp only [List.prod_nil, one_right, List.map_nil]

Premises used: jacobiSym.one_right, List.prod_nil, List.map_nil
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
⊢ n ≠ 0

Tactic:
have hn := hl n List.mem_cons_self
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
⊢ l'.prod ≠ 0

Tactic:
have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
⊢ ∀ (m : ℕ) (hm : m ∈ l'), m ≠ 0

Tactic:
have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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')
cons₄ 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')
⊢ J(a | (n :: l').prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) (n :: l'))

Tactic:
rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]

Premises used: List.map, jacobiSym.mul_right', List.prod_cons
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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)) [])
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'))
⊢ J(a | l.prod) = List.prod (List.map (fun (n : ℕ) ↦ J(a | 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]

Premises used: List.map, jacobiSym.one_right, List.prod_nil, List.prod_cons, List.map_nil
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
h : J(a | 0) = -1
⊢ Eq (α := ℤ) 1 0

Tactic:
rw [zero_right, CharZero.eq_neg_self_iff] at h

Premises used: CharZero.eq_neg_self_iff, jacobiSym.zero_right
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
h : Eq (α := ℤ) 1 0
⊢ False

Tactic:
one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
h : Eq (α := ℤ) 1 0
⊢ False

Tactic:
exact one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ 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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
⊢ 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

Premises used: jacobiSym.list_prod_right, Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
h₁ : Eq (α := ℤ) (List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) n.primeFactorsList)) (-1)
⊢ n ≠ 0

Tactic:
rw [← Nat.prod_primeFactorsList hn₀, list_prod_right hf₀] at h

Premises used: jacobiSym.list_prod_right, Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
n : ℕ
h : J(a | n) = -1
hn₀ : n ≠ 0
hf₀ : ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0
h₁ : Eq (α := ℤ) (List.prod (List.map (fun (n : ℕ) ↦ J(a | n)) n.primeFactorsList)) (-1)
hn₁ : n ≠ 0
⊢ ∀ (p : ℕ) (hp : p ∈ n.primeFactorsList), p ≠ 0

Tactic:
rw [← Nat.prod_primeFactorsList hn₀, list_prod_right hf₀] at h

Premises used: jacobiSym.list_prod_right, Nat.prod_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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
obtain : ∀ (p : ℕ) (hmem : p ∈ n.primeFactorsList) (hj : J(a | p) = -1), ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ 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)

Premises used: List.neg_one_mem_of_prod_eq_neg_one, Iff.mp, List.mem_map
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : ℕ
hmem : p ∈ n.primeFactorsList
hj : J(a | p) = -1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
⟨p, Nat.prime_of_mem_primeFactorsList hmem, Nat.dvd_of_mem_primeFactorsList hmem, hj⟩

Premises used: Nat.prime_of_mem_primeFactorsList, And.intro, Exists.intro, Nat.dvd_of_mem_primeFactorsList
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
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 : ℕ
hmem : p ∈ n.primeFactorsList
hj : J(a | p) = -1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
exact ⟨p, Nat.prime_of_mem_primeFactorsList hmem, Nat.dvd_of_mem_primeFactorsList hmem, hj⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : (↑a : ZMod b) = r * r
⊢ a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)

Tactic:
rw [← r.coe_valMinAbs, ← Int.cast_mul, intCast_eq_intCast_iff', ← sq] at ha

Premises used: ZMod.coe_valMinAbs, sq, ZMod.intCast_eq_intCast_iff', Int.cast_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)
⊢ ¬LE.le (α := ℤ) 0 (-1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Goal:
a : ℤ
b : ℕ
h : J(a | b) = -1
h_1 : IsSquare (α := ZMod b) (↑a : ZMod b)
r : ZMod b
ha : a % (↑b : ℤ) = HPow.hPow (β := ℕ) r.valMinAbs 2 % (↑b : ℤ)
apply : LE.le (α := ℤ) 0 (-1)
⊢ False

Tactic:
apply (by simp : ¬(0 : ℤ) ≤ -1)