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

State before:
x y : GaussInt
hy : y ≠ 0
⊢ ¬(x * y).norm.natAbs < x.norm.natAbs
Tactic:
apply not_lt_of_ge
State after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ (x * y).norm.natAbs ≥ x.norm.natAbs

State before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ (x * y).norm.natAbs ≥ x.norm.natAbs
Tactic:
rw [norm_mul, Int.natAbs_mul]
State after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ x.norm.natAbs * y.norm.natAbs ≥ x.norm.natAbs

State before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ x.norm.natAbs * y.norm.natAbs ≥ x.norm.natAbs
Tactic:
apply le_mul_of_one_le_right (Nat.zero_le _)
State after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ 1 ≤ y.norm.natAbs

State before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ 1 ≤ y.norm.natAbs
Tactic:
apply Int.ofNat_le.1
State after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑y.norm.natAbs

State before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑y.norm.natAbs
Tactic:
rw [coe_natAbs_norm]
State after:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ y.norm

State before:
case h
x y : GaussInt
hy : y ≠ 0
⊢ ↑1 ≤ y.norm
Tactic:
exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)
State after:
no goals