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 c : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃
h₃₂₁ : btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (z_1 : α) (h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃)
    (h₃₂₁ : btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)),
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ (↑z : α ⧸ AddSubgroup.zmultiples p) = x₂ ∨ x₂ = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₂ using QuotientAddGroup.induction_on
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
h₁₂₃ : btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃
h₃₂₁ : btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
H :
  ∀ (z_2 : α)
    (h₁₂₃ :
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p))
    (h₃₂₁ :
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
        (↑z : α ⧸ AddSubgroup.zmultiples p)),
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
        Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
          (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) = x₃ ∨ x₃ = (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₃ using QuotientAddGroup.induction_on
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [btw_cyclic] at h₃₂₁

Premises used: btw_cyclic
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
⊢ toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2

Tactic:
simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁

Premises used: QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p)
h₃₂₁ :
  btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
    (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
h₁₂₄ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
⊢ toIcoMod (p := p) ⋯ z z_2 ≤ toIocMod (p := p) ⋯ z z_1

Tactic:
simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁

Premises used: QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
h₃₂₁ : toIcoMod (p := p) ⋯ z z_2 ≤ toIocMod (p := p) ⋯ z z_1
H : z ≡ z_1 [PMOD p] ∨ z_1 ≡ z_2 [PMOD p] ∨ z_2 ≡ z [PMOD p]
⊢ Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) ∨
    Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      Eq (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [← modEq_iff_eq_mod_zmultiples]

Premises used: AddCommGroup.modEq_iff_eq_mod_zmultiples
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
h₁₂₃ : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2
h₃₂₁ : toIcoMod (p := p) ⋯ z z_2 ≤ toIocMod (p := p) ⋯ z z_1
⊢ z ≡ z_1 [PMOD p] ∨ z_1 ≡ z_2 [PMOD p] ∨ z_2 ≡ z [PMOD p]

Tactic:
simpa only [modEq_comm] using toIxxMod_antisymm _ h₁₂₃ h₃₂₁

Premises used: _private.0.toIxxMod_antisymm, AddCommGroup.modEq_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 : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
H : ∀ (z : α), btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∨ btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw x₁ x₂ x₃ ∨ btw x₃ x₂ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
x₂ x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z : α
H :
  ∀ (z_1 : α),
    btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∨
      btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ∨ btw x₃ x₂ (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₂ using QuotientAddGroup.induction_on
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
x₃ : HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)
z z_1 : α
H :
  ∀ (z_2 : α),
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p)
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
      btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
        (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)
