awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
inl : ∀ (hc : ringChar (ZMod p) = 2), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
inr : ∀ (hc : ringChar (ZMod p) ≠ 2), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)

Tactic:
rcases eq_or_ne (ringChar (ZMod p)) 2 with hc | hc

Premises used: ZMod, ringChar, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
pos :
  ∀ (ha : Eq (α := ZMod p) (↑a : ZMod p) 0),
    (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
neg :
  ∀ (ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0),
    (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)

Tactic:
by_cases ha : (a : ZMod p) = 0

Premises used: Int.cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : Eq (α := ZMod p) (↑a : ZMod p) 0
pos : Eq (α := ZMod p) (↑0 : ZMod p) 0
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)

Tactic:
rw [legendreSym, ha, quadraticChar_zero,
        zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne']

Premises used: quadraticChar_zero, legendreSym, LT.lt.ne', Nat.succ_pos, Nat.Prime.two_le, OfNat.ofNat, Nat.div_pos, zero_pow, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : Eq (α := ZMod p) (↑a : ZMod p) 0
pos pos₁ pos₂ pos₃ : Eq (α := ZMod p) 0 0
⊢ Eq (α := ZMod p) (↑0 : ZMod p) 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ p = 2

Tactic:
have := (ringChar_zmod_n p).symm.trans hc
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0
this : p = 2
neg :
  ∀ [inst : Fact (Nat.Prime 2)] (hc : ringChar (ZMod 2) = 2) (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0),
    (↑(legendreSym 2 a) : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)

Tactic:
subst p
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0
neg : (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
⊢ (↑(legendreSym 2 a) : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)

Tactic:
rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]

Premises used: legendreSym, quadraticChar_eq_one_of_char_two
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0
neg : ∀ (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0), (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
⊢ (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)

Tactic:
revert ha
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
neg : ∀ (b : ZMod 2) (ha : ¬b = 0), 1 = HPow.hPow (β := ℕ) b 1
⊢ ∀ (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0), 1 = HPow.hPow (α := ZMod 2) (β := ℕ) (↑a : ZMod 2) 1

Tactic:
generalize (a : ZMod 2) = b

Premises used: Int.cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
neg :
  ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) 0),
    1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) 1
neg₁ :
  ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) 0),
    1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) 1
⊢ ∀ (ha : ¬b = 0), 1 = HPow.hPow (β := ℕ) b 1

Tactic:
fin_cases b
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
neg :
  ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) 0 →
    1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) 1
⊢ ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) 0),
    1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) 1

Tactic:
tauto
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) 0),
    1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ (↑((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑a : ZMod p)) : ZMod p) =
    HPow.hPow (α := ZMod p) (↑a : ZMod p) (Fintype.card (ZMod p) / 2)

Tactic:
quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)

Premises used: Int.cast, quadraticChar_eq_pow_of_char_ne_two'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
h : p = Fintype.card (ZMod p)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)

Tactic:
convert! quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)

Premises used: Int.cast, quadraticChar_eq_pow_of_char_ne_two'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)

Tactic:
(card p).symm

Premises used: Eq.symm, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)

Tactic:
exact (card p).symm

Premises used: Eq.symm, ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ legendreSym p a = 1 ∨ legendreSym p a = -1

Tactic:
quadraticChar_dichotomy ha

Premises used: quadraticChar_dichotomy, legendreSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ legendreSym p a = -1 ↔ ¬legendreSym p a = 1

Tactic:
quadraticChar_eq_neg_one_iff_not_one ha

Premises used: legendreSym, quadraticChar_eq_neg_one_iff_not_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = 0 ↔ Eq (α := ZMod p) (↑a : ZMod p) 0

Tactic:
quadraticChar_eq_zero_iff

Premises used: quadraticChar_eq_zero_iff, legendreSym
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑0 : ZMod p) : ℤ) (0 : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 0 : ℤ) (0 : ℤ)
rw₂ rw₃ : Eq (α := ℤ) 0 0
⊢ legendreSym p 0 = 0

Tactic:
rw [legendreSym, Int.cast_zero, MulChar.map_zero]

Premises used: Int.cast_zero, legendreSym, MulChar.map_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑1 : ZMod p) : ℤ) (1 : ℤ)
rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 1 : ℤ) (1 : ℤ)
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ legendreSym p 1 = 1

Tactic:
rw [legendreSym, Int.cast_one, MulChar.map_one]

Premises used: MulChar.map_one, legendreSym, Int.cast_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a b : ℤ
⊢ legendreSym p (a * b) = legendreSym p a * legendreSym p b

Tactic:
simp [legendreSym, Int.cast_mul, map_mul]

Premises used: legendreSym, map_mul, Int.cast_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ HPow.hPow (β := ℕ) (legendreSym p a) 2 = 1

