awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
y : ℕ
h : (a < y ∧ y ≤ b) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
c : (↑y : ℤ) = x
⊢ ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
have h₁ : (LT.lt (α := ℤ) (↑a : ℤ) (↑y : ℤ) ∧ LE.le (α := ℤ) (↑y : ℤ) (↑b : ℤ)) ∧ (↑y : ℤ) ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
Tactic: subst c
Cleared hypotheses: x, c
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r v : ℕ
x : ℤ
h : ((↑a : ℤ) < x ∧ x ≤ (↑b : ℤ)) ∧ x ≡ (↑v : ℤ) [ZMOD (↑r : ℤ)]
⊢ ∃ (a_1 : ℕ), ((a < a_1 ∧ a_1 ≤ b) ∧ a_1 ≡ v [MOD r]) ∧ (↑a_1 : ℤ) = x
have 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 : ℤ)
Tactic: lift x to ℕ using (by lia)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℕ
hr : 0 < r
v : ℕ
⊢ (↑(#({x ∈ Ico a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0
have simp_rw : (↑(card (α := ℤ) ({x ∈ Ico (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑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]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
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
⊢ (↑(#({x ∈ Ico a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉) 0
have 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
Tactic: simp_rw [← Ico_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ico_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
a b r : ℕ
hr : 0 < r
v : ℕ
⊢ (↑(#({x ∈ Ioc a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0
have simp_rw : (↑(card (α := ℤ) ({x ∈ Ioc (↑a : ℤ) (↑b : ℤ) | x ≡ (↑v : ℤ) [ZMOD (↑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]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
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
⊢ (↑(#({x ∈ Ioc a b | x ≡ v [MOD r]})) : ℤ) =
    max (⌊HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋ - ⌊HSub.hSub (α := ℚ) (↑a : ℚ) (↑v : ℚ) / (↑r : ℚ)⌋) 0
have 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
Tactic: simp_rw [← Ioc_filter_modEq_cast _ _ ▸ card_map _,
    Int.Ioc_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (hypothesis)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ (↑(count (fun (x : ℕ) ↦ x ≡ v [MOD r]) b) : ℤ) = ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
have hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
Tactic: have hr' : 0 < (r : ℚ) := by positivity
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ ≤ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉
have hab : 0 ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ (↑(count (fun (x : ℕ) ↦ x ≡ v [MOD r]) b) : ℤ) = ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
have rw : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ =
  ⌈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)]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉
have rw : ⌈((↑b : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ -
  ⌈((↑0 : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉
Tactic: rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑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 : ℚ)⌉
have 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 : ℚ)⌉
Tactic: simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
| ⌈((↑b : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉ -
    ⌈((↑0 : ℚ) - ((↑(v % r) : ℚ) + HMul.hMul (α := ℚ) (↑r : ℚ) (↑(v / r) : ℚ))) / (↑r : ℚ)⌉
have tactic : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ) -
  (⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ))
Tactic: tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ) -
    (⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - (↑(v / r) : ℤ))
have rw : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉
Tactic: rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉
have rw : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉
Tactic: rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
    tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
    rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
have conv_lhs : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉ =
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
Tactic: conv_lhs =>
    rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
    tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne',
      Int.ceil_sub_natCast]
    rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
have rw : v % r < r ∧ LE.le (α := ℚ) (-(↑(v % r) : ℚ)) 0
Tactic: rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', neg_one_mul,
    zero_mul, neg_lt_neg_iff, cast_lt]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (hypothesis)
Goal:
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
have hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
Tactic: have hr' : 0 < (r : ℚ) := by positivity
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ count (fun (x : ℕ) ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
have rw : ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ =
  HAdd.hAdd (α := ℤ) (↑(b / r) : ℤ) (↑(if v % r < b % r then 1 else 0) : ℤ)
Tactic: rw [← ofNat_inj, count_modEq_card_eq_ceil _ hr, cast_add]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
have rw : (↑(b / r) : ℤ) + ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
Tactic: 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_natCast, add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ (↑(b / r) : ℤ) + ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ =
    HAdd.hAdd (α := ℤ) (↑(b / r) : ℤ) (↑(if v % r < b % r then 1 else 0) : ℤ)
have rw : ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑(if v % r < b % r then 1 else 0) : ℤ)
Tactic: rw [add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑(if v % r < b % r then 1 else 0) : ℤ)
have pos : ∀ (h : v % r < b % r), ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑1 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
pos : ∀ (h : v % r < b % r), ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑1 : ℤ)
⊢ ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑(if v % r < b % r then 1 else 0) : ℤ)
have neg : ∀ (h : ¬v % r < b % r), ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑0 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : v % r < b % r
⊢ ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑1 : ℤ)
have pos : v % r < b % r ∧ b % r ≤ r + v % r
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]
-- Lean 4 proof step from Mathlib.Data.Int.CardIntervalMod (goal)
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : ¬v % r < b % r
⊢ ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑0 : ℤ)
have neg : v % r < r + b % r ∧ b % r ≤ v % r
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]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ HAdd.hAdd (α := R) (↑(n - m) : R) (↑m : R) = (↑n : R)
have rw : Eq.{u + 1} (α := R) (↑(n - m + m) : R) (↑n : R)
Tactic: rw [← cast_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
h : m ≤ n
rw : Eq.{u + 1} (α := R) (↑(n - m + m) : R) (↑n : R)
⊢ HAdd.hAdd (α := R) (↑(n - m) : R) (↑m : R) = (↑n : R)
have rw₁ : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
Tactic: rw [← cast_add, Nat.sub_add_cancel h]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
h : 0 < n + 1
⊢ (↑(n + 1 - 1) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have rw : (↑(n + 1 - 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1 - 1
Tactic: rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
h : 0 < n + 1
rw : (↑(n + 1 - 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1 - 1
⊢ (↑(n + 1 - 1) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have rw₁ : Eq.{u + 1} (α := R) (↑(n + 1 - 1) : R) (↑n : R)
Tactic: rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
h : 0 < n + 1
rw : (↑(n + 1 - 1) : R) = HAdd.hAdd (α := R) (↑n : R) 1 - 1
rw₁ : Eq.{u + 1} (α := R) (↑(n + 1 - 1) : R) (↑n : R)
⊢ (↑(n + 1 - 1) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1
have rw₂ : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
Tactic: rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑1 : R) 1
have rw : Eq.{u + 1} (α := R) (↑(↑1 : ℤ) : R) 1
Tactic: rw [← Int.natCast_one, cast_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
rw : Eq.{u + 1} (α := R) (↑(↑1 : ℤ) : R) 1
⊢ Eq.{u + 1} (α := R) (↑1 : R) 1
have rw₁ : Eq.{u + 1} (α := R) (↑1 : R) 1
Tactic: rw [← Int.natCast_one, cast_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
rw : Eq.{u + 1} (α := R) (↑(↑1 : ℤ) : R) 1
rw₁ : Eq.{u + 1} (α := R) (↑1 : R) 1
⊢ Eq.{u + 1} (α := R) (↑1 : R) 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [← Int.natCast_one, cast_natCast, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(-(↑(n + 1) : ℤ)) : R) (-(↑(↑(n + 1) : ℤ) : R))
have rw : Eq.{u + 1} (α := R) (↑-[n+1] : R) (-(↑(n + 1) : R))
Tactic: rw [cast_natCast, neg_ofNat_succ]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(- -[n+1]) : R) (-(↑-[n+1] : R))
have rw : Eq.{u + 1} (α := R) (↑(n + 1) : R) (-(↑-[n+1] : R))
Tactic: rw [Int.neg_negSucc, cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑(subNatNat m n) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
have unfold : (↑(match (motive := ℕ → ℤ) n - m with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) :
    R) =
  HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: unfold subNatNat
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑(match (motive := ℕ → ℤ) n - m with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have zero : ∀ (e : n - m = 0),
  (↑(match (motive := ℕ → ℤ) 0 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: cases e : n - m
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
zero :
  ∀ (e : n - m = 0),
    (↑(match (motive := ℕ → ℤ) 0 with
          | 0 => ofNat (m - n)
          | k.succ => -[k+1]) :
        R) =
      HSub.hSub (α := R) (↑m : R) (↑n : R)
⊢ (↑(match (motive := ℕ → ℤ) n - m with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have succ : ∀ (n_1 : ℕ) (e : n - m = n_1 + 1),
  (↑(match (motive := ℕ → ℤ) n_1 + 1 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: cases e : n - m
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n n_1 : ℕ
e : n - m = n_1 + 1
⊢ (↑(match (motive := ℕ → ℤ) n_1 + 1 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have succ : -(↑(n_1 + 1) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n n_1 : ℕ
e : n - m = n_1 + 1
succ : -(↑(n_1 + 1) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
⊢ (↑(match (motive := ℕ → ℤ) n_1 + 1 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have succ₁ : -(↑(n - m) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n n_1 : ℕ
e : n - m = n_1 + 1
succ : -(↑(n_1 + 1) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
succ₁ : -(↑(n - m) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
⊢ (↑(match (motive := ℕ → ℤ) n_1 + 1 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have succ₂ : -HSub.hSub (α := R) (↑n : R) (↑m : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n n_1 : ℕ
e : n - m = n_1 + 1
succ : -(↑(n_1 + 1) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
succ₁ : -(↑(n - m) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
succ₂ : -HSub.hSub (α := R) (↑n : R) (↑m : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
⊢ (↑(match (motive := ℕ → ℤ) n_1 + 1 with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
have succ₃ : HSub.hSub (α := R) (↑m : R) (↑n : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)
Tactic: rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑((↑m : ℤ) + -[n+1]) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
have rw : (↑(subNatNat m n.succ) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
Tactic: rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat m n.succ) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
⊢ (↑((↑m : ℤ) + -[n+1]) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
have rw₁ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
Tactic: rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat m n.succ) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
rw₁ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
⊢ (↑((↑m : ℤ) + -[n+1]) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
have rw₂ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑-[n+1] : R)
Tactic: rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat m n.succ) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
rw₁ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
rw₂ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑-[n+1] : R)
⊢ (↑((↑m : ℤ) + -[n+1]) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
have rw₃ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑m : R) (-(↑(n + 1) : R))
Tactic: rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat m n.succ) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
rw₁ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
rw₂ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑m : R) (↑-[n+1] : R)
rw₃ : HSub.hSub (α := R) (↑m : R) (↑n.succ : R) = HAdd.hAdd (α := R) (↑m : R) (-(↑(n + 1) : R))
⊢ (↑((↑m : ℤ) + -[n+1]) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑-[n+1] : R)
have rw₄ : HAdd.hAdd (α := R) (↑m : R) (-(↑n.succ : R)) = HAdd.hAdd (α := R) (↑m : R) (-(↑(n + 1) : R))
Tactic: rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Int.Cast.Basic (goal)
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑(subNatNat n m.succ) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
rw₁ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑(↑n : ℤ) : R)
have rw₂ : HSub.hSub (α := R) (↑n : R) (↑m.succ : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑n : R)
Tactic: rw [Int.negSucc_add_ofNat, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_iff_eq_add,
      add_assoc, eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]