awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑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]

Premises used: sub_sub_sub_cancel_right, Nat.div_add_mod, HSub.hSub, Int.ceil_sub_natCast, mul_div_cancel_left₀, sub_div, add_comm, LT.lt.ne', Nat.cast_add, sub_sub, Nat.cast_mul, Nat.cast_zero, zero_sub
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
conv_lhs :
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
⊢ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑v : ℚ) / (↑r : ℚ)⌉ - ⌈HSub.hSub (α := ℚ) (↑0 : ℚ) (↑v : ℚ) / (↑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]

Premises used: sub_sub_sub_cancel_right, Nat.div_add_mod, HSub.hSub, Int.ceil_sub_natCast, mul_div_cancel_left₀, sub_div, add_comm, LT.lt.ne', Nat.cast_add, sub_sub, Nat.cast_mul, Nat.cast_zero, zero_sub
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw : v % r < r ∧ LE.le (α := ℚ) (-(↑(v % r) : ℚ)) 0
⊢ ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ - ⌈HDiv.hDiv (α := ℚ) (-(↑(v % r) : ℚ)) (↑r : ℚ)⌉ =
    ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉

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]

Premises used: div_le_iff₀, neg_lt_neg_iff, lt_div_iff₀, MulZeroClass.zero_mul, neg_one_mul, Int.ceil_eq_zero_iff, sub_eq_self, Set.mem_Ioc, Nat.cast_lt
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ LE.le (α := ℚ) (-(↑(v % r) : ℚ)) 0

Tactic:
simp
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
⊢ v % r < r ∧ LE.le (α := ℚ) (-(↑(v % r) : ℚ)) 0

Tactic:
exact ⟨mod_lt _ hr, by simp⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw :
  ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ =
    HAdd.hAdd (α := ℤ) (↑(b / r) : ℤ) (↑(if v % r < b % r then 1 else 0) : ℤ)
⊢ 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]

Premises used: Int.ofNat_inj, Nat.cast_add, Nat.count_modEq_card_eq_ceil
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw : (↑(b / r) : ℤ) + ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉
| ⌈HSub.hSub (α := ℚ) (↑b : ℚ) (↑(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]

Premises used: add_sub, Nat.div_add_mod, mul_div_cancel_left₀, Int.ceil_add_natCast, add_comm, LT.lt.ne', Nat.cast_add, Nat.cast_mul, add_div
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
rw : ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑(if v % r < b % r then 1 else 0) : ℤ)
⊢ (↑(b / r) : ℤ) + ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ =
    HAdd.hAdd (α := ℤ) (↑(b / r) : ℤ) (↑(if v % r < b % r then 1 else 0) : ℤ)

Tactic:
rw [add_right_inj]

