awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
a : ℤ√d
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a.norm = 1 ↔ a.norm = 1
⊢ a.norm = 1 ↔ Eq (α := ℤ√d) (↑a.norm : ℤ√d) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Zsqrtd.Basic
Goal:
d : ℤ
⊢ Eq (α := Submonoid (ℤ√d)) (MonoidHom.mker (F := ℤ√d →* ℤ) normMonoidHom) (unitary (ℤ√d))

Tactic:
Submonoid.ext fun _ => norm_eq_one_iff_mem_unitary

Premises used: Submonoid.ext, Zsqrtd.norm_eq_one_iff_mem_unitary
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ I * I = (↑(-1) : ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ (toComplex : (a : ℤ[i]) → ℂ) x = (↑x.re : ℂ) + (↑x.im : ℂ) * I

Tactic:
rfl

Premises used: rfl, Complex.I
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ
⊢ (toComplex : (a : ℤ[i]) → ℂ) { re := x, im := y } = (↑x : ℂ) + (↑y : ℂ) * I

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
a : Complex.re ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.re
a₁ : Complex.im ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.im
⊢ (toComplex : (a : ℤ[i]) → ℂ) x = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ Complex.re ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.re

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ Complex.im ((toComplex : (a : ℤ[i]) → ℂ) x) = { re := (↑x.re : ℝ), im := (↑x.im : ℝ) }.im

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ (↑x.re : ℝ) = Complex.re ((toComplex : (a : ℤ[i]) → ℂ) x)

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ (↑x.im : ℝ) = Complex.im ((toComplex : (a : ℤ[i]) → ℂ) x)

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ
⊢ Complex.re ((toComplex : (a : ℤ[i]) → ℂ) { re := x, im := y : ℤ√(-1) }) = (↑x : ℝ)

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ
⊢ Complex.im ((toComplex : (a : ℤ[i]) → ℂ) { re := x, im := y : ℤ√(-1) }) = (↑y : ℝ)

Tactic:
simp [toComplex_def]

Premises used: GaussianInt.toComplex_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ (toComplex : (a : ℤ[i]) → ℂ) (x + y) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)

Tactic:
toComplex.map_add _ _

Premises used: GaussianInt.toComplex, RingHom.map_add
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ (toComplex : (a : ℤ[i]) → ℂ) (x * y) =
    HMul.hMul (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)

Tactic:
toComplex.map_mul _ _

Premises used: GaussianInt.toComplex, RingHom.map_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 1 : ℂ) (1 : ℂ)

Tactic:
toComplex.map_one

Premises used: RingHom.map_one, GaussianInt.toComplex
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ) (0 : ℂ)

Tactic:
toComplex.map_zero

Premises used: GaussianInt.toComplex, RingHom.map_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) (-x) : ℂ) (-(toComplex : (a : ℤ[i]) → ℂ) x : ℂ)

Tactic:
toComplex.map_neg _

Premises used: RingHom.map_neg, GaussianInt.toComplex
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ (toComplex : (a : ℤ[i]) → ℂ) (x - y) =
    HSub.hSub (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)

Tactic:
toComplex.map_sub _ _

Premises used: RingHom.map_sub, GaussianInt.toComplex
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
rw :
  { re := (↑(star x).re : ℝ), im := (↑(star x).im : ℝ) : ℂ } =
    (starRingEnd ℂ : (a : ℂ) → ℂ) { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) (star x) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) : ℂ)

Tactic:
rw [toComplex_def₂, toComplex_def₂]

Premises used: GaussianInt.toComplex_def₂
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ { re := (↑(star x).re : ℝ), im := (↑(star x).im : ℝ) : ℂ } =
    (starRingEnd ℂ : (a : ℂ) → ℂ) { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }

Tactic:
congr_arg₂ _ rfl (Int.cast_neg _)

Premises used: Int.cast_neg, rfl, congr_arg₂
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ { re := (↑(star x).re : ℝ), im := (↑(star x).im : ℝ) : ℂ } =
    (starRingEnd ℂ : (a : ℂ) → ℂ) { re := (↑x.re : ℝ), im := (↑x.im : ℝ) : ℂ }

