awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) 0
rwa : ∀ (this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) (↑0 : R)), a = 0
⊢ a = 0
have rwa₁ : ∀ (this : a.norm = 0), a = 0
Tactic: rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) 0
rwa : ∀ (this : Eq.{u_1 + 1} (α := R) (↑a.norm : R) (↑0 : R)), a = 0
rwa₁ : ∀ (this : a.norm = 0), a = 0
⊢ a = 0
have rwa₂ : ∀ (this : a = 0), a = 0
Tactic: rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
⊢ a = 0
have suffices : Eq (α := R)
  ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
  (0 : R)
Tactic: suffices lift r a.norm = 0 by
      simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
⊢ Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)
have rw : Eq (α := R)
  ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (a * star a) : R) (0 : R)
Tactic: rw [norm_eq_mul_conj, map_mul, ha, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
rw :
  Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (a * star a) : R)
    (0 : R)
⊢ Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)
have rw₁ : HMul.hMul (α := R) (β := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
  0
Tactic: rw [norm_eq_mul_conj, map_mul, ha, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
rw :
  Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (a * star a) : R)
    (0 : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
    0
⊢ Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)
have rw₂ : HMul.hMul (α := R) (β := R) (0 : R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
  0
Tactic: rw [norm_eq_mul_conj, map_mul, ha, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : CharZero R
d : ℤ
r : { r : R // r * r = (↑d : R) }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha :
  Eq (α := R) ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R) (0 : R)
h_inj : Function.Injective.{1, u_1 + 1} (β := R) Int.cast
rw :
  Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (a * star a) : R)
    (0 : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) a : R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
    0
rw₂ :
  HMul.hMul (α := R) (β := R) (0 : R)
      ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (star a) : R) =
    0
⊢ Eq (α := R)
    ((((lift : (a : { r : R // r * r = (↑d : R) }) → ℤ√d →+* R) r : ℤ√d →+* R) : (a : ℤ√d) → R) (↑a.norm : ℤ√d) : R)
    (0 : R)
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [norm_eq_mul_conj, map_mul, ha, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ Membership.mem (γ := Submonoid (ℤ√d)) (unitary (ℤ√d)) a
have rw : a.norm = 1 ↔ Eq (α := ℤ√d) (↑a.norm : ℤ√d) 1
Tactic: rw [Unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.Basic (goal)
Goal:
d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ Eq (α := ℤ√d) (↑a.norm : ℤ√d) 1
have norm_cast : a.norm = 1 ↔ a.norm = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ (toComplex : (a : ℤ[i]) → ℂ) x = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }
have a : Complex.re ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.re
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
a : Complex.re ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.re
⊢ (toComplex : (a : ℤ[i]) → ℂ) x = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }
have a₁ : Complex.im ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) (star x) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) : ℂ)
have rw : { re := (↑(star x).re : ℝ), im := (↑(star x).im : ℝ) : ℂ } =
  (starRingEnd ℂ : (a : ℂ) → ℂ) { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }
Tactic: rw [toComplex_def₂, toComplex_def₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔ x = y
have mk : ∀ (re im : ℤ),
  Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im } : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔
    { re := re, im := im } = y
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
y : ℤ[i]
re im : ℤ
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im } : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔
    { re := re, im := im } = y
have mk : ∀ (re_1 im_1 : ℤ),
  Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im } : ℂ)
      ((toComplex : (a : ℤ[i]) → ℂ) { re := re_1, im := im_1 } : ℂ) ↔
    Eq (α := ℤ[i]) { re := re, im := im } { re := re_1, im := im_1 }
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) (0 : ℂ) ↔ x = 0
have rw : Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ) ↔ x = 0
Tactic: rw [← toComplex_zero, toComplex_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
rw : Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ) ↔ x = 0
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) (0 : ℂ) ↔ x = 0
have rw₁ : x = 0 ↔ x = 0
Tactic: rw [← toComplex_zero, toComplex_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ (↑(norm x) : ℂ) = (↑((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)) : ℂ)
have mk : ∀ (re im : ℤ),
  (↑(norm (d := -1) { re := re, im := im }) : ℂ) =
    (↑((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im : ℤ√(-1) } : ℂ)) : ℂ)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ norm x = 0 ↔ x = 0
