Theorem: gaussInt.norm_mod_lt (LeanCourse/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

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

State before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ norm (x % y) < norm y
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 < norm y
⊢ x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }

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

State before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) < norm y
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 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y ≤ norm y / 2 * norm y

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

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

State before:
case H1
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
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 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y ≤ norm y / 2 * norm y
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 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y = norm (x % y * conj y)
Tactic:
simp only [norm_mul, norm_conj]
State after:
no goals

State before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y * conj y) =
    |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
Tactic:
simp [H1, norm, sq_abs]
State after:
no goals

State before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ |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 ≤
    (norm y / 2) ^ 2 + (norm y / 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 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ (norm y / 2) ^ 2 + (norm y / 2) ^ 2 = norm y / 2 * (norm y / 2 * 2)
Tactic:
ring
State after:
no goals

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

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

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

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

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

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

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