Wrap

source
theorem Lean.Grind.ToInt.of_eq_wrap_co_0 (i : IntInterval) (hi : Int) (h : i = IntInterval.co 0 hi) {a b : Int} :
a = i.wrap b → a = b % hi

Asserted propositions

source
theorem Lean.Grind.ToInt.of_eq {α : Type u_1} {i : IntInterval} [ToInt α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a = b → a' = b'
source
theorem Lean.Grind.ToInt.of_diseq {α : Type u_1} {i : IntInterval} [ToInt α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a ≠ b → a' ≠ b'
source
theorem Lean.Grind.ToInt.of_le {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.LE α] [LE α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a ≤ b → a' ≤ b'
source
theorem Lean.Grind.ToInt.of_not_le {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.LE α] [LE α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
¬a ≤ b → b' + 1 ≤ a'
source
theorem Lean.Grind.ToInt.of_lt {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.LT α] [LT α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
a < b → a' + 1 ≤ b'
source
theorem Lean.Grind.ToInt.of_not_lt {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.LT α] [LT α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
¬a < b → b' ≤ a'

Addition

source
theorem Lean.Grind.ToInt.add_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Add α] [Add α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a + b) = i.wrap (a' + b')
source
theorem Lean.Grind.ToInt.add_congr.ww {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Add α] [Add α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = i.wrap a') (h₂ : ↑b = i.wrap b') :
↑(a + b) = i.wrap (a' + b')
source
theorem Lean.Grind.ToInt.add_congr.wr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Add α] [Add α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = i.wrap b') :
↑(a + b) = i.wrap (a' + b')
source
theorem Lean.Grind.ToInt.add_congr.wl {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Add α] [Add α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = i.wrap a') (h₂ : ↑b = b') :
↑(a + b) = i.wrap (a' + b')

Multiplication

source
theorem Lean.Grind.ToInt.mul_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Mul α] [Mul α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a * b) = i.wrap (a' * b')
source
theorem Lean.Grind.ToInt.mul_congr.ww {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Mul α] [Mul α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = i.wrap a') (h₂ : ↑b = i.wrap b') :
↑(a * b) = i.wrap (a' * b')
source
theorem Lean.Grind.ToInt.mul_congr.wr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Mul α] [Mul α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = i.wrap b') :
↑(a * b) = i.wrap (a' * b')
source
theorem Lean.Grind.ToInt.mul_congr.wl {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Mul α] [Mul α i] (h : i.isFinite = true) {a b : α} {a' b' : Int} (h₁ : ↑a = i.wrap a') (h₂ : ↑b = b') :
↑(a * b) = i.wrap (a' * b')

Subtraction

source
theorem Lean.Grind.ToInt.sub_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Sub α] [Sub α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a - b) = i.wrap (a' - b')

Negation

source
theorem Lean.Grind.ToInt.neg_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Neg α] [Neg α i] {a : α} {a' : Int} (h₁ : ↑a = a') :
↑(-a) = i.wrap (-a')

Power

source
theorem Lean.Grind.ToInt.pow_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [HPow α Nat α] [Pow α i] {a : α} (k : Nat) (a' : Int) (h₁ : ↑a = a') :
↑(a ^ k) = i.wrap (a' ^ k)

Division

source
theorem Lean.Grind.ToInt.div_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Div α] [Div α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a / b) = a' / b'

Modulo

source
theorem Lean.Grind.ToInt.mod_congr {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Mod α] [Mod α i] {a b : α} {a' b' : Int} (h₁ : ↑a = a') (h₂ : ↑b = b') :
↑(a % b) = a' % b'

OfNat

source
theorem Lean.Grind.ToInt.ofNat_eq {α : Type u_1} {i : IntInterval} [ToInt α i] [(n : Nat) → _root_.OfNat α n] [OfNat α i] (n : Nat) :
↑(OfNat.ofNat n) = i.wrap ↑n

Zero

source
theorem Lean.Grind.ToInt.zero_eq {α : Type u_1} {i : IntInterval} [ToInt α i] [_root_.Zero α] [Zero α i] :
↑0 = 0

Lower and upper bounds

source
theorem Lean.Grind.ToInt.ge_lower {α : Type u_1} {i : IntInterval} [ToInt α i] (lo : Int) (h : (i.lo? == some lo) = true) (a : α) :
-1 * ↑a + lo ≤ 0
source
theorem Lean.Grind.ToInt.ge_lower0 {α : Type u_1} {i : IntInterval} [ToInt α i] (h : (i.lo? == some 0) = true) (a : α) :
-1 * ↑a ≤ 0
source
theorem Lean.Grind.ToInt.le_upper {α : Type u_1} {i : IntInterval} [ToInt α i] (hi' : Int) (h : (i.hi? == some (-hi' + 1)) = true) (a : α) :
↑a + hi' ≤ 0
source
theorem Lean.Grind.ToInt.ge_lower' {α : Type u_1} {i : IntInterval} [ToInt α i] (lo : Int) (h : i.lo? = some lo) (a : α) :
lo ≤ ↑a
source
theorem Lean.Grind.ToInt.le_upper' {α : Type u_1} {i : IntInterval} [ToInt α i] (hi : Int) (h : i.hi? = some hi) (a : α) :
↑a + 1 ≤ hi