Tactic:
quadraticChar_sq_one ha

Premises used: legendreSym, quadraticChar_sq_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
rw :
  Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (HPow.hPow (α := ZMod p) (β := ℕ) (↑a : ZMod p) 2) : ℤ)
    (1 : ℤ)
⊢ Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑(HPow.hPow (β := ℕ) a 2) : ZMod p) : ℤ) (1 : ℤ)

Tactic:
rw [Int.cast_pow]

Premises used: Int.cast_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (HPow.hPow (α := ZMod p) (β := ℕ) (↑a : ZMod p) 2) : ℤ)
    (1 : ℤ)

Tactic:
quadraticChar_sq_one' ha

Premises used: quadraticChar_sq_one'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (HPow.hPow (α := ZMod p) (β := ℕ) (↑a : ZMod p) 2) : ℤ)
    (1 : ℤ)

Tactic:
exact quadraticChar_sq_one' ha

Premises used: quadraticChar_sq_one'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = legendreSym p (a % (↑p : ℤ))

Tactic:
simp only [legendreSym, intCast_mod]

Premises used: legendreSym, ZMod.intCast_mod
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ legendreSym p a = 1 ↔ IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
quadraticChar_one_iff_isSquare ha0

Premises used: legendreSym, quadraticChar_one_iff_isSquare
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
rw : IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
ha0₁ : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
⊢ legendreSym p (↑a : ℤ) = 1 ↔ IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
rw [eq_one_iff]

