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 : ℤ
refine : b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - m

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc _ ?_

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- 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 - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)

Tactic:
rw [sub_smul, ← sub_add, add_right_comm]

Premises used: sub_add, sub_smul, add_right_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 : ℤ
⊢ b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + p + m • p)

Tactic:
simpa using sub_toIocDiv_zsmul_mem_Ioc hp a b

Premises used: sub_toIocDiv_zsmul_mem_Ioc
-- 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 : ℕ
⊢ toIocDiv hp (a + m • p) b = toIocDiv hp a b - (↑m : ℤ)

Tactic:
mod_cast toIocDiv_add_zsmul' hp a b m

Premises used: congrArg, HSub.hSub, cast, Int, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, toIocDiv_add_zsmul', Eq.refl, HSMul.hSMul, congrFun', Eq, toIocDiv
-- 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 : toIcoDiv hp a (b + m • p) = m + toIcoDiv hp a b
rw₁ : toIcoDiv hp a b + m = m + toIcoDiv hp a b
rw₂ rw₃ : m + toIcoDiv hp a b = m + toIcoDiv hp a b
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b

Tactic:
rw [add_comm, toIcoDiv_add_zsmul, add_comm]

Premises used: toIcoDiv_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 : ℕ
⊢ toIcoDiv hp a (m • p + b) = (↑m : ℤ) + toIcoDiv hp a b

Tactic:
mod_cast toIcoDiv_zsmul_add hp a b m

Premises used: congrArg, cast, toIcoDiv_zsmul_add, toIcoDiv.congr_simp, toIcoDiv, Int, Nat.cast, HAdd.hAdd, 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 : toIocDiv hp a (b + m • p) = m + toIocDiv hp a b
rw₁ : toIocDiv hp a b + m = m + toIocDiv hp a b
rw₂ rw₃ : m + toIocDiv hp a b = m + toIocDiv hp a b
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Tactic:
rw [add_comm, toIocDiv_add_zsmul, add_comm]

Premises used: add_comm, 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 : ℕ
⊢ toIocDiv hp a (m • p + b) = (↑m : ℤ) + toIocDiv hp a b

Tactic:
mod_cast toIocDiv_zsmul_add hp a b m

Premises used: congrArg, cast, Int, toIocDiv.congr_simp, Nat.cast, toIocDiv_zsmul_add, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIocDiv
-- 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 : toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
rw₁ : toIcoDiv hp a (b + -m • p) = toIcoDiv hp a b - m
rw₂ : toIcoDiv hp a b + -m = toIcoDiv hp a b - m
rw₃ rw₄ : toIcoDiv hp a b + -m = toIcoDiv hp a b + -m
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul, sub_eq_add_neg]

Premises used: neg_smul, sub_eq_add_neg, toIcoDiv_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 : ℕ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - (↑m : ℤ)

Tactic:
mod_cast toIcoDiv_sub_zsmul hp a b m

Premises used: congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Int, Nat.cast, Nat.cast_smul_eq_nsmul, toIcoDiv_sub_zsmul, 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 : toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
rw₁ : toIcoDiv hp (a + -m • p) b = toIcoDiv hp a b + m
rw₂ : toIcoDiv hp a b - -m = toIcoDiv hp a b + m
rw₃ rw₄ : toIcoDiv hp a b + m = toIcoDiv hp a b + m
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_eq_add]

Premises used: neg_smul, sub_eq_add_neg, toIcoDiv_add_zsmul', sub_neg_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 : α
m : ℕ
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + (↑m : ℤ)

Tactic:
mod_cast toIcoDiv_sub_zsmul' hp a b m

Premises used: congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Int, Nat.cast, HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIcoDiv_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 : α
m : ℤ
rw : toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
rw₁ : toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m
rw₂ : toIocDiv hp a b + -m = toIocDiv hp a b - m
rw₃ rw₄ : toIocDiv hp a b + -m = toIocDiv hp a b + -m
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul, sub_eq_add_neg]

Premises used: neg_smul, sub_eq_add_neg, 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 : ℕ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - (↑m : ℤ)

Tactic:
mod_cast toIocDiv_sub_zsmul hp a b m

Premises used: congrArg, HSub.hSub, cast, Int, toIocDiv.congr_simp, Nat.cast, toIocDiv_sub_zsmul, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIocDiv
-- 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 : toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
rw₁ : toIocDiv hp (a + -m • p) b = toIocDiv hp a b + m
rw₂ : toIocDiv hp a b - -m = toIocDiv hp a b + m
rw₃ rw₄ : toIocDiv hp a b + m = toIocDiv hp a b + m
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_eq_add]

