awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocDiv hp a (b - (↑m : R) * p) = toIocDiv hp a b - (↑m : ℤ)

Tactic:
mod_cast toIocDiv_sub_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, HSub.hSub, cast, toIocDiv.congr_simp, Nat.cast, Eq.refl, congrFun', toIocDiv_sub_intCast_mul, Eq, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocDiv hp a (b - OfNat.ofNat m * p) = toIocDiv hp a b - OfNat.ofNat m

Tactic:
toIocDiv_sub_natCast_mul hp a b m

Premises used: toIocDiv_sub_natCast_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocDiv hp (a - (↑m : R) * p) b = toIocDiv hp a b + m

Tactic:
simpa using toIocDiv_sub_zsmul' hp a b m

Premises used: toIocDiv_sub_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocDiv hp (a - (↑m : R) * p) b = toIocDiv hp a b + (↑m : ℤ)

Tactic:
mod_cast toIocDiv_sub_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, HSub.hSub, cast, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, toIocDiv_sub_intCast_mul', Eq.refl, congrFun', Eq, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocDiv hp (a - OfNat.ofNat m * p) b = toIocDiv hp a b + OfNat.ofNat m

Tactic:
toIocDiv_sub_natCast_mul' hp a b m

Premises used: toIocDiv_sub_natCast_mul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp a (b + (↑m : R) * p) = toIcoMod hp a b

Tactic:
simpa using toIcoMod_add_zsmul hp a b m

Premises used: toIcoMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp a (b + (↑m : R) * p) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_add_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIcoMod_add_intCast_mul, cast, Nat.cast, HAdd.hAdd, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp a (b + OfNat.ofNat m * p) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_add_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIcoMod_add_intCast_mul, cast, Nat.cast, HAdd.hAdd, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp (a + (↑m : R) * p) b = toIcoMod hp a b + (↑m : R) * p

Tactic:
simpa using toIcoMod_add_zsmul' hp a b m

Premises used: toIcoMod_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp (a + (↑m : R) * p) b = toIcoMod hp a b + (↑m : R) * p

Tactic:
mod_cast toIcoMod_add_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, toIcoMod_add_intCast_mul', Nat.cast, HAdd.hAdd, congr, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp (a + OfNat.ofNat m * p) b = toIcoMod hp a b + OfNat.ofNat m * p

Tactic:
toIcoMod_add_natCast_mul' hp a b m

Premises used: toIcoMod_add_natCast_mul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a (b + (↑m : R) * p) = toIocMod hp a b

Tactic:
simpa using toIocMod_add_zsmul hp a b m

Premises used: toIocMod_add_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp a (b + (↑m : R) * p) = toIocMod hp a b

Tactic:
mod_cast toIocMod_add_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, toIocMod_add_intCast_mul, cast, Nat.cast, HAdd.hAdd, toIocMod, Eq.refl, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp a (b + OfNat.ofNat m * p) = toIocMod hp a b

Tactic:
toIocMod_add_natCast_mul hp a b m

Premises used: toIocMod_add_natCast_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp (a + (↑m : R) * p) b = toIocMod hp a b + (↑m : R) * p

Tactic:
simpa using toIocMod_add_zsmul' hp a b m

Premises used: toIocMod_add_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp (a + (↑m : R) * p) b = toIocMod hp a b + (↑m : R) * p

Tactic:
mod_cast toIocMod_add_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, toIocMod_add_intCast_mul', cast, Nat.cast, HAdd.hAdd, congr, toIocMod, Eq.refl, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp (a + OfNat.ofNat m * p) b = toIocMod hp a b + OfNat.ofNat m * p

Tactic:
toIocMod_add_natCast_mul' hp a b m

Premises used: toIocMod_add_natCast_mul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp a ((↑m : R) * p + b) = toIcoMod hp a b

Tactic:
simpa using toIcoMod_zsmul_add hp a b m

Premises used: toIcoMod_zsmul_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp a ((↑m : R) * p + b) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_intCast_mul_add hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, HAdd.hAdd, toIcoMod_intCast_mul_add, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp a (OfNat.ofNat m * p + b) = toIcoMod hp a b

Tactic:
toIcoMod_natCast_mul_add hp a b m

Premises used: toIcoMod_natCast_mul_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIcoMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIcoMod hp a b
rw₁ : toIcoMod hp a b + (↑m : R) * p = (↑m : R) * p + toIcoMod hp a b
rw₂ rw₃ : (↑m : R) * p + toIcoMod hp a b = (↑m : R) * p + toIcoMod hp a b
⊢ toIcoMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_intCast_mul', add_comm]

Premises used: toIcoMod_add_intCast_mul', add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIcoMod hp a b

Tactic:
mod_cast toIcoMod_intCast_mul_add' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, HAdd.hAdd, congr, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp, toIcoMod_intCast_mul_add'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp (OfNat.ofNat m * p + a) b = OfNat.ofNat m * p + toIcoMod hp a b

Tactic:
toIcoMod_natCast_mul_add' hp a b m

