Theorem: GaussInt.norm_mod_lt (MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm
Tactic:
have norm_y_pos : 0 < norm y := by rwa [norm_pos]
State after:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ (x % y).norm < y.norm

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ (x % y).norm < y.norm
Tactic:
have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
State after:
case H1
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }

x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm < y.norm

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm < y.norm
Tactic:
have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
State after:
case H2
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm ≤ y.norm / 2 * y.norm

x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ (x % y).norm < y.norm

State before:
x y : GaussInt
hy : y ≠ 0
⊢ 0 < y.norm
Tactic:
rwa [norm_pos]
State after:
no goals

State before:
case H1
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
Tactic:
ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
State after:
no goals

State before:
case H2
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
Tactic:
calc
  norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
  _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
      + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
  _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
  _ = norm y / 2 * (norm y / 2 * 2) := by ring
  _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm * y.norm = (x % y * y.conj).norm
Tactic:
simp only [norm_mul, norm_conj]
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y * y.conj).norm =
    |(x.re * y.re + x.im * y.im).mod' y.norm| ^ 2 + |(-(x.re * y.im) + x.im * y.re).mod' y.norm| ^ 2
Tactic:
simp [H1, norm, sq_abs]
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ |(x.re * y.re + x.im * y.im).mod' y.norm| ^ 2 + |(-(x.re * y.im) + x.im * y.re).mod' y.norm| ^ 2 ≤
    (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2
Tactic:
gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 = y.norm / 2 * (y.norm / 2 * 2)
Tactic:
ring
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * (y.norm / 2 * 2) ≤ y.norm / 2 * y.norm
Tactic:
gcongr
State after:
case h
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * 2 ≤ y.norm

State before:
case h
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ y.norm / 2 * 2 ≤ y.norm
Tactic:
apply Int.ediv_mul_le
State after:
case h.H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ 2 ≠ 0

State before:
case h.H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm / 2 < y.norm
Tactic:
apply Int.ediv_lt_of_lt_mul
State after:
case H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ 0 < 2

case H'
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm < y.norm * 2

State before:
case H
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case H'
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm < y.norm * 2
Tactic:
linarith
State after:
no goals