-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem ZMod.isSquare_neg_one_iff' {n : ℕ} (hn : Squarefree n) :
    IsSquare (-1 : ZMod n) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
rw [ZMod.isSquare_neg_one_iff hn]

Result:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
hp : p % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Tactic:
replace hq := hq (dvd_of_mul_left_dvd hpq)

Result:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3

Tactic:
replace hp := H hp (dvd_of_mul_right_dvd hpq)

Result:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
hp : p % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Proof state:
n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide

Result:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
intro H

Result:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3

Tactic:
rw [Nat.cast_mul]

Result:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑p * ↑q = ↑3

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3 % 4
⊢ 3 = 3 % 4

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 1 ∣ n
⊢ 1 % 4 ≠ 3

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3

Tactic:
rw [show 3 = 3 % 4 by norm_num, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢

Result:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)

Result:
case refine_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3

case refine_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3

case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3

Proof state:
n : ℕ
hn : Squarefree n
⊢ ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3

Tactic:
decide

Result:
no goals

Proof state:
case refine_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3

Tactic:
exact fun _ => by norm_num

Result:
no goals

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑p * ↑q = ↑3

Tactic:
exact help p q hp hq

Result:
no goals

Proof state:
case refine_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3

Tactic:
exact fun _ => by norm_num

Result:
no goals

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
refine ⟨?_, fun H q _ => H⟩

Result:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Proof state:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 0 ∣ n
⊢ 0 % 4 ≠ 3

Tactic:
norm_num

Result:
no goals