-- Mathlib/Data/Int/CardIntervalMod.lean
theorem count_modEq_card (v : ℕ) :
    b.count (· ≡ v [MOD r]) = b / r + if v % r < b % r then 1 else 0

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
have hr' : 0 < (r : ℚ) := by positivity

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ count (fun x => x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
rw [← ofNat_inj, count_modEq_card_eq_ceil _ hr, cast_add]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Proof state:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0

Tactic:
rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', zero_mul,
  tsub_nonpos, ← neg_eq_neg_one_mul, neg_lt_sub_iff_lt_add, ← cast_add, cast_lt, cast_le]

Result:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ v % r < r + b % r ∧ b % r ≤ v % r

Proof state:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ v % r < r + b % r ∧ b % r ≤ v % r

Tactic:
exact ⟨(mod_lt _ hr).trans_le (by simp), not_lt.mp h⟩

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Tactic:
rw [add_right_inj]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ r ≤ r + v % r

Tactic:
simp

Result:
no goals

Proof state:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑1

Tactic:
rw [← cast_sub h.le, Int.ceil_eq_iff, div_le_iff₀ hr', lt_div_iff₀ hr', cast_one, Int.cast_one,
  sub_self, zero_mul, cast_pos, tsub_pos_iff_lt, one_mul, cast_le, tsub_le_iff_right]

Result:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ b % r ≤ r + v % r

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(if v % r < b % r then 1 else 0)

Tactic:
split_ifs with h

Result:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑1

case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ 0 < ↑r

Tactic:
positivity

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ r ≤ r + b % r

Tactic:
simp

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Tactic:
conv_lhs => rw [← div_add_mod b r, cast_add, cast_mul, ← add_sub, _root_.add_div,
  mul_div_cancel_left₀ _ hr'.ne', add_comm, Int.ceil_add_nat, add_comm]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(b / r) + ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑(b / r) + ↑(if v % r < b % r then 1 else 0)

Proof state:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ b % r ≤ r + v % r

Tactic:
exact ⟨h, ((mod_lt _ hr).trans_le (by simp)).le⟩

Result:
no goals