Premises used: add_right_inj
-- Module: Mathlib.Data.Int.CardIntervalMod
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 : ℤ)
neg : ∀ (h : ¬v % r < b % r), ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑0 : ℤ)
⊢ ⌈HSub.hSub (α := ℚ) (↑(b % r) : ℚ) (↑(v % r) : ℚ) / (↑r : ℚ)⌉ = (↑(if v % r < b % r then 1 else 0) : ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : v % r < b % r
pos : v % r < b % r ∧ b % r ≤ r + v % r
⊢ ⌈HSub.hSub (α := ℚ) (↑(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]

Premises used: div_le_iff₀, Nat.cast_pos, sub_self, tsub_pos_iff_lt, Nat.cast_sub, lt_div_iff₀, MulZeroClass.zero_mul, Int.ceil_eq_iff, LT.lt.le, tsub_le_iff_right, Nat.cast_le, Nat.cast_one, one_mul, Int.cast_one
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : v % r < b % r
⊢ r ≤ r + v % r

Tactic:
simp
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 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⟩
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : ¬v % r < b % r
neg : v % r < r + b % r ∧ b % r ≤ v % r
⊢ ⌈HSub.hSub (α := ℚ) (↑(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]

Premises used: div_le_iff₀, tsub_nonpos, lt_div_iff₀, neg_lt_sub_iff_lt_add, MulZeroClass.zero_mul, Int.ceil_eq_zero_iff, Nat.cast_add, neg_eq_neg_one_mul, Set.mem_Ioc, Nat.cast_zero, Nat.cast_le, Nat.cast_lt
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 0 (↑r : ℚ)
h : ¬v % r < b % r
⊢ r ≤ r + b % r

Tactic:
simp
-- Module: Mathlib.Data.Int.CardIntervalMod
Goal:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : LT.lt (α := ℚ) 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⟩
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
h : m ≤ n
rw : Eq.{u + 1} (α := R) (↑(n - m + m) : R) (↑n : R)
rw₁ rw₂ : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
⊢ HAdd.hAdd (α := R) (↑(n - m) : R) (↑m : R) = (↑n : R)

Tactic:
rw [← cast_add, Nat.sub_add_cancel h]

Premises used: Nat.cast_add, Nat.sub_add_cancel
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
h : LT.lt (α := ℕ) 0 0
⊢ (↑(HSub.hSub (α := ℕ) 0 1) : R) = HSub.hSub (α := R) (↑0 : R) 1

Tactic:
cases h
-- Module: Mathlib.Data.Int.Cast.Basic
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)
rw₂ rw₃ : Eq.{u + 1} (α := R) (↑n : R) (↑n : R)
⊢ (↑(n + 1 - 1) : R) = HSub.hSub (α := R) (↑(n + 1) : R) 1

Tactic:
rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]

Premises used: Nat.cast_succ, Nat.add_sub_cancel_right, add_sub_cancel_right
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : IntCast R
P : Prop
inst_1 : Decidable P
m n : ℤ
⊢ Eq.{u + 1} (α := R) (↑(if P then m else n) : R) (if P then (↑m : R) else (↑n : R))

Tactic:
apply_ite _ _ _ _

Premises used: apply_ite
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑-[n+1] : R) (-(↑(n + 1) : R))

Tactic:
AddGroupWithOne.intCast_negSucc n

Premises used: AddGroupWithOne.intCast_negSucc
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑0 : R) 0

Tactic:
(AddGroupWithOne.intCast_ofNat 0).trans Nat.cast_zero

Premises used: Nat.cast_zero, AddGroupWithOne.intCast_ofNat, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(↑n : ℤ) : R) (↑n : R)

Tactic:
AddGroupWithOne.intCast_ofNat _

Premises used: AddGroupWithOne.intCast_ofNat
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (↑(OfNat.ofNat n) : R) (OfNat.ofNat n)

Tactic:
simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n

Premises used: AddGroupWithOne.intCast_ofNat, OfNat.ofNat
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
rw : Eq.{u + 1} (α := R) (↑(↑1 : ℤ) : R) 1
rw₁ : Eq.{u + 1} (α := R) (↑1 : R) 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) (↑1 : R) 1

Tactic:
rw [← Int.natCast_one, cast_natCast, Nat.cast_one]

Premises used: Int.cast_natCast, Int.natCast_one, Nat.cast_one
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑(-(↑0 : ℤ)) : R) (-(↑(↑0 : ℤ) : R))

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
rw : Eq.{u + 1} (α := R) (↑-[n+1] : R) (-(↑(n + 1) : R))
⊢ Eq.{u + 1} (α := R) (↑(-(↑(n + 1) : ℤ)) : R) (-(↑(↑(n + 1) : ℤ) : R))

Tactic:
rw [cast_natCast, neg_ofNat_succ]

Premises used: Int.cast_natCast, Int.neg_ofNat_succ
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑-[n+1] : R) (-(↑(n + 1) : R))

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
rw : Eq.{u + 1} (α := R) (↑(n + 1) : R) (-(↑-[n+1] : R))
⊢ Eq.{u + 1} (α := R) (↑(- -[n+1]) : R) (-(↑-[n+1] : R))

Tactic:
rw [Int.neg_negSucc, cast_natCast]

Premises used: Int.cast_natCast, Int.neg_negSucc
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(n + 1) : R) (-(↑-[n+1] : R))

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
unfold :
  (↑(match (motive := ℕ → ℤ) n - m with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)
⊢ (↑(subNatNat m n) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)

Tactic:
unfold subNatNat

Premises used: Int.subNatNat
-- Module: Mathlib.Data.Int.Cast.Basic
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)
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)
⊢ (↑(match (motive := ℕ → ℤ) n - m with
        | 0 => ofNat (m - n)
        | k.succ => -[k+1]) :
      R) =
    HSub.hSub (α := R) (↑m : R) (↑n : R)

