-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_bmod {x : Int} {m : Nat} (h : 0 < m) : - (m/2) ≤ Int.bmod x m

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -1 * q ≤ -1 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
apply Int.le_refl

Result:
case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 1 / 2 = 0

Tactic:
decide

Result:
no goals

Proof state:
case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
all_goals try decide

Result:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
try decide

Result:
no goals

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
⊢ -((2 * q + ↑m % 2) / 2) ≤ (2 * q + ↑m % 2 + 1) / 2 - (2 * q + ↑m % 2)

Tactic:
generalize h : (m : Int) % 2 = r at *

Result:
case isFalse
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q r : Int
h : ↑m % 2 = r
v : r = 0 ∨ r = 1
⊢ -((2 * q + r) / 2) ≤ (2 * q + r + 1) / 2 - (2 * q + r)

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ (1 + 1) / 2 = 1

Tactic:
decide

Result:
no goals

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 1 - 2 = -1

Tactic:
decide

Result:
no goals

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
all_goals try apply Int.dvd_mul_right

Result:
no goals

Proof state:
case isTrue.refine_2
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ ↑m ≠ 0

Tactic:
exact Int.ne_of_gt (ofNat_pos.mpr h)

Result:
no goals

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ -1 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
apply Int.le_refl

Result:
case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Proof state:
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 1 / 2 = 0

Tactic:
decide

Result:
no goals

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -((2 * q + 1) / 2) ≤ (2 * q + 1 + 1) / 2 - (2 * q + 1)

Tactic:
rw [Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left,
  show (1 / 2 : Int) = 0 by decide, Int.add_assoc, Int.add_ediv_of_dvd_left,
  Int.mul_ediv_cancel_left, show ((1 + 1) / 2 : Int) = 1 by decide, ← Int.sub_sub,
  Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_right_comm, Int.add_assoc q,
  show (1 + -1 : Int) = 0 by decide, Int.add_zero, ← Int.neg_mul]

Result:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ -q ≤ q + -2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Proof state:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ 1 * q - 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Tactic:
rw [← Int.sub_mul, show (1 - 2 : Int) = -1 by decide]

Result:
case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ -1 * q ≤ -1 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

case isFalse.inl
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ∣ 2 * q

case isFalse.inl.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 0
⊢ 2 ≠ 0

Proof state:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : ¬x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ x % ↑m - ↑m

Tactic:
simp [Int.not_lt] at w

Result:
case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : (↑m + 1) / 2 ≤ x % ↑m
⊢ -(↑m / 2) ≤ x % ↑m - ↑m

Proof state:
x : Int
m : Nat
h : 0 < m
⊢ -(↑m / 2) ≤ x.bmod m

Tactic:
dsimp [bmod]

Result:
x : Int
m : Nat
h : 0 < m
⊢ -(↑m / 2) ≤ if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m

Proof state:
case isFalse.inr.H
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ≠ 0

Tactic:
try decide

Result:
no goals

Proof state:
case isFalse.inr
x : Int
m : Nat
h✝ : 0 < m
w : (↑m + 1) / 2 ≤ x % ↑m
q : Int
h : ↑m % 2 = 1
⊢ 2 ∣ 2 * q

Tactic:
try apply Int.dvd_mul_right

Result:
no goals

Proof state:
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
⊢ -(↑m / 2) ≤ if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m

Tactic:
split <;> rename_i w

Result:
case isTrue
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ x % ↑m

case isFalse
x : Int
m : Nat
h : 0 < m
v : ↑m % 2 = 0 ∨ ↑m % 2 = 1
w : ¬x % ↑m < (↑m + 1) / 2
⊢ -(↑m / 2) ≤ x % ↑m - ↑m