Fastest way to prove this

Stream: Is there code for X?

[Jeremy Tan]

What's the fastest way to prove this?

import Mathlib.Data.Fintype.Card

variable {n r v : ℕ} (hr : 0 < r)

theorem vvv : Fintype.card { x : Fin n // v % r = x % r } =
    n / r + if v % r < n % r then 1 else 0 := by
  simp

The theorem looks so simple but apparently there's no theorem in the library for it.

[Yaël Dillies]

This is weirdly stated. Try ((Finset.range n).filter (· ≡ v [MOD n])).card instead.

[Jeremy Tan]

Or even

import Mathlib.Data.Nat.ModEq
import Mathlib.Data.Nat.Count

variable {n r v : ℕ} (hr : 0 < r)

theorem vvv : n.count (· ≡ v [MOD r]) =
    n / r + if v % r < n % r then 1 else 0 := by
  sorry

[Jeremy Tan]

This is what I should be proving

import Mathlib.Data.Int.ModEq
import Mathlib.Data.Int.Interval
import Mathlib.Algebra.Order.Floor

variable {a b r : ℤ}

theorem filter_Ico_modEq_card (hr : 0 < r) :
    ((Finset.Ico a b).filter (· ≡ 0 [ZMOD r])).card = max (⌈b / r⌉ - ⌈a / r⌉) 0 := by
  sorry

[Jeremy Tan]

OK, I proved it. Can you make the proof shorter?

import Mathlib.Data.Int.Interval
import Mathlib.Data.Rat.Floor
import Mathlib.Tactic.Qify

open Finset

-- ⌈(n - v) / r⌉

def remb {r : ℤ} (hr : 0 < r) : ℤ ↪ ℤ where
  toFun x := x * r
  inj' := mul_left_injective₀ hr.ne.symm

theorem Ico_map_eq_Ico_filter (a b : ℤ) {r : ℤ} (hr : 0 < r) :
    (Ico ⌈a / (r : ℚ)⌉ ⌈b / (r : ℚ)⌉).map (remb hr) = (Ico a b).filter (r ∣ ·) := by
  ext x
  constructor
  · simp only [mem_map, mem_Ico, mem_filter, forall_exists_index, and_imp]
    intro d lb ub p
    rw [remb, Function.Embedding.coeFn_mk] at p
    qify at lb hr
    replace lb := (div_le_iff hr).mp ((Int.le_ceil _).trans lb)
    norm_cast at lb
    rw [p] at lb
    refine' ⟨⟨lb, _⟩, Dvd.intro_left d p⟩
    contrapose! ub
    rw [← p] at ub
    qify at ub
    exact Int.ceil_le.mpr ((div_le_iff hr).mpr ub)
  · simp only [mem_filter, mem_Ico, mem_map, and_imp]
    intro lb ub v
    rw [dvd_def] at v
    obtain ⟨d, p⟩ := v
    use d
    rw [mul_comm] at p
    rw [remb, Function.Embedding.coeFn_mk]
    subst p; qify at lb hr
    refine' ⟨⟨Int.ceil_le.mpr ((div_le_iff hr).mpr lb), _⟩, rfl⟩
    contrapose! ub
    exact_mod_cast (div_le_iff hr).mp (Int.ceil_le.mp ub)

theorem filter_Ico_dvd_card (a b : ℤ) {r : ℤ} (hr : 0 < r) :
    ((Ico a b).filter (r ∣ ·)).card = max (⌈b / (r : ℚ)⌉ - ⌈a / (r : ℚ)⌉) 0 := by
  rw [← Ico_map_eq_Ico_filter a b hr, card_map, Int.card_Ico, Int.toNat_eq_max]

[Jeremy Tan]

#9348

[Kevin Buzzard]

docs#dvd_def

[Kevin Buzzard]

That's true by definition so you can rintro lb ub \<d,p\> at the beginning of the second case

[Eric Wieser]

Your remb already exists