Premises used: toIcoMod_natCast_mul_add'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIocMod hp a (b + (↑m : R) * p) = toIocMod hp a b
rw₁ rw₂ : toIocMod hp a b = toIocMod hp a b
⊢ toIocMod hp a ((↑m : R) * p + b) = toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_intCast_mul]

Premises used: toIocMod_add_intCast_mul, add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp a ((↑m : R) * p + b) = toIocMod hp a b

Tactic:
mod_cast toIocMod_intCast_mul_add hp a b m

Premises used: toIocMod_intCast_mul_add, Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, cast, Nat.cast, HAdd.hAdd, toIocMod, Eq.refl, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp a (OfNat.ofNat m * p + b) = toIocMod hp a b

Tactic:
toIocMod_natCast_mul_add hp a b m

Premises used: toIocMod_natCast_mul_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
rw : toIocMod hp (a + (↑m : R) * p) b = (↑m : R) * p + toIocMod hp a b
rw₁ : toIocMod hp a b + (↑m : R) * p = (↑m : R) * p + toIocMod hp a b
rw₂ rw₃ : (↑m : R) * p + toIocMod hp a b = (↑m : R) * p + toIocMod hp a b
⊢ toIocMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIocMod hp a b

Tactic:
rw [add_comm, toIocMod_add_intCast_mul', add_comm]

Premises used: toIocMod_add_intCast_mul', add_comm
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp ((↑m : R) * p + a) b = (↑m : R) * p + toIocMod hp a b

Tactic:
mod_cast toIocMod_intCast_mul_add' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, cast, Nat.cast, HAdd.hAdd, congr, toIocMod, Eq.refl, congrFun', toIocMod_intCast_mul_add', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp (OfNat.ofNat m * p + a) b = OfNat.ofNat m * p + toIocMod hp a b

Tactic:
toIocMod_natCast_mul_add' hp a b m

Premises used: toIocMod_natCast_mul_add'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp a (b - (↑m : R) * p) = toIcoMod hp a b

Tactic:
simpa using toIcoMod_sub_zsmul hp a b m

Premises used: toIcoMod_sub_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp a (b - (↑m : R) * p) = toIcoMod hp a b

Tactic:
mod_cast toIcoMod_sub_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, HSub.hSub, cast, toIcoMod_sub_intCast_mul, Nat.cast, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp a (b - OfNat.ofNat m * p) = toIcoMod hp a b

Tactic:
toIcoMod_sub_natCast_mul hp a b m

Premises used: toIcoMod_sub_natCast_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoMod hp (a - (↑m : R) * p) b = toIcoMod hp a b - (↑m : R) * p

Tactic:
simpa using toIcoMod_sub_zsmul' hp a b m

Premises used: toIcoMod_sub_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIcoMod hp (a - (↑m : R) * p) b = toIcoMod hp a b - (↑m : R) * p

Tactic:
mod_cast toIcoMod_sub_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, HSub.hSub, cast, Nat.cast, toIcoMod_sub_intCast_mul', congr, Eq.refl, congrFun', Eq, toIcoMod, toIcoMod.congr_simp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIcoMod hp (a - OfNat.ofNat m * p) b = toIcoMod hp a b - OfNat.ofNat m * p

Tactic:
toIcoMod_sub_natCast_mul' hp a b m

Premises used: toIcoMod_sub_natCast_mul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp a (b - (↑m : R) * p) = toIocMod hp a b

Tactic:
simpa using toIocMod_sub_zsmul hp a b m

Premises used: toIocMod_sub_zsmul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp a (b - (↑m : R) * p) = toIocMod hp a b

Tactic:
mod_cast toIocMod_sub_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, HSub.hSub, cast, Nat.cast, toIocMod, Eq.refl, congrFun', Eq, toIocMod_sub_intCast_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp a (b - OfNat.ofNat m * p) = toIocMod hp a b

Tactic:
toIocMod_sub_natCast_mul hp a b m

Premises used: toIocMod_sub_natCast_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIocMod hp (a - (↑m : R) * p) b = toIocMod hp a b - (↑m : R) * p

Tactic:
simpa using toIocMod_sub_zsmul' hp a b m

Premises used: toIocMod_sub_zsmul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
⊢ toIocMod hp (a - (↑m : R) * p) b = toIocMod hp a b - (↑m : R) * p

Tactic:
mod_cast toIocMod_sub_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, toIocMod.congr_simp, toIocMod_sub_intCast_mul', HSub.hSub, cast, Nat.cast, congr, toIocMod, Eq.refl, congrFun', Eq
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℕ
inst_4 : m.AtLeastTwo
⊢ toIocMod hp (a - OfNat.ofNat m * p) b = toIocMod hp a b - OfNat.ofNat m * p

Tactic:
toIocMod_sub_natCast_mul' hp a b m

Premises used: toIocMod_sub_natCast_mul'
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv (p := p) hp a b = ⌊(b - a) / p⌋

Tactic:
toIcoDiv_eq_of_sub_zsmul_mem_Ico hp ?_

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
refine : b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
⊢ toIcoDiv (p := p) hp a b = ⌊(b - a) / p⌋

Tactic:
refine toIcoDiv_eq_of_sub_zsmul_mem_Ico hp ?_

Premises used: toIcoDiv_eq_of_sub_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
rw : 0 ≤ b - a - (↑⌊(b - a) / p⌋ : α) * p ∧ b - a - (↑⌊(b - a) / p⌋ : α) * p < p
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)