Tactic:
cases e : n - m
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
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:
simp [Nat.le_of_sub_eq_zero e]

Premises used: Nat.le_of_sub_eq_zero
-- Module: Mathlib.Data.Int.Cast.Basic
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)
succ₃ succ₄ : HSub.hSub (α := R) (↑m : R) (↑n : 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)

Tactic:
rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

Premises used: neg_sub, Nat.cast_sub, le_of_lt, Int.cast_negSucc, Nat.lt_of_sub_eq_succ
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
n : ℕ
⊢ Eq.{u + 1} (α := R) (↑(negOfNat n) : R) (-(↑n : R))

Tactic:
simp [Int.cast_neg, negOfNat_eq]

Premises used: Int.cast_neg, Int.negOfNat_eq
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
⊢ (↑(HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : R) = HAdd.hAdd (α := R) (↑(↑m : ℤ) : R) (↑(↑n : ℤ) : R)

Tactic:
simp [← Int.natCast_add]

Premises used: Int.natCast_add
-- Module: Mathlib.Data.Int.Cast.Basic
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))
rw₄ rw₅ : HAdd.hAdd (α := 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)

Tactic:
rw [Int.ofNat_add_negSucc, cast_subNatNat, cast_natCast, cast_negSucc, sub_eq_add_neg]

