awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
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) : ℂ))) :
      ℝ)
⊢ (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) : ℂ)) :
        ℝ)
have 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) : ℂ)) :
    ℝ)
Tactic: rw [← normSq_mul, mul_sub, mul_div_cancel₀ _ this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
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) : ℂ)) :
      ℝ)
⊢ (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) : ℂ)) :
        ℝ)
have 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) : ℂ))) :
    ℝ)
Tactic: rw [← normSq_mul, mul_sub, mul_div_cancel₀ _ this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm (x * y)).natAbs
have rw : (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs
Tactic: rw [Zsqrtd.norm_mul, Int.natAbs_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ LE.le (α := ℤ) (↑1 : ℤ) (↑(norm y).natAbs : ℤ)
have rw : (↑1 : ℤ) ≤ norm y
Tactic: rw [abs_natCast_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
⊢ ∀ (a : ℤ[i]), a / 0 = 0
have simp : Eq (α := ℤ[i]) { re := 0, im := 0 } 0
Tactic: simp [div_def]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
⊢ ¬(norm (d := -1) (↑p : ℤ[i])).natAbs = 1
have rw : ¬(Int.natAbs (↑p : ℤ) = 1 ∧ Int.natAbs (↑p : ℤ) = 1)
Tactic: rw [norm_natCast, Int.natAbs_mul, mul_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
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 = HPow.hPow (β := ℕ) p 2
have rw : (↑((norm a).natAbs * (norm b).natAbs) : ℤ) = norm (a * b)
Tactic: rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp2 : p = 2
⊢ p % 4 = 3
have 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 }
Tactic: have := hpi.irreducible.isUnit_or_isUnit (a := ⟨1, 1⟩) (b := ⟨1, -1⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ False
have let : ∀ (k : ZMod p) (hk : -1 = k * k), False
Tactic: let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 hp3
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ False
have obtain : ∀ (k : ℕ) (k_lt_p : k < p) (hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)), 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⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
have rw : p ∣ k * k + 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₁ : Eq (α := ZMod p) (↑(k * k + 1) : ZMod p) 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₂ : HAdd.hAdd (α := ZMod p) (↑(k * k) : ZMod p) (↑1 : ZMod p) = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₃ : HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p) + (↑1 : ZMod p) = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₄ : HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p) + 1 = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₅ : HAdd.hAdd (α := ZMod p) (-1) 1 = 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ p ∣ HPow.hPow (β := ℕ) k 2 + 1
have rw₆ : Eq (α := ZMod p) 0 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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)
⊢ False
have hpk : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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 }
have re : (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).re =
  (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).re
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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
⊢ HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
have im : (HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1).im =
  (HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) }).im
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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
⊢ False
have hkmul : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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 }
⊢ False
have hk₀ : k ≠ 0
Tactic: have hk₀ : k ≠ 0 := by rintro rfl; simp at hk
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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
⊢ False
have hkltp : 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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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 ((↑p : ℤ[i]) * x)).natAbs = (norm (d := -1) { re := (↑k : ℤ), im := -1 }).natAbs
have rw : (norm ((↑p : ℤ[i]) * x)).natAbs = (norm ((↑p : ℤ[i]) * x)).natAbs
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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
⊢ False
have hpk₁ : ¬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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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 ((↑p : ℤ[i]) * x)).natAbs = (norm (d := -1) { re := (↑k : ℤ), im := 1 }).natAbs
have rw : (norm ((↑p : ℤ[i]) * x)).natAbs = (norm ((↑p : ℤ[i]) * x)).natAbs
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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 }
⊢ False
have hpk₂ : ¬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
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
⊢ False
have obtain : ∀ (y : ℕ) (hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y), False
Tactic: obtain ⟨y, hy⟩ := hpk
Cleared hypotheses: hpk
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
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)
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 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
⊢ HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) } =
    HMul.hMul (α := ℤ[i]) (↑p : ℤ[i]) (↑y : ℤ[i])
have rw : HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 = (↑(HPow.hPow (β := ℕ) k 2 + 1) : ℤ[i])
Tactic: rw [← hkmul, ← Nat.cast_mul p, ← hy]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (hypothesis)
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)
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 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
⊢ False
have this : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 } ∨
  Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
Tactic: have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
a b : ℕ
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p
⊢ ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑p : ZMod 4)
have rw : ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑3 : ZMod 4)
Tactic: rw [← ZMod.natCast_mod p 4, hp3]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
have inl : ∀ (hab : r a b), a = b
Tactic: obtain hab | hab | hab := trichotomous_of r a b
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : ∀ (hab : r a b), a = b
⊢ a = b
have inr : ∀ (hab : a = b), a = b
Tactic: obtain hab | hab | hab := trichotomous_of r a b
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : ∀ (hab : r a b), a = b
inr : ∀ (hab : a = b), a = b
⊢ a = b
have inr₁ : ∀ (hab : r b a), a = b
Tactic: obtain hab | hab | hab := trichotomous_of r a b
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : Membership.mem (γ := Set β) ((⇑φ : (a : α) → β) '' s) b
b' : β
hb' : Membership.mem (γ := Set β) ((⇑φ : (a : α) → β) '' s) b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
have rw : ∀ (hb : ∃ x ∈ s, (φ : (a : α) → β) x = b) ⦃b' : β⦄ (hb' : ∃ x ∈ s, (φ : (a : α) → β) x = b') (h₁ : b ≠ b')
  (h₂ : r' b b'), False
Tactic: rw [Set.mem_image] at hb hb'
Cleared hypotheses: hb, b', hb', h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, (φ : (a : α) → β) x = b
b' : β
hb' : ∃ x ∈ s, (φ : (a : α) → β) x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
have obtain : ∀ (a : α) (has : a ∈ s) (a' : α) (has' : a' ∈ s)
  (h₁ : Ne.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β))
  (h₂ : r' ((φ : (a : α) → β) a) ((φ : (a : α) → β) a')), False
Tactic: obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
Cleared hypotheses: b, hb, b', hb', h₁, h₂