-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
theorem FiniteField.isSquare_odd_prime_iff (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime]
    (hp : p ≠ 2) :
    IsSquare (p : F) ↔ quadraticChar (ZMod p) (χ₄ (Fintype.card F) * Fintype.card F) ≠ -1

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Tactic:
rw [← Iff.not_left (@quadraticChar_neg_one_iff_not_isSquare F _ _ _ _),
  quadraticChar_odd_prime hF hp]

Result:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ ringChar F ≠ p

Proof state:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * 0 ^ ↑n = -1

Tactic:
simp only [zero_pow n.ne_zero, mul_zero, zero_eq_neg, one_ne_zero, not_false_iff]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ↑p = 0

Tactic:
rw [← hFp]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ↑(ringChar F) = 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ ringChar F = ringChar (ZMod p)

Tactic:
rw [hFp]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ p = ringChar (ZMod p)

Proof state:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1

Tactic:
conv => enter [1, 1, 2]; rw [hc, Nat.cast_pow, map_pow, hchar, map_ringChar]

Result:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * 0 ^ ↑n = -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Tactic:
by_cases hFp : ringChar F = p

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Proof state:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1

Tactic:
have hchar : ringChar F = ringChar (ZMod p) := by rw [hFp]; exact (ringChar_zmod_n p).symm

Result:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
hchar : ringChar F = ringChar (ZMod p)
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ¬ringChar F = p
⊢ ringChar F ≠ p

Tactic:
exact hFp

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare ↑p ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Tactic:
rw [show (p : F) = 0 by rw [← hFp]; exact ringChar.Nat.cast_ringChar]

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare 0 ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1

Tactic:
obtain ⟨n, _, hc⟩ := FiniteField.card F (ringChar F)

Result:
case pos.intro.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
n : ℕ+
left✝ : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
⊢ p = ringChar (ZMod p)

Tactic:
exact (ringChar_zmod_n p).symm

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ↑(ringChar F) = 0

Tactic:
exact ringChar.Nat.cast_ringChar

Result:
no goals

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ IsSquare 0 ↔ (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F)) ≠ -1

Tactic:
simp only [IsSquare.zero, Ne, true_iff, map_mul]

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
hFp : ringChar F = p
⊢ ¬(quadraticChar (ZMod p)) ↑(χ₄ ↑(Fintype.card F)) * (quadraticChar (ZMod p)) ↑(Fintype.card F) = -1