Premises used: Int.cast_natCast, sub_eq_add_neg, Int.cast_negSucc, Int.ofNat_add_negSucc, Int.cast_subNatNat
-- Module: Mathlib.Data.Int.Cast.Basic
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)
rw₂ : HSub.hSub (α := R) (↑n : R) (↑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)
rw₄ : (↑n : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑n : R) + (↑m.succ : R)
rw₅ : (↑n : R) = -(↑(m + 1) : R) + HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₆ : HAdd.hAdd (α := R) (↑(m + 1) : R) (↑n : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₇ : (↑(m + 1 + n) : R) = HAdd.hAdd (α := R) (↑n : R) (↑m.succ : R)
rw₈ : Eq.{u + 1} (α := R) (↑(m + 1 + n) : R) (↑(n + m.succ) : R)
rw₉ rw₁₀ : Eq.{u + 1} (α := R) (↑(n + (m + 1)) : R) (↑(n + m.succ) : R)
⊢ (↑(-[m+1] + (↑n : ℤ)) : 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]

Premises used: Int.cast_natCast, add_assoc, Int.negSucc_add_ofNat, Int.cast_negSucc, Nat.cast_add, eq_neg_add_iff_add_eq, sub_eq_iff_eq_add, Int.cast_subNatNat, Nat.add_comm
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℕ
rw : (↑-[(m + n).succ+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₁ : (↑-[m + n + 1+1] : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₂ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)
rw₃ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (↑-[n+1] : R)
rw₄ : -(↑(m + n + 1 + 1) : R) = HAdd.hAdd (α := R) (-(↑(m + 1) : R)) (-(↑(n + 1) : R))
rw₅ : -(↑(m + n + 1 + 1) : R) = -HAdd.hAdd (α := R) (↑(n + 1) : R) (↑(m + 1) : R)
rw₆ : Eq.{u + 1} (α := R) (-(↑(m + n + 1 + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₇ : Eq.{u + 1} (α := R) (-(↑(m + 1 + n + 1) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₈ : Eq.{u + 1} (α := R) (-(↑(m + 1 + (n + 1)) : R)) (-(↑(n + 1 + (m + 1)) : R))
rw₉ rw₁₀ : Eq.{u + 1} (α := R) (-(↑(n + 1 + (m + 1)) : R)) (-(↑(n + 1 + (m + 1)) : R))
⊢ (↑(-[m+1] + -[n+1]) : R) = HAdd.hAdd (α := R) (↑-[m+1] : R) (↑-[n+1] : R)

Tactic:
rw [Int.negSucc_add_negSucc, succ_eq_add_one, cast_negSucc, cast_negSucc, cast_negSucc,
      ← neg_add_rev, ← Nat.cast_add, Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]

Premises used: neg_add_rev, Nat.succ_eq_add_one, Int.cast_negSucc, Nat.cast_add, Nat.add_assoc, Int.negSucc_add_negSucc, OfNat.ofNat, Nat.add_right_comm, Nat.add_comm
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
m n : ℤ
⊢ (↑(m - n) : R) = HSub.hSub (α := R) (↑m : R) (↑n : R)

Tactic:
simp [Int.sub_eq_add_neg, sub_eq_add_neg, Int.cast_neg, Int.cast_add]

Premises used: Int.cast_neg, sub_eq_add_neg, Int.cast_add, Int.sub_eq_add_neg
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑2 : R) 2

Tactic:
cast_ofNat _

Premises used: Int.cast_ofNat
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑3 : R) 3

Tactic:
cast_ofNat _

Premises used: Int.cast_ofNat
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u
inst : AddGroupWithOne R
⊢ Eq.{u + 1} (α := R) (↑4 : R) 4

Tactic:
cast_ofNat _

Premises used: Int.cast_ofNat
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
n : ℤ
ofNat : ∀ (a : ℕ), HSMul.hSMul (β := R) (Int.ofNat a) 1 = (↑(Int.ofNat a) : R)
negSucc : ∀ (a : ℕ), HSMul.hSMul (β := R) (Int.negSucc a) 1 = (↑(Int.negSucc a) : R)
⊢ HSMul.hSMul (β := R) n 1 = (↑n : R)

Tactic:
cases n
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
a : ℕ
⊢ HSMul.hSMul (β := R) (Int.ofNat a) 1 = (↑(Int.ofNat a) : R)

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Basic
Goal:
R : Type u_1
inst : AddGroupWithOne R
a : ℕ
⊢ HSMul.hSMul (β := R) (Int.negSucc a) 1 = (↑(Int.negSucc a) : R)

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Field
Goal:
R : Type u_2
inst : DivisionRing R
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (↑(-(↑n : ℤ)) : R) (-(↑n : R))

Tactic:
simp
-- Module: Mathlib.Data.Int.Cast.Field
Goal:
α : Type u_1
inst : DivisionRing α
m n : ℤ
n_dvd : n ∣ m
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
rcases : ∀ (k : ℤ), (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
⊢ (↑(m / n) : α) = HDiv.hDiv (α := α) (↑m : α) (↑n : α)

Tactic:
rcases n_dvd with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Field
Goal:
α : Type u_1
inst : DivisionRing α
k : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑0 : α) 0
⊢ False

Tactic:
simp at hn
-- Module: Mathlib.Data.Int.Cast.Field
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
⊢ n ≠ 0

Tactic:
have : n ≠ 0 := by rintro rfl; simp at hn
-- Module: Mathlib.Data.Int.Cast.Field
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
hn : Ne.{u_1 + 1} (α := α) (↑n : α) 0
k : ℤ
this : n ≠ 0
rw : (↑k : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)
rw₁ : (↑k : α) = HDiv.hDiv (α := α) (↑(k * n) : α) (↑n : α)
rw₂ : (↑k : α) = HMul.hMul (α := α) (↑k : α) (↑n : α) / (↑n : α)
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) (↑k : α) (↑k : α)
⊢ (↑(n * k / n) : α) = HDiv.hDiv (α := α) (↑(n * k) : α) (↑n : α)

Tactic:
rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]

Premises used: mul_div_cancel_right₀, Int.cast_mul, Int.mul_ediv_cancel_left, mul_comm
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
⊢ Eq (α := (a : ℤ) → α) (⇑(castAddHom α) : (a : ℤ) → α) fun (x : ℤ) ↦ (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
n : ℤ
h : Even n
⊢ Even.{u_3} (α := α) (↑n : α)

Tactic:
h.map (castAddHom α)

Premises used: Even.map, Int.castAddHom
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : Eq.{u_3 + 1} (α := α) (↑n : α) 0
ofNat : ∀ (a : ℕ) (h : Eq.{u_3 + 1} (α := α) (↑(Int.ofNat a) : α) 0), Int.ofNat a = 0
negSucc : ∀ (a : ℕ) (h : Eq.{u_3 + 1} (α := α) (↑-[a+1] : α) 0), -[a+1] = 0
⊢ n = 0

Tactic:
cases n
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑(ofNat a) : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑a : α) 0

Tactic:
rw [ofNat_eq_natCast, Int.cast_natCast] at h

Premises used: Int.cast_natCast, Int.ofNat_eq_natCast
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑a : α) 0
⊢ ofNat a = 0

Tactic:
congr_arg _ (Nat.cast_eq_zero.1 h)

Premises used: congr_arg, Nat.cast_eq_zero, Iff.mp
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑a : α) 0
⊢ ofNat a = 0

Tactic:
exact congr_arg _ (Nat.cast_eq_zero.1 h)

Premises used: congr_arg, Nat.cast_eq_zero, Iff.mp
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : Eq.{u_3 + 1} (α := α) (↑-[a+1] : α) 0
⊢ a + 1 = 0

Tactic:
rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h

Premises used: neg_eq_zero, Int.cast_negSucc, Nat.cast_eq_zero
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
a : ℕ
h : a + 1 = 0
⊢ -[a+1] = 0

Tactic:
contradiction
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
h : n = 0
rw : Eq.{u_3 + 1} (α := α) (↑0 : α) 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) 0 0
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 0

Tactic:
rw [h, cast_zero]

Premises used: Int.cast_zero
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
m n : ℤ
rw : HSub.hSub (α := α) (↑m : α) (↑n : α) = 0 ↔ m = n
rw₁ : Eq.{u_3 + 1} (α := α) (↑(m - n) : α) 0 ↔ m = n
rw₂ : m - n = 0 ↔ m = n
rw₃ rw₄ : m = n ↔ m = n
⊢ Eq.{u_3 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n

Tactic:
rw [← sub_eq_zero, ← cast_sub, cast_eq_zero, sub_eq_zero]

Premises used: sub_eq_zero, Int.cast_sub, Int.cast_eq_zero
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
⊢ Injective.{1, u_3 + 1} (β := α) Int.cast

Tactic:
fun _ _ ↦ cast_inj.1

Premises used: Int.cast_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
⊢ Ne.{u_3 + 1} (α := α) (↑n : α) 0 ↔ n ≠ 0

Tactic:
not_congr cast_eq_zero

Premises used: Int.cast_eq_zero, not_congr
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
rw : Eq.{u_3 + 1} (α := α) (↑n : α) (↑1 : α) ↔ n = 1
rw₁ rw₂ : n = 1 ↔ n = 1
⊢ Eq.{u_3 + 1} (α := α) (↑n : α) 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

Premises used: Int.cast_inj, Int.cast_one
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : AddGroupWithOne α
inst_1 : CharZero α
n : ℤ
⊢ Ne.{u_3 + 1} (α := α) (↑n : α) 1 ↔ n ≠ 1

Tactic:
cast_eq_one.not

Premises used: Iff.not, Int.cast_eq_one
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
⊢ Eq (α := (a : ℤ) → α) (⇑(castRingHom α) : (a : ℤ) → α) fun (x : ℤ) ↦ (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑(↑n : ℤ) : α) x

Tactic:
simpa using n.cast_commute x

Premises used: Nat.cast_commute
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
n : ℕ
x : α
⊢ Commute (↑-[n+1] : α) x

Tactic:
simpa only [cast_negSucc, Commute.neg_left_iff, Commute.neg_right_iff] using
      (n + 1).cast_commute (-x)

Premises used: Commute.neg_right_iff, Commute.neg_left_iff, Int.cast_negSucc, HAdd.hAdd, OfNat.ofNat, Neg.neg, Nat.cast_commute
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
n : ℤ
x : α
⊢ (↑n : α) * x = x * (↑n : α)

Tactic:
(cast_commute ..).eq

Premises used: Int.cast_commute, Commute.eq
-- Module: Mathlib.Data.Int.Cast.Lemmas
Goal:
α : Type u_3
inst : NonAssocRing α
a : α
n : ℤ
⊢ Commute a (↑n : α)

Tactic:
(cast_commute ..).symm

Premises used: Commute.symm, Int.cast_commute