Tactic:
rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
    sub_right_comm _ _ a]

Premises used: zsmul_eq_mul, Set.mem_Ico, add_comm, sub_right_comm, sub_lt_iff_lt_add, sub_nonneg
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - (↑⌊(b - a) / p⌋ : α) * p ∧ b - a - (↑⌊(b - a) / p⌋ : α) * p < p

Tactic:
⟨Int.sub_floor_div_mul_nonneg _ hp, Int.sub_floor_div_mul_lt _ hp⟩

Premises used: Int.sub_floor_div_mul_nonneg, And.intro, Int.sub_floor_div_mul_lt
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - (↑⌊(b - a) / p⌋ : α) * p ∧ b - a - (↑⌊(b - a) / p⌋ : α) * p < p

Tactic:
exact ⟨Int.sub_floor_div_mul_nonneg _ hp, Int.sub_floor_div_mul_lt _ hp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv (p := p) hp a b = -⌊(a + p - b) / p⌋

Tactic:
toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
refine : b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)
⊢ toIocDiv (p := p) hp a b = -⌊(a + p - b) / p⌋

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_

Premises used: toIocDiv_eq_of_sub_zsmul_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
rw : a < b + (↑⌊(a + p - b) / p⌋ : α) * p ∧ 0 ≤ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)

Tactic:
rw [Set.mem_Ioc, zsmul_eq_mul, Int.cast_neg, neg_mul, sub_neg_eq_add, ← sub_nonneg,
    sub_add_eq_sub_sub]

Premises used: Int.cast_neg, zsmul_eq_mul, sub_add_eq_sub_sub, Set.mem_Ioc, neg_mul, sub_nonneg, sub_neg_eq_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + (↑⌊(a + p - b) / p⌋ : α) * p ∧ 0 ≤ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p

Tactic:
⟨?_, Int.sub_floor_div_mul_nonneg _ hp⟩

Premises used: Int.sub_floor_div_mul_nonneg, And.intro
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
refine : a < b + (↑⌊(a + p - b) / p⌋ : α) * p
⊢ a < b + (↑⌊(a + p - b) / p⌋ : α) * p ∧ 0 ≤ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p

Tactic:
refine ⟨?_, Int.sub_floor_div_mul_nonneg _ hp⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
rw : a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p < p
⊢ a < b + (↑⌊(a + p - b) / p⌋ : α) * p

Tactic:
rw [← add_lt_add_iff_right p, add_assoc, add_comm b, ← sub_lt_iff_lt_add, add_comm (_ * _), ←
    sub_lt_iff_lt_add]

Premises used: HMul.hMul, add_assoc, add_comm, sub_lt_iff_lt_add, add_lt_add_iff_right
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p < p

Tactic:
Int.sub_floor_div_mul_lt _ hp

Premises used: Int.sub_floor_div_mul_lt
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p < p

Tactic:
exact Int.sub_floor_div_mul_lt _ hp

Premises used: Int.sub_floor_div_mul_lt
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
b : α
⊢ toIcoDiv (p := 1) ⋯ 0 b = ⌊b⌋

Tactic:
simp [toIcoDiv_eq_floor]

Premises used: toIcoDiv_eq_floor
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
rw : b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - (↑⌊(b - a) / p⌋ : α)) * p
⊢ toIcoMod (p := p) hp a b = a + Int.fract ((b - a) / p) * p

Tactic:
rw [toIcoMod, toIcoDiv_eq_floor, Int.fract]

Premises used: Int.fract, toIcoDiv_eq_floor, toIcoMod
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
simp : b - (↑⌊(b - a) / p⌋ : α) * p = a + (b - a - (↑⌊(b - a) / p⌋ : α) * p)
⊢ b - ⌊(b - a) / p⌋ • p = a + ((b - a) / p - (↑⌊(b - a) / p⌋ : α)) * p

Tactic:
simp [field, -Int.self_sub_floor]

Premises used: Int.self_sub_floor
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - (↑⌊(b - a) / p⌋ : α) * p = a + (b - a - (↑⌊(b - a) / p⌋ : α) * p)

Tactic:
ring
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
b : α
⊢ toIcoMod (p := p) hp 0 b = Int.fract (b / p) * p

Tactic:
simp [toIcoMod_eq_add_fract_mul]

Premises used: toIcoMod_eq_add_fract_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
rw : b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - (↑⌊(a + p - b) / p⌋ : α)) * p
⊢ toIocMod (p := p) hp a b = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]

Premises used: Int.fract, toIocDiv_eq_neg_floor, toIocMod