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

Proof state:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
haveI : Fact p.Prime := ⟨hpp⟩

Result:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ IsSquare (-1)

Proof state:
case h₀
hn : Squarefree 0
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 0 → q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
exact False.elim (hn.ne_zero rfl)

Result:
no goals

Proof state:
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hc : ¬p.Coprime n
⊢ False

Tactic:
exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)

Result:
no goals

Proof state:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : p.Coprime n
hp₁ : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
exact ZMod.isSquare_neg_one_mul hcp hp₁
  (ih hn.of_mul_right fun hqp hqd => H hqp <| dvd_mul_of_dvd_right hqd _)

Result:
no goals

Proof state:
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ p.Coprime n

Tactic:
by_contra hc

Result:
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hc : ¬p.Coprime n
⊢ False

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

Tactic:
refine ⟨fun H q hqp hqd => hqp.mod_four_ne_three_of_dvd_isSquare_neg_one hqd H, fun H => ?_⟩

Result:
n : ℕ
hn : Squarefree n
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ IsSquare (-1)

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

Tactic:
induction n using induction_on_primes with
| h₀ => exact False.elim (hn.ne_zero rfl)
| h₁ => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
| h p n hpp ih =>
  haveI : Fact p.Prime := ⟨hpp⟩
  have hcp : p.Coprime n := by
    by_contra hc
    exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
  have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))
  exact ZMod.isSquare_neg_one_mul hcp hp₁
    (ih hn.of_mul_right fun hqp hqd => H hqp <| dvd_mul_of_dvd_right hqd _)

Result:
no goals

Proof state:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : p.Coprime n
⊢ IsSquare (-1)

Tactic:
have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))

Result:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : p.Coprime n
hp₁ : IsSquare (-1)
⊢ IsSquare (-1)

Proof state:
case h₁
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩

Result:
no goals

Proof state:
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ -1 = 0 * 0

Tactic:
simp only [mul_zero, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ IsSquare (-1)

Tactic:
have hcp : p.Coprime n := by
  by_contra hc
  exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)

Result:
case h
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : p.Coprime n
⊢ IsSquare (-1)