Premises used: neg_smul, sub_eq_add_neg, toIocDiv_add_zsmul', sub_neg_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 : α
m : ℕ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + (↑m : ℤ)

Tactic:
mod_cast toIocDiv_sub_zsmul' hp a b m

Premises used: congrArg, HSub.hSub, cast, Int, toIocDiv.congr_simp, Nat.cast, toIocDiv_sub_zsmul', HAdd.hAdd, Nat.cast_smul_eq_nsmul, Eq.refl, HSMul.hSMul, congrFun', Eq, toIocDiv
-- 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 : α
⊢ toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1

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

Premises used: toIcoDiv_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 : α
⊢ toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

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

Premises used: one_zsmul, toIcoDiv_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 : α
⊢ toIocDiv hp a (b + p) = toIocDiv hp a b + 1

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

Premises used: one_zsmul, toIocDiv_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 : α
⊢ toIocDiv hp (a + p) b = toIocDiv hp a b - 1

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

Premises used: one_zsmul, toIocDiv_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 : α
rw : toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
rw₁ rw₂ : toIcoDiv hp a b + 1 = toIcoDiv hp a b + 1
⊢ toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1

Tactic:
rw [add_comm, toIcoDiv_add_right]

Premises used: add_comm, toIcoDiv_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 : toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
rw₁ rw₂ : toIcoDiv hp a b - 1 = toIcoDiv hp a b - 1
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Tactic:
rw [add_comm, toIcoDiv_add_right']

Premises used: add_comm, toIcoDiv_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 : toIocDiv hp a (b + p) = toIocDiv hp a b + 1
rw₁ rw₂ : toIocDiv hp a b + 1 = toIocDiv hp a b + 1
⊢ toIocDiv hp a (p + b) = toIocDiv hp a b + 1

Tactic:
rw [add_comm, toIocDiv_add_right]

Premises used: add_comm, toIocDiv_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 : toIocDiv hp (a + p) b = toIocDiv hp a b - 1
rw₁ rw₂ : toIocDiv hp a b - 1 = toIocDiv hp a b - 1
⊢ toIocDiv hp (p + a) b = toIocDiv hp a b - 1

Tactic:
rw [add_comm, toIocDiv_add_right']

Premises used: toIocDiv_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 : α
⊢ toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1

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

Premises used: one_zsmul, toIcoDiv_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 : α
⊢ toIcoDiv hp (a - p) b = toIcoDiv hp a b + 1

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

Premises used: one_zsmul, OfNat.ofNat, toIcoDiv_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 : α
⊢ toIocDiv hp a (b - p) = toIocDiv hp a b - 1

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

Premises used: toIocDiv_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 : α
⊢ toIocDiv hp (a - p) b = toIocDiv hp a b + 1

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

Premises used: one_zsmul, toIocDiv_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 c : α
a₁ : b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)
⊢ toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b

Tactic:
apply toIcoDiv_eq_of_sub_zsmul_mem_Ico

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- 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 : α
a₁ : b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)
⊢ b - c - toIcoDiv hp (a + c) b • p ∈ Set.Ico a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ico_iff_left, add_right_comm]

Premises used: Set.sub_mem_Ico_iff_left, add_right_comm, sub_right_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 c : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)

Tactic:
sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

Premises used: Set.Mem, sub_toIcoDiv_zsmul_mem_Ico, HAdd.hAdd
-- 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 : α
⊢ b - toIcoDiv hp (a + c) b • p ∈ Set.Ico (a + c) (a + c + p)

Tactic:
exact sub_toIcoDiv_zsmul_mem_Ico hp (a + c) b

Premises used: sub_toIcoDiv_zsmul_mem_Ico, HAdd.hAdd
-- 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 : α
a₁ : b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)
⊢ toIocDiv hp a (b - c) = toIocDiv hp (a + c) b

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- 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 : α
a₁ : b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ioc_iff_left, add_right_comm]

Premises used: Set.sub_mem_Ioc_iff_left, add_right_comm, sub_right_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 c : α
⊢ b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)

Tactic:
sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

Premises used: Set.Mem, HAdd.hAdd, sub_toIocDiv_zsmul_mem_Ioc
-- 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 : α
⊢ b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)

Tactic:
exact sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

