awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ ∀ (ha : ¬b = 0), 1 = HPow.hPow (β := ℕ) b 1
have neg₁ : ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, sorry⟩) 0),
  1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, sorry⟩ : Fin (1 + 1))) 1
Tactic: fin_cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have h : p = Fintype.card (ZMod p)
Tactic: convert! quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ legendreSym p 0 = 0
have rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑0 : ZMod p) : ℤ) (0 : ℤ)
Tactic: rw [legendreSym, Int.cast_zero, MulChar.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑0 : ZMod p) : ℤ) (0 : ℤ)
⊢ legendreSym p 0 = 0
have rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 0 : ℤ) (0 : ℤ)
Tactic: rw [legendreSym, Int.cast_zero, MulChar.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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 : ℤ)
⊢ legendreSym p 0 = 0
have rw₂ : Eq (α := ℤ) 0 0
Tactic: rw [legendreSym, Int.cast_zero, MulChar.map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ legendreSym p 1 = 1
have rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑1 : ZMod p) : ℤ) (1 : ℤ)
Tactic: rw [legendreSym, Int.cast_one, MulChar.map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (↑1 : ZMod p) : ℤ) (1 : ℤ)
⊢ legendreSym p 1 = 1
have rw₁ : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) 1 : ℤ) (1 : ℤ)
Tactic: rw [legendreSym, Int.cast_one, MulChar.map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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 : ℤ)
⊢ legendreSym p 1 = 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [legendreSym, Int.cast_one, MulChar.map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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 (β := ℕ) a 2) : ZMod p) : ℤ) (1 : ℤ)
have rw : Eq (α := ℤ) ((quadraticChar (ZMod p) : (a : ZMod p) → ℤ) (HPow.hPow (α := ZMod p) (β := ℕ) (↑a : ZMod p) 2) : ℤ) (1 : ℤ)
Tactic: rw [Int.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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)
have rw : IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
Tactic: rw [eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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)
⊢ legendreSym p (↑a : ℤ) = 1 ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
have ha0₁ : Ne (α := ZMod p) (↑(↑a : ℤ) : ZMod p) 0
Tactic: rw [eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
ha0 : Ne (α := ZMod p) (↑a : ZMod p) 0
⊢ IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
have norm_cast : IsSquare (α := ZMod p) (↑a : ZMod p) ↔ IsSquare (α := ZMod p) (↑a : ZMod p)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
⊢ legendreSym p (↑a : ℤ) = -1 ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
have rw : ¬IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
Tactic: rw [eq_neg_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
⊢ ¬IsSquare (α := ZMod p) (↑(↑a : ℤ) : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
have norm_cast : ¬IsSquare (α := ZMod p) (↑a : ZMod p) ↔ ¬IsSquare (α := ZMod p) (↑a : ZMod p)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ legendreSym p a = 1
have hxy₁ : (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
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ legendreSym p a = 1
have hxy₁ : (HPow.hPow (β := ℕ) x 2 - (↑a : ZMod p) * HPow.hPow (β := ℕ) y 2) * HPow.hPow (β := ℕ) y⁻¹ 2 = 0
Tactic: simp only [zero_mul] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ legendreSym p a = 1
have hxy₁ : 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
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ False
have hxy₁ : x = 0
Tactic: rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ legendreSym p a = 1
have hy : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ False
have 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
Tactic: rw [(eq_zero_iff p a).mpr hf] at h
Cleared hypotheses: h, x, y, hxy, hf
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ x = 0 ∧ y = 0
have ha : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ x = 0 ∧ y = 0
have by_contra : ∀ (hf : ¬(x = 0 ∧ y = 0)), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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)
⊢ False
have inl : ∀ (hx : ¬x = 0), False
Tactic: rcases imp_iff_or_not.mp (not_and'.mp hf) with hx | hy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ False
have inr : ∀ (hy : ¬y = 0), False
Tactic: rcases imp_iff_or_not.mp (not_and'.mp hf) with hx | hy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ False
have 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
Tactic: rw [eq_one_of_sq_sub_mul_sq_eq_zero' ha hx hxy, CharZero.eq_neg_self_iff] at h
Cleared hypotheses: h, x, y, hxy, ha, hf, hx
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
⊢ False
have 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
Tactic: rw [eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy, CharZero.eq_neg_self_iff] at h
Cleared hypotheses: h, x, y, hxy, ha, hf, hy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
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
have 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
Tactic: simp_rw [← ZMod.intCast_zmod_eq_zero_iff_dvd] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
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
⊢ Eq (α := ZMod p) (↑x : ZMod p) 0 ∧ Eq (α := ZMod p) (↑y : ZMod p) 0
have hxy₁ : 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
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
⊢ legendreSym p (-a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
have rw : legendreSym p (-1 * a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
Tactic: rw [neg_eq_neg_one_mul, legendreSym.mul p (-1) a, legendreSym.at_neg_one hp]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
rw : legendreSym p (-1 * a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
⊢ legendreSym p (-a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
have rw₁ : legendreSym p (-1) * legendreSym p a = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
Tactic: rw [neg_eq_neg_one_mul, legendreSym.mul p (-1) a, legendreSym.at_neg_one hp]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
rw : legendreSym p (-1 * a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
rw₁ :
  legendreSym p (-1) * legendreSym p a =
    HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
⊢ legendreSym p (-a) = HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
have rw₂ : HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a) =
  HMul.hMul (α := ℤ) ((χ₄ : (a : ZMod 4) → ℤ) (↑p : ZMod 4) : ℤ) (legendreSym p a)
Tactic: rw [neg_eq_neg_one_mul, legendreSym.mul p (-1) a, legendreSym.at_neg_one hp]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ IsSquare (α := ZMod p) (-1) ↔ p % 4 ≠ 3
have rw : Fintype.card (ZMod p) % 4 ≠ 3 ↔ p % 4 ≠ 3
Tactic: rw [FiniteField.isSquare_neg_one_iff, card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Fintype.card (ZMod p) % 4 ≠ 3 ↔ p % 4 ≠ 3
⊢ IsSquare (α := ZMod p) (-1) ↔ p % 4 ≠ 3
have rw₁ : p % 4 ≠ 3 ↔ p % 4 ≠ 3
Tactic: rw [FiniteField.isSquare_neg_one_iff, card p]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 = -HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have hxy₁ : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
Tactic: apply_fun fun z => z / y ^ 2 at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have rwa : ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
  HPow.hPow (β := ℕ) (x / y) 2 = -1
Tactic: rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
rwa :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have rwa₁ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
  HPow.hPow (β := ℕ) (x / y) 2 = -1
Tactic: rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
rwa :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₁ :
  ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have rwa₂ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (β := ℕ) (y / y) 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
Tactic: rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
rwa :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₁ :
  ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₂ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (β := ℕ) (y / y) 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have rwa₃ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
Tactic: rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2
rwa :
  ∀ (hxy : HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) y 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₁ :
  ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -(HPow.hPow (β := ℕ) y 2 / HPow.hPow (β := ℕ) y 2)),
    HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₂ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (β := ℕ) (y / y) 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
rwa₃ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2), HPow.hPow (β := ℕ) (x / y) 2 = -1
⊢ HPow.hPow (β := ℕ) (x / y) 2 = -1
have rwa₄ : ∀ (hxy : HPow.hPow (β := ℕ) (x / y) 2 = -1), HPow.hPow (β := ℕ) (x / y) 2 = -1
Tactic: rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Complex (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
ch : PrimitiveAddChar F ℂ := primitiveChar F ℂ ⋯
⊢ AddChar F ℂ
have refine : CyclotomicField (↑ch.n : ℕ) ℂ →* ℂ
Tactic: refine MonoidHom.compAddChar ?_ ch.char
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Complex (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Finite F
⊢ IsPrimitive (primitiveChar_to_Complex F)
have refine : Function.Injective (α := CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ sorry)) : ℕ) ℂ) (β := ℂ)
  (⇑(MulEquiv.toMonoidHom
        (AlgEquiv.toMulEquiv
          (IsCyclotomicExtension.algEquiv {(↑(PrimitiveAddChar.n (primitiveChar F ℂ sorry)) : ℕ)} ℂ
            (CyclotomicField (↑(PrimitiveAddChar.n (primitiveChar F ℂ sorry)) : ℕ) ℂ) ℂ))) :
    (a : CyclotomicField (↑(primitiveChar F ℂ sorry).n : ℕ) ℂ) → ℂ)
Tactic: refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ (a * (↑x : ZMod p)).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val)
    (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)
have he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
Tactic: have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ (a * (↑x : ZMod p)).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val)
    (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)
have hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
Tactic: have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
    lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ (a * (↑x : ZMod p)).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val)
    (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)
have hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
Tactic: have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x := fun hx hpx =>
    not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero (he hx).1) hpx) (hep hx)
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
⊢ Eq (α := Multiset ℕ) (Multiset.map (fun (x : ℕ) ↦ (a * (↑x : ZMod p)).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val)
    (Multiset.map (fun (a : ℕ) ↦ a) (Ico 1 (p / 2).succ).val)
have hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
Tactic: have hmem : ∀ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ),
      (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ := by
    intro x hx
    simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
have refine_1 : 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs
Tactic: refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
refine_1 : 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs
⊢ ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
have refine_2 : ((↑b : ZMod p) / a).valMinAbs.natAbs < (p / 2).succ
Tactic: refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * (↑x : ZMod p)).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
refine_1 : 1 ≤ ((↑b : ZMod p) / a).valMinAbs.natAbs
refine_2 : ((↑b : ZMod p) / a).valMinAbs.natAbs < (p / 2).succ
⊢ ∃ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ), (a * (↑x : ZMod p)).valMinAbs.natAbs = b
have refine_3 : (a * (↑((↑b : ZMod p) / a).valMinAbs.natAbs : ZMod p)).valMinAbs.natAbs = b
Tactic: refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