-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem eq_pow (a : ℤ) : (legendreSym p a : ZMod p) = (a : ZMod p) ^ (p / 2)

Proof state:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)

Tactic:
revert ha

Result:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → ↑1 = ↑a ^ (2 / 2)

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
have := (ringChar_zmod_n p).symm.trans hc

Result:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
this : p = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Proof state:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

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

Result:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Proof state:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
⊢ ¬b = 0 → 1 = b ^ 1

Tactic:
fin_cases b

Result:
case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic._hyg.680.«0»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i => i) ⟨0, ⋯⟩ = 0 → 1 = (fun i => i) ⟨0, ⋯⟩ ^ 1

case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic._hyg.680.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i => i) ⟨1, ⋯⟩ = 0 → 1 = (fun i => i) ⟨1, ⋯⟩ ^ 1

Proof state:
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)

Tactic:
exact (card p).symm

Result:
no goals

Proof state:
case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic._hyg.680.«0»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i => i) ⟨0, ⋯⟩ = 0 → 1 = (fun i => i) ⟨0, ⋯⟩ ^ 1

Tactic:
tauto

Result:
no goals

Proof state:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → 1 = ↑a ^ 1

Tactic:
generalize (a : ZMod 2) = b

Result:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
⊢ ¬b = 0 → 1 = b ^ 1

Proof state:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → ↑1 = ↑a ^ (2 / 2)

Tactic:
push_cast

Result:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬↑a = 0 → 1 = ↑a ^ 1

Proof state:
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

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

Result:
case h.e'_3.h.e'_6.h.e'_5
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ p = Fintype.card (ZMod p)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

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

Result:
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Proof state:
case neg.«_@».Mathlib.NumberTheory.LegendreSymbol.Basic._hyg.680.«1»
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ¬(fun i => i) ⟨1, ⋯⟩ = 0 → 1 = (fun i => i) ⟨1, ⋯⟩ ^ 1

Tactic:
simp

Result:
no goals

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0

Tactic:
norm_cast

Result:
no goals

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬↑a = 0
this : p = 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
subst p

Result:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym 2 a) = ↑a ^ (2 / 2)

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

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

Result:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ↑a = 0
⊢ ↑0 = 0

Proof state:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑(legendreSym 2 a) = ↑a ^ (2 / 2)

Tactic:
rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]

Result:
case neg
a : ℤ
inst✝ : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬↑a = 0
⊢ ↑1 = ↑a ^ (2 / 2)