Tactic:
exact congr_arg₂ _ rfl (Int.cast_neg _)

Premises used: Int.cast_neg, rfl, congr_arg₂
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
mk :
  ∀ (re im : ℤ),
    Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im } : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔
      { re := re, im := im } = y
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔ x = y

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
y : ℤ[i]
re im : ℤ
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 }
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im } : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ) ↔
    { re := re, im := im } = y

Tactic:
cases y
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
re im 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:
simp [toComplex_def₂]

Premises used: GaussianInt.toComplex_def₂
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
⊢ Function.Injective (α := ℤ[i]) (β := ℂ) (⇑toComplex : (a : ℤ[i]) → ℂ)

Tactic:
fun ⦃_ _⦄ ↦ toComplex_inj.mp

Premises used: GaussianInt.toComplex_inj, Iff.mp, Function.Injective
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
rw : Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) 0 : ℂ) ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ Eq (α := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) (0 : ℂ) ↔ x = 0

Tactic:
rw [← toComplex_zero, toComplex_inj]

Premises used: GaussianInt.toComplex_inj, GaussianInt.toComplex_zero
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ Eq (α := ℝ) ((↑(x.re * x.re - -1 * x.im * x.im) : ℝ) : ℝ)
    (({ toFun := fun (z : ℂ) ↦ z.re * z.re + z.im * z.im, map_zero' := normSq._proof_1, map_one' := normSq._proof_2,
            map_mul' := ⋯ } :
          (a : ℂ) → ℝ)
        ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) :
      ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
mk :
  ∀ (re im : ℤ),
    (↑(norm (d := -1) { re := re, im := im }) : ℂ) =
      (↑((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im : ℤ√(-1) } : ℂ)) : ℂ)
⊢ (↑(norm x) : ℂ) = (↑((normSq : (a : ℂ) → ℝ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ)) : ℂ)

Tactic:
cases x
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
re im : ℤ
⊢ (↑(Zsqrtd.re (d := -1) { re := re, im := im : ℤ√(-1) } * Zsqrtd.re (d := -1) { re := re, im := im : ℤ√(-1) } -
          -1 * Zsqrtd.im (d := -1) { re := re, im := im : ℤ√(-1) } *
            Zsqrtd.im (d := -1) { re := re, im := im : ℤ√(-1) }) :
      ℂ) =
    (↑(({ toFun := fun (z : ℂ) ↦ z.re * z.re + z.im * z.im, map_zero' := normSq._proof_1, map_one' := normSq._proof_2,
              map_mul' := ⋯ : ℂ →*₀ ℝ } :
            (a : ℂ) → ℝ)
          ((toComplex : (a : ℤ[i]) → ℂ) { re := re, im := im : ℤ√(-1) } : ℂ)) :
      ℂ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
rw : Eq (α := ℝ) (↑(norm x) : ℝ) (↑0 : ℝ) ↔ x = 0
⊢ norm x = 0 ↔ x = 0

Tactic:
rw [← @Int.cast_inj ℝ _ _ _]

Premises used: Int.cast_inj
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ Eq (α := ℝ) (↑(norm x) : ℝ) (↑0 : ℝ) ↔ x = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
rw : 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
⊢ 0 < norm x ↔ x ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]

Premises used: lt_iff_le_and_ne, GaussianInt.norm_eq_zero, Ne, eq_comm
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0

Tactic:
simp [norm_nonneg]

Premises used: GaussianInt.norm_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ (↑(norm x).natAbs : ℤ) = norm x

Tactic:
Int.natAbs_of_nonneg (norm_nonneg _)

Premises used: Int.natAbs_of_nonneg, GaussianInt.norm_nonneg
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
α : Type u_1
inst : AddGroupWithOne α
x : ℤ[i]
⊢ Eq.{u_1 + 1} (α := α) (↑(norm x).natAbs : α) (↑(norm x) : α)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
zify : |norm x| = |x.re| * |x.re| + |x.im| * |x.im|
⊢ (norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs

Tactic:
zify
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
rw : norm x = |x.re| * |x.re| + |x.im| * |x.im|
⊢ |norm x| = |x.re| * |x.re| + |x.im| * |x.im|

Tactic:
rw [abs_norm (by simp)]

Premises used: Zsqrtd.abs_norm
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x : ℤ[i]
⊢ norm x = |x.re| * |x.re| + |x.im| * |x.im|

Tactic:
simp [Zsqrtd.norm]

Premises used: Zsqrtd.norm
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ Eq (α := ℤ√(-1))
    { re := round (HMul.hMul (α := ℚ) (↑(x * star y).re : ℚ) (↑(norm y) : ℚ)⁻¹),
      im := round (HMul.hMul (α := ℚ) (↑(x * star y).im : ℚ) (↑(norm y) : ℚ)⁻¹) }
    { re := round (HDiv.hDiv (α := ℚ) (↑(x * star y).re : ℚ) (↑(norm y) : ℚ)),
      im := round (HDiv.hDiv (α := ℚ) (↑(x * star y).im : ℚ) (↑(norm y) : ℚ)) }

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
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) :
      ℝ)
