awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
simp : HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ + HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ < 1
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (1 / 2 + 1 / 2 * I) : ℝ) (1 : ℝ)

Tactic:
simp [normSq]

Premises used: Complex.normSq
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ + HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ < 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ x % y = x - y * (x / y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
rwa : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
rwa₁ : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ)
rwa₂ rwa₃ rwa₄ rwa₅ : ¬y = 0
⊢ Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
rwa [Ne, ← toComplex_zero, toComplex_inj]

Premises used: Ne, GaussianInt.toComplex_inj, GaussianInt.toComplex_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
this : Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
⊢ Eq (α := ℝ) ((↑(norm (x % y)) : ℝ) : ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
          (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)

Tactic:
simp [mod_def]

Premises used: GaussianInt.mod_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
this : Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
rw :
  Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
          (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HMul.hMul (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
          (HSub.hSub (β := ℂ)
            (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)
rw₁ :
  Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
          (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HMul.hMul (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)) -
          HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ)) :
      ℝ)
rw₂ rw₃ :
  Eq (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
          (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ)
        (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
          (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) :
      ℝ)
⊢ (normSq : (a : ℂ) → ℝ)
      (HSub.hSub (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
        (HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ))) =
    HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) : ℝ)
      ((normSq : (a : ℂ) → ℝ)
          (HSub.hSub (β := ℂ)
            (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
            ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ)) :
        ℝ)

Tactic:
rw [← normSq_mul, mul_sub, mul_div_cancel₀ _ this]

