awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
hc2 : IsCoprime (HPow.hPow (β := ℕ) x 2) (n + -1 * HPow.hPow (β := ℕ) x 2)
⊢ IsCoprime x n

Tactic:
(IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Premises used: IsCoprime.pow_left_iff, Iff.mp, IsCoprime.of_add_mul_right_right, zero_lt_two
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
hc2 : IsCoprime (HPow.hPow (β := ℕ) x 2) (n + -1 * HPow.hPow (β := ℕ) x 2)
⊢ IsCoprime x n

Tactic:
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Premises used: IsCoprime.pow_left_iff, Iff.mp, IsCoprime.of_add_mul_right_right, zero_lt_two
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
obtain : ∀ (u v : ℤ) (huv : u * x + v * n = 1), IsSquare (α := ZMod n.natAbs) (-1)
⊢ IsSquare (α := ZMod n.natAbs) (-1)

Tactic:
obtain ⟨u, v, huv⟩ : IsCoprime x n := by
    have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
    rw [show y ^ 2 = n + -1 * x ^ 2 by lia] at hc2
    exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Premises used: IsCoprime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)

Tactic:
linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv

Premises used: HMul.hMul, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)

Tactic:
have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
    linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ IsSquare (α := ZMod n.natAbs) (-1)

Tactic:
⟨u * y, ?_⟩

Premises used: Int.cast, HMul.hMul, IsSquare, Exists.intro
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
refine :
  -1 =
    HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
      HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs)
⊢ IsSquare (α := ZMod n.natAbs) (-1)

Tactic:
refine ⟨u * y, ?_⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)
⊢ HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
      HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) =
    (↑(u * y * (u * y)) : ZMod n.natAbs)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
conv_rhs : Eq (α := ZMod n.natAbs) (-1) (↑(u * y * (u * y)) : ZMod n.natAbs)
⊢ -1 =
    HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
      HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs)

Tactic:
conv_rhs => tactic => norm_cast
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ZMod n.natAbs) (↑(Int.negSucc 0) : ZMod n.natAbs) (↑(Int.negSucc 0) : ZMod n.natAbs)
⊢ Eq (α := ZMod n.natAbs) (-1) (↑(-1) : ZMod n.natAbs)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
rw : Eq (α := ZMod n.natAbs) (↑(-1) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)
⊢ Eq (α := ZMod n.natAbs) (-1) (↑(u * y * (u * y)) : ZMod n.natAbs)

Tactic:
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ Eq (α := ZMod n.natAbs) (↑(-1) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)

Tactic:
(ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, Iff.mpr, Exists.intro, Int.natAbs_dvd
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ Eq (α := ZMod n.natAbs) (↑(-1) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)

Tactic:
exact (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)

Premises used: ZMod.intCast_eq_intCast_iff_dvd_sub, Iff.mpr, Exists.intro, Int.natAbs_dvd
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : x.Coprime y
⊢ (↑n : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2

Tactic:
zify at h
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
hc : x.Coprime y
h : (↑n : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
⊢ IsSquare (α := ZMod n) (-1)

Tactic:
ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime

Premises used: Int.natAbs, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime, Nat.Coprime.isCoprime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
hc : x.Coprime y
h : (↑n : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
⊢ IsSquare (α := ZMod n) (-1)

Tactic:
exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime

Premises used: ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime, Nat.Coprime.isCoprime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
mp :
  (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) →
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
mpr :
  (∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)) →
    ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
pos : ∀ (hxy : x = 0 ∧ y = 0), ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
neg : ∀ (hxy : ¬(x = 0 ∧ y = 0)), ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
by_cases hxy : x = 0 ∧ y = 0
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₃ : HAdd.hAdd (α := ℕ) 0 0 = HMul.hMul (α := ℕ) 0 1
rw₄ : 0 = HMul.hMul (α := ℕ) 0 1
rw₅ rw₆ : Eq (α := ℕ) 0 0
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1

Tactic:
rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, two_ne_zero, And.right, And.left, add_zero, zero_pow
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : Eq (α := ZMod 1) (-1) 0
rw₁ : Eq (α := ZMod 1) 1 0
rw₂ rw₃ : 0 + 1 = 1
⊢ -1 = HMul.hMul (α := ZMod 1) 0 0

Tactic:
rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]

Premises used: Fin.one_eq_zero_iff, MulZeroClass.zero_mul, neg_eq_zero
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
exact ⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul],
        ⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ 0 < x.gcd y

Tactic:
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
neg :
  ∀ (g x₁ y₁ : ℕ),
    0 < g →
      ∀ (h₂ : x₁.Coprime y₁) (h₃ : x = x₁ * g) (h₄ : y = y₁ * g),
        ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg

Premises used: Nat.exists_coprime'
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
rw :
  HPow.hPow (β := ℕ) (x₁ * g) 2 + HPow.hPow (β := ℕ) (y₁ * g) 2 =
    HPow.hPow (β := ℕ) g 2 * (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) y₁ 2)