Premises used: legendreSym.eq_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : IsSquare (α := ZMod p) (↑a : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
⊢ IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0

Tactic:
mod_cast ha0

Premises used: Int.cast, Int.cast_natCast, congrArg, Int.cast_zero, cast, Ne, Nat.cast, congr, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0

Tactic:
exact mod_cast ha0
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
quadraticChar_neg_one_iff_not_isSquare

Premises used: legendreSym, quadraticChar_neg_one_iff_not_isSquare
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
rw : ¬IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
⊢ legendreSym p (↑a : ℤ) = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
rw [eq_neg_one_iff]

Premises used: legendreSym.eq_neg_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ¬IsSquare (α := ZMod p) (↑a : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
⊢ ¬IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
⊢ (↑(Finset.card (α := ZMod p) (Set.toFinset {x : ZMod p | HPow.hPow (β := ℕ) x 2 = (↑a : ZMod p)})) : ℤ) =
    legendreSym p a + 1

Tactic:
quadraticChar_card_sqrts ((ringChar_zmod_n p).substr hp) a

Premises used: quadraticChar_card_sqrts, Int.cast, legendreSym, Eq.substr, ZMod.ringChar_zmod_n
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
⊢ (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 =
    0 * HPow.hPow (β := ℕ) y⁻¹ 2

Tactic:
apply_fun (· * y⁻¹ ^ 2) at hxy

Premises used: HMul.hMul, Inv.inv, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy :
  (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 =
    0 * HPow.hPow (β := ℕ) y⁻¹ 2
⊢ (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 = 0

Tactic:
simp only [zero_mul] at hxy

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy : (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 = 0
⊢ (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 =
    HPow.hPow (β := ℕ) (x * y⁻¹) 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) (y * y⁻¹) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy : (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 = 0
⊢ x * y⁻¹ * (x * y⁻¹) = (↑a : ZMod p)

Tactic:
rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2),
    mul_inv_cancel₀ hy, one_pow, mul_one, sub_eq_zero, pow_two] at hxy

Premises used: one_pow, pow_two, mul_inv_cancel₀, sub_eq_zero, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = (↑a : ZMod p)
⊢ legendreSym p a = 1

Tactic:
(eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩

Premises used: Iff.mpr, HMul.hMul, legendreSym.eq_one_iff, Inv.inv, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = (↑a : ZMod p)
⊢ legendreSym p a = 1

Tactic:
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩

Premises used: Iff.mpr, HMul.hMul, legendreSym.eq_one_iff, Inv.inv, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ZMod p
hx : x ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (α := ZMod p) (β := ℕ) 0 2 = 0
⊢ x = 0

Tactic:
rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy

Premises used: sub_zero, MulZeroClass.mul_zero, two_ne_zero, zero_pow, sq_eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False

Tactic:
hx hxy
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x : ZMod p
hx : x ≠ 0
hxy : x = 0
⊢ False

Tactic:
exact hx hxy
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hx : x ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
⊢ y ≠ 0

Tactic:
haveI hy : y ≠ 0 := by
    rintro rfl
    rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy
    exact hx hxy
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hx : x ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1

Tactic:
eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy

Premises used: legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
x y : ZMod p
hx : x ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
hy : y ≠ 0
⊢ legendreSym p a = 1

Tactic:
exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy

Premises used: legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
hf : Eq (α := ZMod p) (↑a : ZMod p) 0
rw :
  ∀ (h : Eq (α := ℤ) 0 (-1)) {x y : ZMod p} (hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0)
    (hf : Eq (α := ZMod p) (↑a : ZMod p) 0), False
⊢ False

Tactic:
rw [(eq_zero_iff p a).mpr hf] at h

Premises used: Iff.mpr, legendreSym.eq_zero_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : Eq (α := ℤ) 0 (-1)
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
hf : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
⊢ Ne (α := ZMod p) (↑a : ZMod p) 0

Tactic:
have ha : (a : ZMod p) ≠ 0 := by
    intro hf
    rw [(eq_zero_iff p a).mpr hf] at h
    simp at h
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
by_contra : ∀ (hf : ¬(x = 0 ∧ y = 0)), False
⊢ x = 0 ∧ y = 0

Tactic:
by_contra hf
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
inl : ∀ (hx : ¬x = 0), False
inr : ∀ (hy : ¬y = 0), False
⊢ False

Tactic:
rcases imp_iff_or_not.mp (not_and'.mp hf) with hx | hy

Premises used: Iff.mp, not_and', imp_iff_or_not
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
inl :
  ∀ (h : Eq (α := ℤ) 1 0) {x y : ZMod p} (hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0)
    (ha : Ne (α := ZMod p) (↑a : ZMod p) 0) (hf : ¬(x = 0 ∧ y = 0)) (hx : ¬x = 0), False
⊢ False

Tactic:
rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, CharZero.eq_neg_self_iff] at h

Premises used: CharZero.eq_neg_self_iff, legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero'
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : Eq (α := ℤ) 1 0
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False

Tactic:
one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : Eq (α := ℤ) 1 0
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hx : ¬x = 0
⊢ False

Tactic:
exact one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
inr :
  ∀ (h : Eq (α := ℤ) 1 0) {x y : ZMod p} (hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0)
    (ha : Ne (α := ZMod p) (↑a : ZMod p) 0) (hf : ¬(x = 0 ∧ y = 0)) (hy : ¬y = 0), False
⊢ False

Tactic:
rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, CharZero.eq_neg_self_iff] at h

Premises used: CharZero.eq_neg_self_iff, legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : Eq (α := ℤ) 1 0
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False

Tactic:
one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : Eq (α := ℤ) 1 0
x y : ZMod p
hxy : HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2 = 0
ha : Ne (α := ZMod p) (↑a : ZMod p) 0
hf : ¬(x = 0 ∧ y = 0)
hy : ¬y = 0
⊢ False

Tactic:
exact one_ne_zero h

Premises used: one_ne_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
simp_rw :
  ∀ (hxy : Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2) : ZMod p) 0),
    Eq (α := ZMod p) (↑x : ZMod p) 0 ∧ Eq (α := ZMod p) (↑y : ZMod p) 0
⊢ (↑p : ℤ) ∣ x ∧ (↑p : ℤ) ∣ y

Tactic:
simp_rw [← ZMod.intCast_zmod_eq_zero_iff_dvd] at hxy ⊢

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) x 2 - a * HPow.hPow (β := ℕ) y 2) : ZMod p) 0
⊢ HPow.hPow (α := ZMod p) (β := ℕ) (↑x : ZMod p) 2 - (↑a : ZMod p) * HPow.hPow (α := ZMod p) (β := ℕ) (↑y : ZMod p) 2 =
    0

Tactic:
push_cast at hxy
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑x : ZMod p) 2 - (↑a : ZMod p) * HPow.hPow (α := ZMod p) (β := ℕ) (↑y : ZMod p) 2 =
    0
⊢ Eq (α := ZMod p) (↑x : ZMod p) 0 ∧ Eq (α := ZMod p) (↑y : ZMod p) 0

Tactic:
eq_zero_mod_of_eq_neg_one h hxy

Premises used: legendreSym.eq_zero_mod_of_eq_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑x : ZMod p) 2 - (↑a : ZMod p) * HPow.hPow (α := ZMod p) (β := ℕ) (↑y : ZMod p) 2 =
    0
⊢ Eq (α := ZMod p) (↑x : ZMod p) 0 ∧ Eq (α := ZMod p) (↑y : ZMod p) 0

Tactic:
exact eq_zero_mod_of_eq_neg_one h hxy

Premises used: legendreSym.eq_zero_mod_of_eq_neg_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-1) = (χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4)

Tactic:
simp only [legendreSym, card p, quadraticChar_neg_one ((ringChar_zmod_n p).substr hp),
    Int.cast_neg, Int.cast_one]

Premises used: Int.cast_neg, legendreSym, Eq.substr, ZMod.ringChar_zmod_n, quadraticChar_neg_one, Int.cast_one, ZMod.card