⊢ Complex.re ((toComplex : (a : ℤ[i]) → ℂ) (x / y)) =
    (↑(round
          (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).re) :
      ℝ)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _]

Premises used: Rat.round_cast, GaussianInt.div_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ 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:
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, add_mul]

Premises used: add_mul, mul_assoc, Rat.round_cast, div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
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) :
      ℝ)
⊢ Complex.im ((toComplex : (a : ℤ[i]) → ℂ) (x / y)) =
    (↑(round
          (HDiv.hDiv (α := ℂ) (β := ℂ) ((toComplex : (a : ℤ[i]) → ℂ) x : ℂ) ((toComplex : (a : ℤ[i]) → ℂ) y : ℂ)).im) :
      ℝ)

Tactic:
rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]

Premises used: Rat.round_cast, GaussianInt.div_def
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ 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:
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, add_mul]

Premises used: add_mul, mul_assoc, Rat.round_cast, div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
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
⊢ x.re * x.re + x.im * x.im ≤ y.re * y.re + y.im * y.im

Tactic:
nlinarith [sq_le_sq.mpr hre, sq_le_sq.mpr him]

Premises used: Iff.mpr, sq_le_sq
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
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
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
⊢ 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

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ (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:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ (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:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ LE.le (α := ℝ) 0 2⁻¹

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
⊢ Eq (α := ℝ) |2⁻¹| 2⁻¹

Tactic:
have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by simp)
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
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|
⊢ |((↑(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|

Tactic:
rw [toComplex_re_div]

Premises used: GaussianInt.toComplex_re_div
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
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⁻¹
⊢ |((↑(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:
simp [normSq, this]

Premises used: Complex.normSq
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
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) :
          ℝ)| ≤
    2⁻¹

Tactic:
simpa using abs_sub_round (x / y : ℂ).re

Premises used: abs_sub_round, HDiv.hDiv, GaussianInt.toComplex, Complex.re, DFunLike.coe
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
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|
⊢ |((↑(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|

Tactic:
rw [toComplex_im_div]

Premises used: GaussianInt.toComplex_im_div
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
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⁻¹
⊢ |((↑(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:
simp [normSq, this]

Premises used: Complex.normSq
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |(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:
simpa using abs_sub_round (x / y : ℂ).im

Premises used: abs_sub_round, Complex.im, HDiv.hDiv, GaussianInt.toComplex, DFunLike.coe
-- Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt
Goal:
x y : ℤ[i]
this : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ 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) : ℝ)

Tactic:
exact normSq_le_normSq_of_re_le_of_im_le
        (by rw [toComplex_re_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).re)
        (by rw [toComplex_im_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).im)

Premises used: GaussianInt.normSq_le_normSq_of_re_le_of_im_le