⊢ n = HPow.hPow (β := ℕ) g 2 * (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) y₁ 2)

Tactic:
rw [h, h₃, h₄]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ HPow.hPow (β := ℕ) (x₁ * g) 2 + HPow.hPow (β := ℕ) (y₁ * g) 2 =
    HPow.hPow (β := ℕ) g 2 * (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) y₁ 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring,
        ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
mpr :
  ∀ (x' y' : ℕ) (h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2),
    ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂

Premises used: Nat.eq_sq_add_sq_of_isSquare_mod_neg_one
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
x' y' : ℕ
h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2
rw :
  HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2) =
    HPow.hPow (β := ℕ) (a * x') 2 + HPow.hPow (β := ℕ) (a * y') 2
⊢ n = HPow.hPow (β := ℕ) (a * x') 2 + HPow.hPow (β := ℕ) (a * y') 2

Tactic:
rw [h₁, h]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
x' y' : ℕ
h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2
⊢ HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2) =
    HPow.hPow (β := ℕ) (a * x') 2 + HPow.hPow (β := ℕ) (a * y') 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
x' y' : ℕ
h : b = HPow.hPow (β := ℕ) x' 2 + HPow.hPow (β := ℕ) y' 2
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
inl :
  (∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)
inr :
  ∀ (hn₀ : n > 0),
    (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
      ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn₀)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
⊢ (∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)

Tactic:
⟨fun _ q _ _ ↦ (padicValNat_zero_right _).symm ▸ Even.zero, fun _ ↦ ⟨0, 0, rfl⟩⟩

Premises used: Even.zero, Eq.rec, padicValNat_zero_right, Iff.intro, Exists.intro, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
⊢ (∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)

Tactic:
exact ⟨fun _ q _ _ ↦ (padicValNat_zero_right _).symm ▸ Even.zero, fun _ ↦ ⟨0, 0, rfl⟩⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩

Premises used: Nat.eq_sq_add_sq_iff_eq_sq_mul, _private.0.Nat.eq_sq_add_sq_iff.match_1, padicValNat, Even, Iff.intro, Iff.trans
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
inr :
  (∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)) →
    ∀ (q : ℕ) (hq : q ∈ n.primeFactors) (h : q % 4 = 3) (a b : ℕ) (h₁ : n = HPow.hPow (β := ℕ) a 2 * b)
      (h₂ : IsSquare (α := ZMod b) (-1)), Even (padicValNat q n)
inr₁ :
  ∀ (H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)),
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩

Premises used: Nat.eq_sq_add_sq_iff_eq_sq_mul, Iff.intro, Iff.trans
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
⊢ Fact (Prime q)

Tactic:
have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
this : Fact (Prime q)
⊢ q ∣ b → q ∈ b.primeFactors

Tactic:
grind
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
this : Fact (Prime q)
⊢ q ∣ b → q ∈ b.primeFactors

Tactic:
have : q ∣ b → q ∈ b.primeFactors := by grind
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
h_1 : ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
q : ℕ
hq : q ∈ n.primeFactors
h : q % 4 = 3
a b : ℕ
h₁ : n = HPow.hPow (β := ℕ) a 2 * b
h₂ : IsSquare (α := ZMod b) (-1)
this_1 : Fact (Prime q)
this : q ∣ b → q ∈ b.primeFactors
⊢ Even (padicValNat q n)

