awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_add_zsmul hp a b m

Premises used: congrArg, cast, toIcoMod_add_zsmul, Int, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
simp only [toIcoMod, toIcoDiv_add_zsmul', sub_smul, sub_add]

Premises used: sub_add, sub_smul, toIcoDiv_add_zsmul', toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
mod_cast toIcoMod_add_zsmul' hp a b m

Premises used: congrArg, cast, Int, Nat.cast, HAdd.hAdd, congr, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, toIcoMod_add_zsmul', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b

Tactic:
rw [toIocMod, toIocDiv_add_zsmul, toIocMod, add_smul]

Premises used: add_smul, toIocMod, toIocDiv_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b

Tactic:
mod_cast toIocMod_add_zsmul hp a b m

Premises used: congrArg, toIocMod.congr_simp, cast, Int, Nat.cast, HAdd.hAdd, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', toIocMod_add_zsmul, Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + m • p) b = toIocMod hp a b + m • p

Tactic:
simp only [toIocMod, toIocDiv_add_zsmul', sub_smul, sub_add]

Premises used: sub_add, sub_smul, toIocMod, toIocDiv_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp (a + m • p) b = toIocMod hp a b + m • p

Tactic:
mod_cast toIocMod_add_zsmul' hp a b m

Premises used: congrArg, toIocMod.congr_simp, cast, toIocMod_add_zsmul', Int, Nat.cast, HAdd.hAdd, congr, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIcoMod hp a (b + m • p) = toIcoMod hp a b
rw₁ rw₂ : toIcoMod hp a b = toIcoMod hp a b
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_zsmul]

Premises used: toIcoMod_add_zsmul, add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp a (m • p + b) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_zsmul_add hp a b m

Premises used: congrArg, cast, Int, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, toIcoMod_zsmul_add, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIcoMod hp (a + m • p) b = m • p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + m • p = m • p + toIcoMod hp a b
rw₂ rw₃ : m • p + toIcoMod hp a b = m • p + toIcoMod hp a b
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_zsmul', add_comm]

Premises used: add_comm, toIcoMod_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b

Tactic:
mod_cast toIcoMod_zsmul_add' hp a b m

Premises used: congrArg, cast, Int, Nat.cast, toIcoMod_zsmul_add', HAdd.hAdd, congr, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIocMod hp a (b + m • p) = toIocMod hp a b
rw₁ rw₂ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_zsmul]

Premises used: add_comm, toIocMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp a (m • p + b) = toIocMod hp a b

Tactic:
mod_cast toIocMod_zsmul_add hp a b m

Premises used: congrArg, toIocMod.congr_simp, cast, Int, Nat.cast, HAdd.hAdd, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, toIocMod_zsmul_add, HSMul.hSMul, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIocMod hp (a + m • p) b = m • p + toIocMod hp a b
rw₁ : toIocMod hp a b + m • p = m • p + toIocMod hp a b
rw₂ rw₃ : m • p + toIocMod hp a b = m • p + toIocMod hp a b
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_zsmul', add_comm]

Premises used: toIocMod_add_zsmul', add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp (m • p + a) b = m • p + toIocMod hp a b

Tactic:
mod_cast toIocMod_zsmul_add' hp a b m

Premises used: congrArg, toIocMod.congr_simp, toIocMod_zsmul_add', cast, Int, Nat.cast, HAdd.hAdd, congr, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIcoMod hp a (b + -(m • p)) = toIcoMod hp a b
rw₁ : toIcoMod hp a (b + -m • p) = toIcoMod hp a b
rw₂ rw₃ : toIcoMod hp a b = toIcoMod hp a b
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul]

Premises used: neg_smul, sub_eq_add_neg, toIcoMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_sub_zsmul hp a b m

Premises used: toIcoMod_sub_zsmul, congrArg, HSub.hSub, cast, Int, Nat.cast, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
simp_rw : toIcoMod hp (a + -(m • p)) b = toIcoMod hp a b + -(m • p)
simp_rw₁ : toIcoMod hp (a + -m • p) b = toIcoMod hp a b + -m • p
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p

Tactic:
simp_rw [sub_eq_add_neg, ← neg_smul, toIcoMod_add_zsmul']

Premises used: neg_smul, sub_eq_add_neg, toIcoMod_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p

Tactic:
mod_cast toIcoMod_sub_zsmul' hp a b m

Premises used: congrArg, HSub.hSub, cast, Int, Nat.cast, congr, toIcoMod_sub_zsmul', Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
rw : toIocMod hp a (b + -(m • p)) = toIocMod hp a b
rw₁ : toIocMod hp a (b + -m • p) = toIocMod hp a b
rw₂ rw₃ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul]

