Wrap

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

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'

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'

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'

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'

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'

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

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')

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')

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')

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

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')

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')

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')

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

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

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

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

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

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

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

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

Lower and upper bounds

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

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

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

theorem Lean.Grind.ToInt.ge_lower' {α : Type u_1} {i : IntInterval} [ToInt α i] (lo : Int) (h : i.lo? = some lo) (a : α) : lo ≤ ↑a

theorem Lean.Grind.ToInt.le_upper' {α : Type u_1} {i : IntInterval} [ToInt α i] (hi : Int) (h : i.hi? = some hi) (a : α) : ↑a + 1 ≤ hi