-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem normSq_div_sub_div_lt_one (x y : ℤ[i]) :
    Complex.normSq ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ)) < 1 :=
  calc
    Complex.normSq ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ))
    _ = Complex.normSq
      ((x / y : ℂ).re - ((x / y : ℤ[i]) : ℂ).re + ((x / y : ℂ).im - ((x / y : ℤ[i]) : ℂ).im) *
        I : ℂ) :=
      congr_arg _ <| by apply Complex.ext <;> simp
    _ ≤ Complex.normSq (1 / 2 + 1 / 2 * I)

Proof state:
x y : ℤ[i]
⊢ 0 ≤ 2⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℤ[i]
⊢ normSq
      (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤
    normSq (1 / 2 + 1 / 2 * I)

Tactic:
have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by norm_num)

Result:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ normSq
      (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤
    normSq (1 / 2 + 1 / 2 * I)

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑↑(round (toComplex x / toComplex y).im)) * I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|

Tactic:
simp [normSq, this]

Result:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).im - ↑(round (toComplex x / toComplex y).im)| ≤ 2⁻¹

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).re - ↑(round (toComplex x / toComplex y).re)| ≤ 2⁻¹

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

Result:
no goals

Proof state:
x y : ℤ[i]
⊢ normSq (1 / 2 + 1 / 2 * I) < 1

Tactic:
simp [normSq]

Result:
x y : ℤ[i]
⊢ 2⁻¹ * 2⁻¹ + 2⁻¹ * 2⁻¹ < 1

Proof state:
x y : ℤ[i]
⊢ 2⁻¹ * 2⁻¹ + 2⁻¹ * 2⁻¹ < 1

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ normSq
      (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤
    normSq (1 / 2 + 1 / 2 * I)

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

Result:
no goals

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|

Tactic:
rw [toComplex_div_im]

Result:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑↑(round (toComplex x / toComplex y).im)) * I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|

Tactic:
rw [toComplex_div_re]

Result:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑↑(round (toComplex x / toComplex y).re) +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑↑(round (toComplex x / toComplex y).re) +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|

Tactic:
simp [normSq, this]

Result:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).re - ↑(round (toComplex x / toComplex y).re)| ≤ 2⁻¹

Proof state:
x y : ℤ[i]
⊢ toComplex x / toComplex y - toComplex (x / y) =
    ↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
      (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I

Tactic:
apply Complex.ext <;> simp

Result:
no goals

Proof state:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).im - ↑(round (toComplex x / toComplex y).im)| ≤ 2⁻¹

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

Result:
no goals