⊢ btw (↑z : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) x₃ ∨
    btw x₃ (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
induction x₃ using QuotientAddGroup.induction_on
-- 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 : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
H : toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2 ∨ toIcoMod (p := p) ⋯ z_2 z_1 ≤ toIocMod (p := p) ⋯ z_2 z
⊢ btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p)) (↑z : α ⧸ AddSubgroup.zmultiples p)
      (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z_2 : α ⧸ AddSubgroup.zmultiples p) ∨
    btw (α := HasQuotient.Quotient α (B := AddSubgroup α) (AddSubgroup.zmultiples p))
      (↑z_2 : α ⧸ AddSubgroup.zmultiples p) (↑z_1 : α ⧸ AddSubgroup.zmultiples p) (↑z : α ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [btw_coe_iff]

Premises used: QuotientAddGroup.btw_coe_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 c : α
n : ℤ
hp' : Fact (0 < p)
z z_1 z_2 : α
⊢ toIcoMod (p := p) ⋯ z z_1 ≤ toIocMod (p := p) ⋯ z z_2 ∨ toIcoMod (p := p) ⋯ z_2 z_1 ≤ toIocMod (p := p) ⋯ z_2 z

Tactic:
apply toIxxMod_total

Premises used: _private.0.toIxxMod_total
-- 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
⊢ b - (↑(toIcoDiv hp a b) : R) * p = toIcoMod hp a b

Tactic:
simpa using self_sub_toIcoDiv_zsmul hp a b

Premises used: self_sub_toIcoDiv_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
⊢ b - (↑(toIocDiv hp a b) : R) * p = toIocMod hp a b

Tactic:
simpa using self_sub_toIocDiv_zsmul hp a b

Premises used: self_sub_toIocDiv_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
⊢ (↑(toIcoDiv hp a b) : R) * p - b = -toIcoMod hp a b

Tactic:
simpa using toIcoDiv_zsmul_sub_self hp a b

Premises used: toIcoDiv_zsmul_sub_self
-- 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
⊢ (↑(toIocDiv hp a b) : R) * p - b = -toIocMod hp a b

Tactic:
simpa using toIocDiv_zsmul_sub_self hp a b

Premises used: toIocDiv_zsmul_sub_self
-- 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
⊢ toIcoMod hp a b - b = -(↑(toIcoDiv hp a b) : R) * p

Tactic:
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
⊢ toIocMod hp a b - b = -(↑(toIocDiv hp a b) : R) * p

Tactic:
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
⊢ b - toIcoMod hp a b = (↑(toIcoDiv hp a b) : R) * p

Tactic:
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
⊢ b - toIocMod hp a b = (↑(toIocDiv hp a b) : R) * p

Tactic:
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
⊢ toIcoMod hp a b + (↑(toIcoDiv hp a b) : R) * p = b

Tactic:
simpa using toIcoMod_add_toIcoDiv_zsmul hp a b

Premises used: toIcoMod_add_toIcoDiv_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
⊢ toIocMod hp a b + (↑(toIocDiv hp a b) : R) * p = b

Tactic:
simpa using toIocMod_add_toIocDiv_zsmul hp a b

Premises used: toIocMod_add_toIocDiv_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
rw : toIcoMod hp a b + (↑(toIcoDiv hp a b) : R) * p = b
rw₁ rw₂ : b = b
⊢ (↑(toIcoDiv hp a b) : R) * p + toIcoMod hp a b = b

Tactic:
rw [add_comm, toIcoMod_add_toIcoDiv_mul]

Premises used: add_comm, toIcoMod_add_toIcoDiv_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
rw : toIocMod hp a b + (↑(toIocDiv hp a b) : R) * p = b
rw₁ rw₂ : b = b
⊢ (↑(toIocDiv hp a b) : R) * p + toIocMod hp a b = b

Tactic:
rw [add_comm, toIocMod_add_toIocDiv_mul]

Premises used: add_comm, toIocMod_add_toIocDiv_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 : ℤ
⊢ toIcoDiv hp a (b + (↑m : R) * p) = toIcoDiv hp a b + m

Tactic:
simpa using toIcoDiv_add_zsmul hp a b m

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

Tactic:
mod_cast toIcoDiv_add_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, toIcoDiv.congr_simp, toIcoDiv, Nat.cast, HAdd.hAdd, toIcoDiv_add_intCast_mul, 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
⊢ toIcoDiv hp a (b + OfNat.ofNat m * p) = toIcoDiv hp a b + OfNat.ofNat m

Tactic:
toIcoDiv_add_natCast_mul hp a b m

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

Tactic:
simpa using toIcoDiv_add_zsmul' hp a b m

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

Tactic:
mod_cast toIcoDiv_add_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, toIcoDiv_add_intCast_mul', HMul.hMul, congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Nat.cast, HAdd.hAdd, 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
⊢ toIcoDiv hp (a + OfNat.ofNat m * p) b = toIcoDiv hp a b - OfNat.ofNat m

Tactic:
toIcoDiv_add_natCast_mul' hp a b m

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

Tactic:
simpa using toIocDiv_add_zsmul hp a b m

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

Tactic:
mod_cast toIocDiv_add_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, toIocDiv_add_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 (b + OfNat.ofNat m * p) = toIocDiv hp a b + OfNat.ofNat m

Tactic:
toIocDiv_add_natCast_mul hp a b m

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

Tactic:
simpa using toIocDiv_add_zsmul' hp a b m

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

Tactic:
mod_cast toIocDiv_add_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, toIocDiv_add_intCast_mul', congrArg, HSub.hSub, cast, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, 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_add_natCast_mul' hp a b m

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

Tactic:
simpa using toIcoDiv_zsmul_add hp a b m

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

Tactic:
mod_cast toIcoDiv_intCast_mul_add hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, toIcoDiv_intCast_mul_add, congrArg, cast, toIcoDiv.congr_simp, toIcoDiv, Nat.cast, HAdd.hAdd, 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
⊢ toIcoDiv hp a (OfNat.ofNat m * p + b) = OfNat.ofNat m + toIcoDiv hp a b

Tactic:
toIcoDiv_natCast_mul_add hp a b m

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

Tactic:
simpa using toIocDiv_zsmul_add hp a b m

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

Tactic:
mod_cast toIocDiv_intCast_mul_add hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, toIocDiv.congr_simp, Nat.cast, HAdd.hAdd, toIocDiv_intCast_mul_add, 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) = OfNat.ofNat m + toIocDiv hp a b

Tactic:
toIocDiv_natCast_mul_add hp a b m

Premises used: toIocDiv_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 : ℤ
⊢ toIcoDiv hp a (b - (↑m : R) * p) = toIcoDiv hp a b - m

Tactic:
simpa using toIcoDiv_sub_zsmul hp a b m

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

Tactic:
mod_cast toIcoDiv_sub_intCast_mul hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Nat.cast, Eq.refl, congrFun', toIcoDiv_sub_intCast_mul, 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
⊢ toIcoDiv hp a (b - OfNat.ofNat m * p) = toIcoDiv hp a b - OfNat.ofNat m

Tactic:
toIcoDiv_sub_natCast_mul hp a b m

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

Tactic:
simpa using toIcoDiv_sub_zsmul' hp a b m

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

Tactic:
mod_cast toIcoDiv_sub_intCast_mul' hp a b m

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, toIcoDiv_sub_intCast_mul', congrArg, HSub.hSub, cast, toIcoDiv.congr_simp, toIcoDiv, Nat.cast, HAdd.hAdd, 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
⊢ toIcoDiv hp (a - OfNat.ofNat m * p) b = toIcoDiv hp a b + OfNat.ofNat m

Tactic:
toIcoDiv_sub_natCast_mul' hp a b m

Premises used: toIcoDiv_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 (b - (↑m : R) * p) = toIocDiv hp a b - m

Tactic:
simpa using toIocDiv_sub_zsmul hp a b m

Premises used: toIocDiv_sub_zsmul