Tactic:
grind (splits := 10) [padicValNat.mul, padicValNat.pow,
      padicValNat.eq_zero_of_not_dvd, mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one]

Premises used: padicValNat.pow, padicValNat.mul, padicValNat.eq_zero_of_not_dvd, Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
inr :
  ∀ (b a : ℕ) (hb₀ : 0 < b) (ha₀ : 0 < a) (hab : HPow.hPow (β := ℕ) a 2 * b = n) (hb : Squarefree b),
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := sq_mul_squarefree_of_pos hn₀

Premises used: Nat.sq_mul_squarefree_of_pos
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb
      |>.mpr fun q hq hq4 ↦ ?_⟩

Premises used: Iff.mpr, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
inr : ∀ (q : ℕ) (hq : q ∈ b.primeFactors) (hq4 : q % 4 = 3), False
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)

Tactic:
refine ⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb
      |>.mpr fun q hq hq4 ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
⊢ Fact (Prime q)

Tactic:
have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this : Fact (Prime q)
⊢ ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors

Tactic:
have := Nat.primeFactors_mono <| Dvd.intro_left _ hab
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this_1 : Fact (Prime q)
this : ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors
⊢ Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) (1 : ℕ)

Tactic:
grind [Squarefree.natFactorization_le_one,
      Prime.dvd_iff_one_le_factorization, prime_of_mem_primeFactors, dvd_of_mem_primeFactors]

Premises used: Nat.dvd_of_mem_primeFactors, Nat.Prime.dvd_iff_one_le_factorization, Squarefree.natFactorization_le_one, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this_1 : Fact (Prime q)
this : ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors
⊢ Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) (1 : ℕ)

Tactic:
have : b.factorization q = 1 := by grind [Squarefree.natFactorization_le_one,
      Prime.dvd_iff_one_le_factorization, prime_of_mem_primeFactors, dvd_of_mem_primeFactors]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : HPow.hPow (β := ℕ) a 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this_1 : Fact (Prime q)
this_2 : ∀ (hn : n ≠ 0), b.primeFactors ⊆ n.primeFactors
this : Eq (α := ℕ) ((b.factorization : (a : ℕ) → ℕ) q : ℕ) (1 : ℕ)
⊢ False

Tactic:
grind [factorization_def, prime_of_mem_primeFactors, padicValNat.mul, padicValNat.pow]

Premises used: padicValNat.pow, Nat.prime_of_mem_primeFactors, padicValNat.mul, Nat.factorization_def
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x

Tactic:
have h₀ := (hasDerivAt_id' x).smul_const s
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
⊢ HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x

Tactic:
have h₁ := h₀.fun_neg.cexp
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
⊢ HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x

Tactic:
have h₂ := ((sumIDeriv p).hasDerivAt (x • s)).comp x h₀
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
Goal:
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun (y : ℝ) ↦ y • s) (HSMul.hSMul (α := ℝ) 1 s) x
h₁ : HasDerivAt (fun (x : ℝ) ↦ cexp (-(x • s))) (cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s) x
h₂ :
  HasDerivAt ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s)
    (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) * HSMul.hSMul (α := ℝ) 1 s) x
⊢ HasDerivAt
    (fun (i : ℝ) ↦
      -HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (fun (x : ℝ) ↦ cexp (-(x • s)))
          ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s) i)
    (-(cexp (-(x • s)) * -HSMul.hSMul (α := ℝ) 1 s *
          ((fun (x : ℂ) ↦ eval x ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) ∘ fun (y : ℝ) ↦ y • s) x +
        cexp (-(x • s)) *
          (eval (x • s) ((derivative : (a : ℂ[X]) → ℂ[X]) ((sumIDeriv : (a : ℂ[X]) → ℂ[X]) p)) *
            HSMul.hSMul (α := ℝ) 1 s)))
    x

Tactic:
(h₁.mul h₂).fun_neg

Premises used: HasDerivAt.fun_neg, HasDerivAt.mul