Premises used: neg_smul, sub_eq_add_neg, toIocMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
mod_cast toIocMod_sub_zsmul hp a b m

Premises used: congrArg, toIocMod.congr_simp, HSub.hSub, cast, Int, Nat.cast, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', toIocMod_sub_zsmul, Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
simp_rw : toIocMod hp (a + -(m • p)) b = toIocMod hp a b + -(m • p)
simp_rw₁ : toIocMod hp (a + -m • p) b = toIocMod hp a b + -m • p
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Tactic:
simp_rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul']

Premises used: neg_smul, sub_eq_add_neg, toIocMod_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℕ
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Tactic:
mod_cast toIocMod_sub_zsmul' hp a b m

Premises used: congrArg, toIocMod.congr_simp, HSub.hSub, cast, Int, Nat.cast, congr, toIocMod, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, Eq, toIocMod_sub_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b + p) = toIcoMod hp a b

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul hp a b 1

Premises used: toIcoMod_add_zsmul, one_zsmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a + p) b = toIcoMod hp a b + p

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul' hp a b 1

Premises used: one_zsmul, toIcoMod_add_zsmul', OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b + p) = toIocMod hp a b

Tactic:
simpa only [one_zsmul] using toIocMod_add_zsmul hp a b 1

Premises used: one_zsmul, OfNat.ofNat, toIocMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a + p) b = toIocMod hp a b + p

Tactic:
simpa only [one_zsmul] using toIocMod_add_zsmul' hp a b 1

Premises used: toIocMod_add_zsmul', one_zsmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIcoMod hp a (b + p) = toIcoMod hp a b
rw₁ rw₂ : toIcoMod hp a b = toIcoMod hp a b
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_right]

Premises used: toIcoMod_add_right, add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIcoMod hp (a + p) b = p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + p = p + toIcoMod hp a b
rw₂ rw₃ : p + toIcoMod hp a b = p + toIcoMod hp a b
⊢ toIcoMod hp (p + a) b = p + toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_right', add_comm]

Premises used: add_comm, toIcoMod_add_right'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocMod hp a (b + p) = toIocMod hp a b
rw₁ rw₂ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a (p + b) = toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_right]

Premises used: add_comm, toIocMod_add_right
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocMod hp (a + p) b = p + toIocMod hp a b
rw₁ : toIocMod hp a b + p = p + toIocMod hp a b
rw₂ rw₃ : p + toIocMod hp a b = p + toIocMod hp a b
⊢ toIocMod hp (p + a) b = p + toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_right', add_comm]

Premises used: add_comm, toIocMod_add_right'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b - p) = toIcoMod hp a b

Tactic:
simpa only [one_zsmul] using toIcoMod_sub_zsmul hp a b 1

Premises used: toIcoMod_sub_zsmul, one_zsmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a - p) b = toIcoMod hp a b - p

Tactic:
simpa only [one_zsmul] using toIcoMod_sub_zsmul' hp a b 1

Premises used: one_zsmul, toIcoMod_sub_zsmul', OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b - p) = toIocMod hp a b

Tactic:
simpa only [one_zsmul] using toIocMod_sub_zsmul hp a b 1

Premises used: one_zsmul, toIocMod_sub_zsmul, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (a - p) b = toIocMod hp a b - p

Tactic:
simpa only [one_zsmul] using toIocMod_sub_zsmul' hp a b 1

Premises used: one_zsmul, OfNat.ofNat, toIocMod_sub_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b - c - toIcoDiv hp a (b - c) • p = b - toIcoDiv hp (a + c) b • p - c
simp_rw₁ : b - c - toIcoDiv hp (a + c) b • p = b - toIcoDiv hp (a + c) b • p - c
⊢ toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c

Tactic:
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add, sub_right_comm]

Premises used: toIcoDiv_sub_eq_toIcoDiv_add, sub_right_comm, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b - c - toIocDiv hp a (b - c) • p = b - toIocDiv hp (a + c) b • p - c
simp_rw₁ : b - c - toIocDiv hp (a + c) b • p = b - toIocDiv hp (a + c) b • p - c
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]

