Theorem: gaussInt.not_norm_mul_left_lt_norm (LeanCourse/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean)

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

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

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

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

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

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