have rw : Eq (α := ℝ) (↑(norm x) : ℝ) (↑0 : ℝ) ↔ x = 0
Tactic: rw [← @Int.cast_inj ℝ _ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ 0 < norm x ↔ x ≠ 0
have rw : 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
Tactic: rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ (norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs
have zify : |norm x| = |x.re| * |x.re| + |x.im| * |x.im|
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x : ℤ[i]
⊢ |norm x| = |x.re| * |x.re| + |x.im| * |x.im|
have rw : norm x = |x.re| * |x.re| + |x.im| * |x.im|
Tactic: rw [abs_norm (by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
⊢ Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y)) =
    (↑(round
          (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
      ℝ)
have rw : Complex.re
    ((toComplex : (a : ℤ[i]) → ℂ)
      { re := round (α := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑(x * star y).re : ℚ) (↑(norm y) : ℚ)) : ℝ),
        im := round (HDiv.hDiv (α := ℚ) (↑(x * star y).im : ℚ) (↑(norm y) : ℚ)) : ℤ√(-1) }) =
  (↑(round (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
    ℝ)
Tactic: rw [div_def, ← @Rat.round_cast ℝ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
⊢ Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y)) =
    (↑(round
          (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
      ℝ)
have rw : Complex.im
    ((toComplex : (a : ℤ[i]) → ℂ)
      { re := round (α := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑(x * star y).re : ℚ) (↑(norm y) : ℚ)) : ℝ),
        im := round (α := ℝ) (↑(HDiv.hDiv (α := ℚ) (↑(x * star y).im : ℚ) (↑(norm y) : ℚ)) : ℝ) : ℤ√(-1) }) =
  (↑(round (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
    ℝ)
Tactic: rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ x.re * x.re + x.im * x.im ≤ y.re * y.re + y.im * y.im
have nlinarith : y.re * y.re + y.im * y.im < x.re * x.re + x.im * x.im →
  y.re * y.re + y.im * y.im - (x.re * x.re + x.im * x.im) + (HPow.hPow (β := ℕ) x.re 2 - HPow.hPow (β := ℕ) y.re 2) +
      (HPow.hPow (β := ℕ) x.im 2 - HPow.hPow (β := ℕ) y.im 2) =
    0
Tactic: nlinarith [sq_le_sq.mpr hre, sq_le_sq.mpr him]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
⊢ HSub.hSub (β := ℂ)
      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
      ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ) =
    (↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
        (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
      ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
            ℂ) -
          (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
        I
have a : (HSub.hSub (β := ℂ)
      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
      ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ)).re =
  ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
        (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
      ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
            ℂ) -
          (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
        I).re
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
a :
  (HSub.hSub (β := ℂ)
        (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
        ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ)).re =
    ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
          (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
        ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
              ℂ) -
            (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
          I).re
⊢ HSub.hSub (β := ℂ)
      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
      ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ) =
    (↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
        (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
      ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
            ℂ) -
          (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
        I
have a₁ : (HSub.hSub (β := ℂ)
      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ))
      ((toComplex : (a : ℤ[i]) → ℂ) (x / y) : ℂ)).im =
  ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
        (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
      ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
            ℂ) -
          (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
        I).im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (hypothesis)
Goal:
x y : ℤ[i]
⊢ LE.le (α := ℝ)
    ((normSq : (a : ℂ) → ℝ)
        ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re :
              ℂ) -
            (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
          ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                      ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
                ℂ) -
              (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
            I) :
      ℝ)
    ((normSq : (a : ℂ) → ℝ) (1 / 2 + 1 / 2 * I) : ℝ)
have this : Eq (α := ℝ) |2⁻¹| 2⁻¹
Tactic: have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by simp)
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
            (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
          ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                      ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
                ℂ) -
              (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
            I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|
have rw : |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
          (↑(↑(round
                    (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                        ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
                ℝ) :
            ℂ) +
        ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
              ℂ) -
            (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
          I).re| ≤
  |(1 / 2 + 1 / 2 * I).re|
Tactic: rw [toComplex_re_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
            (↑(↑(round
                      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                          ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
                  ℝ) :
              ℂ) +
          ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                      ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
                ℂ) -
              (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
            I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|
have simp : |(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re -
      (↑(round
            (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
        ℝ)| ≤
  2⁻¹
Tactic: simp [normSq, this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
            (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
          ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                      ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
                ℂ) -
              (↑(Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ)) *
            I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|
have rw : |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
          (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
        ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
              ℂ) -
            (↑(↑(round
                      (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                          ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
                  ℝ) :
              ℂ)) *
          I).im| ≤
  |(1 / 2 + 1 / 2 * I).im|
Tactic: rw [toComplex_im_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re : ℂ) -
            (↑(Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y))) : ℂ) +
          ((↑(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                      ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im :
                ℂ) -
              (↑(↑(round
                        (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                            ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
                    ℝ) :
                ℂ)) *
            I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|
have simp : |(HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im -
      (↑(round
            (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)
                ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
        ℝ)| ≤
  2⁻¹
Tactic: simp [normSq, this]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (1 / 2 + 1 / 2 * I) : ℝ) (1 : ℝ)
have simp : HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ + HMul.hMul (α := ℝ) 2⁻¹ 2⁻¹ < 1
Tactic: simp [normSq]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
⊢ Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
have rwa : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
Tactic: rwa [Ne, ← toComplex_zero, toComplex_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
rwa : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
⊢ Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
have rwa₁ : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ)
Tactic: rwa [Ne, ← toComplex_zero, toComplex_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
rwa : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
rwa₁ : ¬Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ)
⊢ Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
have rwa₂ : ¬y = 0
Tactic: rwa [Ne, ← toComplex_zero, toComplex_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Zsqrtd.GaussianInt (goal)
Goal:
x y : ℤ[i]
hy : y ≠ 0
this : Ne (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) (0 : ℂ)
⊢ (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 : ℂ)
        (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]