Premises used: toIocDiv_sub_eq_toIocDiv_add, sub_right_comm, toIocMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b + c - toIcoDiv hp a (b + c) • p = b - toIcoDiv hp (a - c) b • p + c
simp_rw₁ : b + c - toIcoDiv hp a (b + c) • p = b - toIcoDiv hp a (b + c) • p + c
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Tactic:
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]

Premises used: toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
simp_rw : b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp (a - c) b • p + c
simp_rw₁ : b + c - toIocDiv hp a (b + c) • p = b - toIocDiv hp a (b + c) • p + c
⊢ toIocMod hp a (b + c) = toIocMod hp (a - c) b + c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add', sub_add_eq_add_sub]

Premises used: toIocMod, sub_add_eq_add_sub, toIocDiv_sub_eq_toIocDiv_add'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
simp_rw : -b - -(toIocDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIocDiv hp (-a) b • p)
⊢ toIcoMod hp a (-b) = p - toIocMod hp (-a) b

Tactic:
simp_rw [toIcoMod, toIocMod, toIcoDiv_neg, neg_smul, add_smul]

Premises used: neg_smul, add_smul, toIocMod, toIcoDiv_neg, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIocDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIocDiv hp (-a) b • p)

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (-a) b = p - toIocMod hp a (-b)

Tactic:
simpa only [neg_neg] using toIcoMod_neg hp (-a) (-b)

Premises used: toIcoMod_neg, neg_neg, Neg.neg
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
simp_rw : -b - -(toIcoDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIcoDiv hp (-a) b • p)
⊢ toIocMod hp a (-b) = p - toIcoMod hp (-a) b

Tactic:
simp_rw [toIocMod, toIcoMod, toIocDiv_neg, neg_smul, add_smul]

Premises used: neg_smul, add_smul, toIocMod, toIocDiv_neg, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ -b - -(toIcoDiv hp (-a) b • p + HSMul.hSMul (α := ℤ) 1 p) = p - (b - toIcoDiv hp (-a) b • p)

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp (-a) b = p - toIcoMod hp a (-b)

Tactic:
simpa only [neg_neg] using toIocMod_neg hp (-a) (-b)

Premises used: toIocMod_neg, neg_neg, Neg.neg
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ (n : ℤ), c - b = n • p

Tactic:
⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩

Premises used: HSub.hSub, toIcoDiv, Iff.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
refine_1 : ∀ (h : toIcoMod hp a b = toIcoMod hp a c), c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p
refine_2 : ∀ (h : ∃ (n : ℤ), c - b = n • p), toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a b = toIcoMod hp a c ↔ ∃ (n : ℤ), c - b = n • p

Tactic:
refine ⟨fun h => ⟨toIcoDiv hp a c - toIcoDiv hp a b, ?_⟩, fun h => ?_⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
rw : toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p)
| c - b

Tactic:
rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]

Premises used: toIcoMod_add_toIcoDiv_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
refine_1 :
  toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p
⊢ c - b = (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
conv_lhs => rw [← toIcoMod_add_toIcoDiv_zsmul hp a b, ← toIcoMod_add_toIcoDiv_zsmul hp a c]

Premises used: toIcoMod_add_toIcoDiv_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
refine_1 :
  toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a b + toIcoDiv hp a b • p) =
    (toIcoDiv hp a c - toIcoDiv hp a b) • p

Tactic:
rw [h, sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a c + toIcoDiv hp a c • p - (toIcoMod hp a c + toIcoDiv hp a b • p) =
    toIcoDiv hp a c • p - toIcoDiv hp a b • p

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ (n : ℤ), c - b = n • p
refine_2 : ∀ (z : ℤ) (hz : c - b = z • p), toIcoMod hp a b = toIcoMod hp a c
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rcases h with ⟨z, hz⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ c = z • p + b

Tactic:
rw [sub_eq_iff_eq_add] at hz

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
refine_2 : toIcoMod hp a b = toIcoMod hp a (z • p + b)
refine_2₁ refine_2₂ : toIcoMod hp a b = toIcoMod hp a b
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rw [hz, toIcoMod_zsmul_add]

Premises used: toIcoMod_zsmul_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a b = toIocMod hp a c ↔ ∃ (n : ℤ), c - b = n • p

Tactic:
⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩

Premises used: HSub.hSub, Iff.intro, Exists.intro, toIocDiv