Premises used: HAdd.hAdd, sub_toIocDiv_zsmul_mem_Ioc
-- 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 : α
rw : toIcoDiv hp (a - c) b = toIcoDiv hp a (b - -c)
rw₁ : toIcoDiv hp (a - c) b = toIcoDiv hp (a + -c) b
rw₂ rw₃ : toIcoDiv hp (a + -c) b = toIcoDiv hp (a + -c) b
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, sub_eq_add_neg]

Premises used: toIcoDiv_sub_eq_toIcoDiv_add, sub_eq_add_neg, sub_neg_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 : α
rw : toIocDiv hp (a - c) b = toIocDiv hp a (b - -c)
rw₁ : toIocDiv hp (a - c) b = toIocDiv hp (a + -c) b
rw₂ rw₃ : toIocDiv hp (a + -c) b = toIocDiv hp (a + -c) b
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg]

Premises used: toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg, sub_neg_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 : α
this : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
rwa : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a + -p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₁ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a - p) b), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₂ : ∀ (this : toIcoDiv hp a (-b) = -toIocDiv hp (-a) (b + p)), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)), toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this

Premises used: sub_eq_add_neg, neg_add, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_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 : α
suffices : toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this
-- 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 : toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)
⊢ toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b

Tactic:
rw [← neg_eq_iff_eq_neg, eq_comm]

Premises used: neg_eq_iff_eq_neg, eq_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 : α
a₁ : b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
⊢ toIocDiv hp (-(a + p)) b = -toIcoDiv hp a (-b)

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- 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 : α
⊢ a ≤ -b - toIcoDiv hp a (-b) • p

Tactic:
obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)

Premises used: sub_toIcoDiv_zsmul_mem_Ico, 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
⊢ -b - toIcoDiv hp a (-b) • p < a + p

Tactic:
obtain ⟨hc, ho⟩ := sub_toIcoDiv_zsmul_mem_Ico hp a (-b)

Premises used: sub_toIcoDiv_zsmul_mem_Ico, 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ -(a + p) < b - -toIcoDiv hp a (-b) • p

Tactic:
rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho

Premises used: neg_lt_neg_iff, neg_smul, neg_neg, neg_sub', 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ≤ -a

Tactic:
rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc

Premises used: neg_smul, neg_neg, neg_sub', Neg.neg, neg_le_neg_iff
-- 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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
hc₁ : b - -toIcoDiv hp a (-b) • p ≤ -a
⊢ -(a + p) < b - -toIcoDiv hp a (-b) • p

Tactic:
rw [← neg_le_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at hc

Premises used: neg_smul, neg_neg, neg_sub', Neg.neg, neg_le_neg_iff
-- 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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
⟨ho, hc.trans_eq ?_⟩

Premises used: Set.Ioc, LE.le.trans_eq, Set.Mem, setOf, And.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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
a₁ : -a = -(a + p) + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
refine ⟨ho, hc.trans_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 : α
hc : b - -toIcoDiv hp a (-b) • p ≤ -a
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
a₁ : -a = -a + -p + p
a₂ a₃ : -a = -a
⊢ -a = -(a + p) + p

Tactic:
rw [neg_add, neg_add_cancel_right]

Premises used: neg_add, neg_add_cancel_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 : α
⊢ toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

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

Premises used: neg_neg, toIcoDiv_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 : α
rw : toIocDiv hp a (- - -b) = -(toIcoDiv hp (-a) (- -b) + 1)
rw₁ : toIocDiv hp a (- - -b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₂ : toIocDiv hp a (-b) = -(-(toIocDiv hp (- -a) (-b) + 1) + 1)
rw₃ : toIocDiv hp a (-b) = -(-(toIocDiv hp a (-b) + 1) + 1)
rw₄ : toIocDiv hp a (-b) = - -(toIocDiv hp a (-b) + 1) - 1
rw₅ : toIocDiv hp a (-b) = toIocDiv hp a (-b) + 1 - 1
rw₆ rw₇ : toIocDiv hp a (-b) = toIocDiv hp a (-b)
⊢ toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)

Tactic:
rw [← neg_neg b, toIcoDiv_neg, neg_neg, neg_neg, neg_add', neg_neg, add_sub_cancel_right]

Premises used: neg_neg, neg_add', toIcoDiv_neg, add_sub_cancel_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 : α
⊢ toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)

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

Premises used: neg_neg, toIocDiv_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 : α
m : ℤ
rw : b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, add_smul]

Premises used: toIcoDiv_add_zsmul, add_smul, 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 : ℤ
⊢ b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p

Tactic:
abel