Premises used: mul_sub, Complex.normSq_mul, mul_div_cancel₀
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
this : Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) : ℝ) (1 : ℝ) =
    (↑(norm y) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ LT.lt (α := ℤ) (↑(norm (x % y)).natAbs : ℤ) (↑(norm y).natAbs : ℤ)

Tactic:
simp [norm_mod_lt x hy]

Premises used: GaussianInt.norm_mod_lt
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
rw : (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs
⊢ (norm x).natAbs ≤ (norm (x * y)).natAbs

Tactic:
rw [Zsqrtd.norm_mul, Int.natAbs_mul]

Premises used: Int.natAbs_mul, Zsqrtd.norm_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
rw : (↑1 : ℤ) ≤ norm y
⊢ LE.le (α := ℤ) (↑1 : ℤ) (↑(norm y).natAbs : ℤ)

Tactic:
rw [abs_natCast_norm]

Premises used: GaussianInt.abs_natCast_norm
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ (↑1 : ℤ) ≤ norm y

Tactic:
Int.add_one_le_of_lt (norm_pos.2 hy)

Premises used: Iff.mpr, GaussianInt.norm_pos, Int.add_one_le_of_lt, Int.add
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ (↑1 : ℤ) ≤ norm y

Tactic:
exact Int.add_one_le_of_lt (norm_pos.2 hy)

Premises used: Iff.mpr, GaussianInt.norm_pos, Int.add_one_le_of_lt
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs

Tactic:
exact le_mul_of_one_le_right (Nat.zero_le _) (Int.ofNat_le.1 (by
    rw [abs_natCast_norm]
    exact Int.add_one_le_of_lt (norm_pos.2 hy)))

Premises used: Nat.zero_le, le_mul_of_one_le_right, Iff.mp, Int.ofNat_le
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ Ne (α := ℤ[i]) 0 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
simp : Eq (α := ℤ[i]) { re := 0, im := 0 } 0
⊢ ∀ (a : ℤ[i]), a / 0 = 0

Tactic:
simp [div_def]

Premises used: GaussianInt.div_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ Eq (α := ℤ[i]) { re := 0, im := 0 } 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x x_1 : ℤ[i]
⊢ x_1 * (x / x_1) + x % x_1 = x

Tactic:
simp [mod_def]

Premises used: GaussianInt.mod_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
rw : ¬(Int.natAbs (↑p : ℤ) = 1 ∧ Int.natAbs (↑p : ℤ) = 1)
⊢ ¬(norm (d := -1) (↑p : ℤ[i])).natAbs = 1

Tactic:
rw [norm_natCast, Int.natAbs_mul, mul_eq_one]

Premises used: Int.natAbs_mul, mul_eq_one, Zsqrtd.norm_natCast
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
⊢ ¬(Int.natAbs (↑p : ℤ) = 1 ∧ Int.natAbs (↑p : ℤ) = 1)

Tactic:
fun h => (ne_of_lt hp.1.one_lt).symm h.1

Premises used: Nat.Prime.one_lt, Ne.symm, And.left, ne_of_lt, Not, Fact.out
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
⊢ ¬(Int.natAbs (↑p : ℤ) = 1 ∧ Int.natAbs (↑p : ℤ) = 1)

Tactic:
exact fun h => (ne_of_lt hp.1.one_lt).symm h.1

Premises used: Nat.Prime.one_lt, Ne.symm, ne_of_lt, Fact.out
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
hpu : ¬IsUnit (M := ℤ[i]) (↑p : ℤ[i])
⊢ ∃ (a : ℤ[i]) (b : ℤ[i]), (↑p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b

Tactic:
simpa [irreducible_iff, hpu, not_forall, not_or] using hpi

Premises used: not_or, irreducible_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
hpu : ¬IsUnit (M := ℤ[i]) (↑p : ℤ[i])
hab : ∃ (a : ℤ[i]) (b : ℤ[i]), (↑p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : (↑p : ℤ[i]) = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
rw : (↑((norm a).natAbs * (norm b).natAbs) : ℤ) = norm (a * b)
⊢ (norm a).natAbs * (norm b).natAbs = HPow.hPow (β := ℕ) p 2

Tactic:
rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]

Premises used: Int.natCast_pow, sq, Zsqrtd.norm_natCast, Int.natCast_inj
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
hpu : ¬IsUnit (M := ℤ[i]) (↑p : ℤ[i])
hab : ∃ (a : ℤ[i]) (b : ℤ[i]), (↑p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : (↑p : ℤ[i]) = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ (↑((norm a).natAbs * (norm b).natAbs) : ℤ) = norm (a * b)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
hpu : ¬IsUnit (M := ℤ[i]) (↑p : ℤ[i])
hab : ∃ (a : ℤ[i]) (b : ℤ[i]), (↑p : ℤ[i]) = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : (↑p : ℤ[i]) = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : (norm a).natAbs = p
⊢ HPow.hPow (β := ℕ) a.re.natAbs 2 + HPow.hPow (β := ℕ) a.im.natAbs 2 = p

Tactic:
simpa [natAbs_norm_eq, sq] using hnap

Premises used: GaussianInt.natAbs_norm_eq, sq
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp2 : p = 2
⊢ (↑p : ℤ[i]) = HMul.hMul (α := ℤ[i]) { re := 1, im := 1 : ℤ√(-1) } { re := 1, im := -1 : ℤ√(-1) } →
    IsUnit (M := ℤ[i]) { re := 1, im := 1 } ∨ IsUnit (M := ℤ[i]) { re := 1, im := -1 }

Tactic:
have := hpi.irreducible.isUnit_or_isUnit (a := ⟨1, 1⟩) (b := ⟨1, -1⟩)
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp2 : p = 2
this :
  (↑p : ℤ[i]) = HMul.hMul (α := ℤ[i]) { re := 1, im := 1 : ℤ√(-1) } { re := 1, im := -1 : ℤ√(-1) } →
    IsUnit (M := ℤ[i]) { re := 1, im := 1 } ∨ IsUnit (M := ℤ[i]) { re := 1, im := -1 }
⊢ p % 4 = 3

Tactic:
simp [hp2, Zsqrtd.ext_iff, ← norm_eq_one_iff, norm_def] at this

Premises used: Zsqrtd.norm_def, Zsqrtd.norm_eq_one_iff, Zsqrtd.ext_iff
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
let : ∀ (k : ZMod p) (hk : -1 = k * k), False
⊢ False

Tactic:
let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 hp3
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ZMod p
hk : -1 = k * k
⊢ ∃ (k' : ℕ) (_ : k' < p), (↑k' : ZMod p) = k

Tactic:
⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩

Premises used: ZMod.natCast_zmod_val, Exists.intro, ZMod.val_lt, ZMod.val
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ZMod p
hk : -1 = k * k
⊢ ∃ (k' : ℕ) (_ : k' < p), (↑k' : ZMod p) = k

Tactic:
exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ZMod p
hk : -1 = k * k
obtain : ∀ (k : ℕ) (k_lt_p : k < p) (hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)), False
⊢ False

Tactic:
obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
        exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
rw : p ∣ k * k + 1
rw₁ : Eq (α := ZMod p) (↑(k * k + 1) : ZMod p) 0
rw₂ : HAdd.hAdd (α := ZMod p) (↑(k * k) : ZMod p) (↑1 : ZMod p) = 0
rw₃ : HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p) + (↑1 : ZMod p) = 0
rw₄ : HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p) + 1 = 0
rw₅ : HAdd.hAdd (α := ZMod p) (-1) 1 = 0
rw₆ rw₇ : Eq (α := ZMod p) 0 0
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1

Tactic:
rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
          ← hk, neg_add_cancel]

Premises used: pow_two, ZMod, Nat.cast_add, Nat.cast_mul, neg_add_cancel, CharP.cast_eq_zero_iff, Nat.cast_one
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1

Tactic:
have hpk : p ∣ k ^ 2 + 1 := by
        rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
          ← hk, neg_add_cancel]
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
re :
  (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).re =
    (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).re
im :
  (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).im =
    (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).im
⊢ HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }

Tactic:
ext
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
⊢ (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).re =
    (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).re

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
⊢ (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).im =
    (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).im

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
⊢ HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }

Tactic:
have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by ext <;> simp [sq]
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k_lt_p : 0 < p
hk : -1 = HMul.hMul (α := ZMod p) (↑0 : ZMod p) (↑0 : ZMod p)
hpk : p ∣ HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑0 : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑0 : ℤ), im := 1 } { re := (↑0 : ℤ), im := -1 }
⊢ False

Tactic:
simp at hk
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
⊢ k ≠ 0

Tactic:
have hk₀ : k ≠ 0 := by rintro rfl; simp at hk
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
⊢ 1 + k * k ≤ k * (k + 1)

Tactic:
lia
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
⊢ 1 + k * k < p * p

Tactic:
have hkltp := calc
          1 + k * k ≤ k * (k + 1) := by lia
          _ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := -1 } = (↑p : ℤ[i]) * x
rw rw₁ : (norm ((↑p : ℤ[i]) * x)).natAbs = (norm ((↑p : ℤ[i]) * x)).natAbs
⊢ (norm ((↑p : ℤ[i]) * x)).natAbs = (norm (d := -1) { re := (↑k : ℤ), im := -1 }).natAbs

Tactic:
rw [hx]
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := -1 } = (↑p : ℤ[i]) * x
⊢ (norm (d := -1) { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).natAbs < (norm (d := -1) (↑p : ℤ[i])).natAbs

Tactic:
simpa [add_comm, Zsqrtd.norm] using hkltp

Premises used: add_comm, Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := -1 } = (↑p : ℤ[i]) * x
hx0 : x = 0
⊢ Ne (α := ℤ) (-1) 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := -1 } = (↑p : ℤ[i]) * x
hx0 : x = 0
⊢ Eq (α := ℤ) (-1) 0

Tactic:
simpa [hx0] using congr_arg Zsqrtd.im hx

Premises used: congr_arg, Zsqrtd.im
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
⊢ ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }

Tactic:
have hpk₁ : ¬(p : ℤ[i]) ∣ ⟨k, -1⟩ := fun ⟨x, hx⟩ =>
        lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
          calc
            (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, -1⟩).natAbs := by rw [hx]
            _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
            _ ≤ (norm (p * x : ℤ[i])).natAbs :=
              norm_le_norm_mul_left _ fun hx0 =>
                show (-1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := 1 } = (↑p : ℤ[i]) * x
rw rw₁ : (norm ((↑p : ℤ[i]) * x)).natAbs = (norm ((↑p : ℤ[i]) * x)).natAbs
⊢ (norm ((↑p : ℤ[i]) * x)).natAbs = (norm (d := -1) { re := (↑k : ℤ), im := 1 }).natAbs

Tactic:
rw [hx]
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := 1 } = (↑p : ℤ[i]) * x
⊢ (norm (d := -1) { re := (↑k : ℤ), im := 1 : ℤ√(-1) }).natAbs < (norm (d := -1) (↑p : ℤ[i])).natAbs

Tactic:
simpa [add_comm, Zsqrtd.norm] using hkltp

Premises used: add_comm, Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := 1 } = (↑p : ℤ[i]) * x
hx0 : x = 0
⊢ Ne (α := ℤ) 1 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
h : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
x : ℤ[i]
hx : { re := (↑k : ℤ), im := 1 } = (↑p : ℤ[i]) * x
hx0 : x = 0
⊢ Eq (α := ℤ) 1 0

Tactic:
simpa [hx0] using congr_arg Zsqrtd.im hx

Premises used: congr_arg, Zsqrtd.im