Theorem: Int.abs_mod'_le (MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

State before:
a b : ℤ
h : 0 < b
⊢ |a.mod' b| ≤ b / 2
Tactic:
rw [mod', abs_le]
State after:
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2 ∧ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2 ∧ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
constructor
State after:
case left
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2

case right
a b : ℤ
h : 0 < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.emod_lt_of_pos (a + b / 2) h
State after:
case right
a b : ℤ
h : 0 < b
this : (a + b / 2) % b < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
this : (a + b / 2) % b < b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.ediv_add_emod b 2
State after:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
have := Int.emod_lt_of_pos b zero_lt_two
State after:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
revert this
State after:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ b % 2 < 2 → (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
this✝ : (a + b / 2) % b < b
this : 2 * (b / 2) + b % 2 = b
⊢ b % 2 < 2 → (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
intro this
State after:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2

State before:
case right
a b : ℤ
h : 0 < b
this✝¹ : (a + b / 2) % b < b
this✝ : 2 * (b / 2) + b % 2 = b
this : b % 2 < 2
⊢ (a + b / 2) % b - b / 2 ≤ b / 2
Tactic:
linarith
State after:
no goals

State before:
case left
a b : ℤ
h : 0 < b
⊢ -(b / 2) ≤ (a + b / 2) % b - b / 2
Tactic:
linarith [Int.emod_nonneg (a + b / 2) h.ne']
State after:
no goals