awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ico a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ico (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
h₅ : (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₆ : (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₇ : (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
h₈ : (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x < b) ∧ r ∣ x - v
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

Premises used: Int.modEq_iff_dvd, eq_sub_iff_add_eq, Int.modEq_comm, exists_eq_right, sub_le_sub_iff_right, sub_lt_sub_iff_right, Function.Embedding.coeFn_mk, Finset.mem_filter, Finset.mem_map, Finset.mem_Ico
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℤ
h :
  ∀ (x : ℤ),
    x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
      x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})
⊢ {x ∈ Ioc a b | x ≡ v [ZMOD r]} =
    map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
ext x
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℤ
h :
  x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ioc (a - v) (b - v) | r ∣ x},
      ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₁ :
  x ∈ Ioc a b ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      (a_1 ∈ Ioc (a - v) (b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₂ :
  (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔
    ∃ (a_1 : ℤ),
      ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧
        ({ toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
h₃ : (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
h₄ : (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ ∃ (a_1 : ℤ), ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ a_1 = x - v
h₅ : (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v
h₆ : (a < x ∧ x ≤ b) ∧ v ≡ x [ZMOD r] ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v
h₇ : (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v
h₈ : (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a < x ∧ x - v ≤ b - v) ∧ r ∣ x - v
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    x ∈ map { toFun := fun (x : ℤ) ↦ x + v, inj' := ⋯ : ℤ ↪ ℤ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

Premises used: Int.modEq_iff_dvd, eq_sub_iff_add_eq, Int.modEq_comm, exists_eq_right, sub_le_sub_iff_right, sub_lt_sub_iff_right, Function.Embedding.coeFn_mk, Finset.mem_filter, Finset.mem_Ioc, Finset.mem_map
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
h :
  ∀ (x : ℤ),
    x ∈ {x ∈ Ico a b | r ∣ x} ↔
      x ∈
        map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
          (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)
⊢ {x ∈ Ico a b | r ∣ x} =
    map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
      (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)

Tactic:
ext x
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
h :
  ((a ≤ x ∧ x < b) ∧ ∃ (c : ℤ), x = c * r) ↔
    ∃ (a_1 : ℤ),
      (a ≤ a_1 * r ∧ a_1 * r < b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ico a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
        (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)

Tactic:
simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Premises used: Iff.mpr, Int.lt_ceil, div_le_iff₀, Int.cast_le, lt_div_iff₀, Int.cast_lt, Int.cast_mul, Int.ceil_le, Finset.mem_filter, Finset.mem_map, dvd_iff_exists_eq_mul_left, Int.cast_pos, Finset.mem_Ico
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a ≤ x ∧ x < b) ∧ ∃ (c : ℤ), x = c * r) ↔
    ∃ (a_1 : ℤ),
      (a ≤ a_1 * r ∧ a_1 * r < b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x

Tactic:
aesop
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
h :
  ∀ (x : ℤ),
    x ∈ {x ∈ Ioc a b | r ∣ x} ↔
      x ∈
        map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
          (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)
⊢ {x ∈ Ioc a b | r ∣ x} =
    map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
      (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)

Tactic:
ext x
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
h :
  ((a < x ∧ x ≤ b) ∧ ∃ (c : ℤ), x = c * r) ↔
    ∃ (a_1 : ℤ),
      (a < a_1 * r ∧ a_1 * r ≤ b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x
⊢ x ∈ {x ∈ Ioc a b | r ∣ x} ↔
    x ∈
      map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
        (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀,
    dvd_iff_exists_eq_mul_left, cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]

Premises used: Iff.mpr, Int.cast_le, Int.floor_lt, Int.cast_lt, div_lt_iff₀, Int.cast_mul, Int.le_floor, Finset.mem_filter, Finset.mem_Ioc, Finset.mem_map, le_div_iff₀, dvd_iff_exists_eq_mul_left, Int.cast_pos
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a < x ∧ x ≤ b) ∧ ∃ (c : ℤ), x = c * r) ↔
    ∃ (a_1 : ℤ),
      (a < a_1 * r ∧ a_1 * r ≤ b) ∧ ({ toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ } : (a : ℤ) → ℤ) a_1 = x

Tactic:
aesop
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉))) :
      ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₁ :
  (↑(#(Ico ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉ ⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉)) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₂ :
  (↑(⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉).toNat : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
rw₃ rw₄ :
  max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0 =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0
⊢ (↑(#({x ∈ Ico a b | r ∣ x})) : ℤ) =
    max (⌈HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌉) 0

Tactic:
rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]

Premises used: Finset.card_map, Int.card_Ico, Int.toNat_eq_max, Int.Ico_filter_dvd_eq
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
rw :
  (↑(#(map { toFun := fun (x : ℤ) ↦ x * r, inj' := ⋯ : ℤ ↪ ℤ }
            (Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋))) :
      ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₁ :
  (↑(#(Ioc ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋ ⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋)) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₂ :
  (↑(⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋).toNat : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
rw₃ rw₄ :
  max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0 =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0
⊢ (↑(#({x ∈ Ioc a b | r ∣ x})) : ℤ) =
    max (⌊HDiv.hDiv (α := ℚ) (↑b : ℚ) (↑r : ℚ)⌋ - ⌊HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑r : ℚ)⌋) 0

Tactic:
rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]

Premises used: Finset.card_map, Int.card_Ioc, Int.toNat_eq_max, Int.Ioc_filter_dvd_eq
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
v : ℤ
⊢ (↑(#({x ∈ Ico a b | x ≡ v [ZMOD r]})) : ℤ) =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0

Tactic:
simp [Ico_filter_modEq_eq, Ico_filter_dvd_eq, hr]

Premises used: Int.Ico_filter_modEq_eq, Int.Ico_filter_dvd_eq
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℤ
hr : 0 < r
v : ℤ
⊢ (↑(#({x ∈ Ioc a b | x ≡ v [ZMOD r]})) : ℤ) =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0

Tactic:
simp [Ioc_filter_modEq_eq, Ioc_filter_dvd_eq, hr]

Premises used: Int.Ioc_filter_dvd_eq, Int.Ioc_filter_modEq_eq
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
h :
  ∀ (x : ℤ),
    Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]})) x ↔
      Membership.mem (γ := Finset ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
⊢ Eq (α := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]}))
    ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})

Tactic:
ext x
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ico a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x

Tactic:
simp only [mem_map, mem_filter, mem_Ico, castEmbedding_apply]

Premises used: Nat.castEmbedding_apply, Finset.mem_filter, Finset.mem_map, Finset.mem_Ico
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
h₁ :
  ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)] →
    ∃ (a_2 : ℕ), ((a ≤ a_2 ∧ a_2 < b) ∧ a_2 ≡ v [MOD r]) ∧ (↑a_2 : ℤ) = x
⊢ (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
constructor
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  ∀ (x_1 : ℕ) (h : ((a ≤ x_1 ∧ x_1 < b) ∧ (↑x_1 : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑x_1 : ℤ) = x),
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff, forall_exists_index
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h :
  ∀ (h : (a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) (c : (↑y : ℤ) = x),
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∀ (h : ((a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑y : ℤ) = x),
    ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
⟨h, c⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h : (a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
c : (↑y : ℤ) = x
h₁ : (LE.le (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LT.lt (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
subst c
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v y : ℕ
h : (a ≤ y ∧ y < b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (LE.le (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LT.lt (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
exact_mod_cast h
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ 0 ≤ x

Tactic:
omega
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) ≤ x ∧ x < (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
h₁ :
  ∀ (x : ℕ)
    (h : (LE.le (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LT.lt (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]),
    ∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑a_1 : ℤ) (↑x : ℤ)
⊢ ∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x

Tactic:
lift x to ℕ using (by omega)
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℕ
h : (LE.le (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LT.lt (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ((a ≤ x ∧ x < b) ∧ x ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑x : ℤ) (↑x : ℤ)

Tactic:
simp_all [natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℕ
h : (LE.le (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LT.lt (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∃ (a_1 : ℕ), ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑a_1 : ℤ) (↑x : ℤ)

Tactic:
exact ⟨x, by simp_all [natCast_modEq_iff]⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
h :
  ∀ (x : ℤ),
    Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]})) x ↔
      Membership.mem (γ := Finset ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x
⊢ Eq (α := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]}))
    ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})

Tactic:
ext x
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ Membership.mem (γ := Finset ℤ) (map castEmbedding ({x ∈ Ioc a b | x ≡ v [MOD r]})) x ↔
    Membership.mem (γ := Finset ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]}) x

Tactic:
simp only [mem_map, mem_filter, mem_Ioc, castEmbedding_apply]

Premises used: Nat.castEmbedding_apply, Finset.mem_filter, Finset.mem_Ioc, Finset.mem_map
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
h₁ :
  ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)] →
    ∃ (a_2 : ℕ), ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ (↑a_2 : ℤ) = x
⊢ (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) ↔
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
constructor
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h :
  ∀ (x_1 : ℕ) (h : ((a < x_1 ∧ x_1 ≤ b) ∧ (↑x_1 : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑x_1 : ℤ) = x),
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x) →
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
simp_rw [forall_exists_index, ← natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff, forall_exists_index
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h :
  ∀ (h : (a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) (c : (↑y : ℤ) = x),
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∀ (h : ((a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]) ∧ (↑y : ℤ) = x),
    ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
⟨h, c⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
c : (↑y : ℤ) = x
h₁ : (LT.lt (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LE.le (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
subst c
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v y : ℕ
h : (a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ (LT.lt (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LE.le (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]

Tactic:
exact_mod_cast h
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ 0 ≤ x

Tactic:
lia
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
h₁ :
  ∀ (x : ℕ)
    (h : (LT.lt (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LE.le (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]),
    ∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑a_1 : ℤ) (↑x : ℤ)
⊢ ∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x

Tactic:
lift x to ℕ using (by lia)
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℕ
h : (LT.lt (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LE.le (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ((a < x ∧ x ≤ b) ∧ x ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑x : ℤ) (↑x : ℤ)

Tactic:
simp_all [natCast_modEq_iff]

Premises used: Int.natCast_modEq_iff
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r v x : ℕ
h : (LT.lt (α := ℤ) (↑a : ℤ) (↑x : ℤ) ∧ LE.le (α := ℤ) (↑x : ℤ) (↑b : ℤ)) ∧ (↑x : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ Eq (α := ℤ) (↑a_1 : ℤ) (↑x : ℤ)

Tactic:
exact ⟨x, by simp_all [natCast_modEq_iff]⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℕ
hr : 0 < r
v : ℕ
simp_rw :
  (↑(card (α := ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})) : ℤ) =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0
simp_rw₁ :
  max
      (⌈HSub.hSub (α := ℚ) (↑(↑b : ℤ) : ℚ) (↑(↑v : ℤ) : ℚ) / (↑(↑r : ℤ) : ℚ)⌉ -
        ⌈HSub.hSub (α := ℚ) (↑(↑a : ℤ) : ℚ) (↑(↑v : ℤ) : ℚ) / (↑(↑r : ℤ) : ℚ)⌉)
      0 =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0
⊢ (↑(#({x ∈ Ico a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0

Tactic:
simp_rw [← Ico_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ico_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.Ico_filter_modEq_card, Nat.cast_lt
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
a b r : ℕ
hr : 0 < r
v : ℕ
simp_rw :
  (↑(card (α := ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]})) : ℤ) =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0
simp_rw₁ :
  max
      (⌊HSub.hSub (α := ℚ) (↑(↑b : ℤ) : ℚ) (↑(↑v : ℤ) : ℚ) / (↑(↑r : ℤ) : ℚ)⌋ -
        ⌊HSub.hSub (α := ℚ) (↑(↑a : ℤ) : ℚ) (↑(↑v : ℤ) : ℚ) / (↑(↑r : ℤ) : ℚ)⌋)
      0 =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0
⊢ (↑(#({x ∈ Ioc a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0

Tactic:
simp_rw [← Ioc_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ioc_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

Premises used: Iff.mpr, Int.cast_natCast, Int.Ioc_filter_modEq_card, Nat.cast_lt
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ LT.lt (α := ℚ) 0 (↑r : ℚ)

Tactic:
positivity
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ LT.lt (α := ℚ) 0 (↑r : ℚ)

Tactic:
have hr' : 0 < (r : ℚ) := by positivity
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
hab : 0 ≤ b
⊢ ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ ≤ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉

Tactic:
gcongr
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ 0 ≤ b

Tactic:
positivity
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw :
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
⊢ (↑(count (fun (x : ℕ) ↦ x ≡ v [MOD r]) b) : ℤ) = ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉

Tactic:
rw [count_eq_card_filter_range, ← Ico_zero_eq_range, Ico_filter_modEq_card _ _ hr,
    max_eq_left (sub_nonneg.mpr <| by gcongr; positivity)]

Premises used: Iff.mpr, Nat.count_eq_card_filter_range, max_eq_left, Nat.Ico_filter_modEq_card, Nat.Ico_zero_eq_range, sub_nonneg
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw :
  ⌈((↑b : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ -
    ⌈((↑0 : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉

Tactic:
rw [← div_add_mod v r, cast_add, cast_mul, add_comm]

Premises used: Nat.div_add_mod, add_comm, Nat.cast_add, Nat.cast_mul
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
simp_rw :
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ) -
      (⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ)) =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉
⊢ ⌈((↑b : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ -
      ⌈((↑0 : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉

Tactic:
simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]

Premises used: HSub.hSub, Int.ceil_sub_natCast, mul_div_cancel_left₀, sub_div, LT.lt.ne', sub_sub
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
tactic :
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ) -
    (⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ))
| ⌈((↑b : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ -
    ⌈((↑0 : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉

Tactic:
tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]

Premises used: HSub.hSub, Int.ceil_sub_natCast, mul_div_cancel_left₀, sub_div, LT.lt.ne', sub_sub
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ) -
    (⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ))

Tactic:
rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]

Premises used: sub_sub_sub_cancel_right, Nat.cast_zero, zero_sub