Init.Omega.Int

Lean.Omega.Int.ofNat_pow theorem

(a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b

Full source

theorem ofNat_pow (a b : Nat) : ((a ^ b : Nat) : Int) = (a : Int) ^ b := by
  induction b with
  | zero => rfl
  | succ b ih => rw [Nat.pow_succ, Int.ofNat_mul, ih]; rfl

Power Preservation under Natural-to-Integer Cast: $(a^b : \mathbb{Z}) = (a : \mathbb{Z})^b$

Informal description

For any natural numbers $a$ and $b$, the integer cast of $a^b$ is equal to the $b$-th power of the integer cast of $a$. That is, $(a^b : \mathbb{Z}) = (a : \mathbb{Z})^b$.

Lean.Omega.Int.pos_pow_of_pos theorem

(a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b

Full source

theorem pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b := by
  rw [Int.eq_natAbs_of_nonneg (Int.le_of_lt h), ← Int.ofNat_zero, ← Int.ofNat_pow, Int.ofNat_lt]
  exact Nat.pow_pos (Int.natAbs_pos.mpr (Int.ne_of_gt h))

Positivity of Integer Powers with Positive Base: $0 < a \implies 0 < a^b$

Informal description

For any integer $a$ and natural number $b$, if $0 < a$, then $0 < a^b$.

Lean.Omega.Int.ofNat_pos theorem

{a : Nat} : 0 < (a : Int) ↔ 0 < a

Full source

theorem ofNat_pos {a : Nat} : 0 < (a : Int) ↔ 0 < a := by
  rw [← Int.ofNat_zero, Int.ofNat_lt]

Positivity Preservation under Natural-to-Integer Cast

Informal description

For any natural number $a$, the integer cast of $a$ is positive if and only if $a$ is positive. That is, $0 < (a : \mathbb{Z}) \leftrightarrow 0 < a$.

Lean.Omega.Int.ofNat_pos_of_pos theorem

{a : Nat} (h : 0 < a) : 0 < (a : Int)

Full source

theorem ofNat_pos_of_pos {a : Nat} (h : 0 < a) : 0 < (a : Int) :=
  ofNat_pos.mpr h

Positivity Preservation under Natural-to-Integer Cast for Positive Natural Numbers

Informal description

For any natural number $a$, if $0 < a$, then the integer cast of $a$ is positive, i.e., $0 < (a : \mathbb{Z})$.

Lean.Omega.Int.natCast_ofNat theorem

{x : Nat} : @Nat.cast Int instNatCastInt (no_index (OfNat.ofNat x)) = OfNat.ofNat x

Full source

theorem natCast_ofNat {x : Nat} :
    @Nat.cast Int instNatCastInt (no_index (OfNat.ofNat x)) = OfNat.ofNat x := rfl

Equality of Natural and Integer Casts for Numeric Literals

Informal description

For any natural number $x$, the integer cast of $x$ (interpreted as a natural number via `OfNat`) is equal to $x$ interpreted directly as an integer via `OfNat`.

Lean.Omega.Int.ofNat_lt_of_lt theorem

{x y : Nat} (h : x < y) : (x : Int) < (y : Int)

Full source

theorem ofNat_lt_of_lt {x y : Nat} (h : x < y) : (x : Int) < (y : Int) :=
  Int.ofNat_lt.mpr h

Strict Order Preservation of Natural-to-Integer Cast

Informal description

For any natural numbers $x$ and $y$, if $x < y$, then the integer cast of $x$ is strictly less than the integer cast of $y$.

Lean.Omega.Int.ofNat_le_of_le theorem

{x y : Nat} (h : x ≤ y) : (x : Int) ≤ (y : Int)

Full source

theorem ofNat_le_of_le {x y : Nat} (h : x ≤ y) : (x : Int) ≤ (y : Int) :=
  Int.ofNat_le.mpr h

Monotonicity of Natural-to-Integer Cast with Respect to Order

Informal description

For any natural numbers $x$ and $y$, if $x \leq y$, then the integer cast of $x$ is less than or equal to the integer cast of $y$.

Lean.Omega.Int.ofNat_shiftLeft_eq theorem

{x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y : Nat)

Full source

theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y : Nat) := by
  simp [Nat.shiftLeft_eq]

Left Shift of Natural Numbers Cast to Integers Equals Multiplication by Power of Two

Informal description

For any natural numbers $x$ and $y$, the integer cast of the left shift operation $x \ll y$ equals the integer cast of $x$ multiplied by $2^y$, i.e., $(x \ll y : \mathbb{Z}) = (x : \mathbb{Z}) \cdot 2^y$.

Lean.Omega.Int.ofNat_shiftRight_eq_div_pow theorem

{x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat)

Full source

theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
  simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]

Right Shift Equals Division by Power of Two in Integer Cast

Informal description

For any natural numbers $x$ and $y$, the integer value obtained by right-shifting $x$ by $y$ bits is equal to the integer division of $x$ by $2^y$. That is, $(x \gg y)_{\mathbb{Z}} = \lfloor x / 2^y \rfloor$.

Lean.Omega.Int.emod_ofNat_nonneg theorem

{x : Nat} {y : Int} : 0 ≤ (x : Int) % y

Full source

theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
  Int.ofNat_zero_le _

Non-Negativity of Natural Number Modulo Integer

Informal description

For any natural number $x$ and integer $y$, the modulo operation $(x \bmod y)$ yields a non-negative result, i.e., $0 \leq (x \bmod y)$.

Lean.Omega.Int.lt_of_not_ge theorem

{x y : Int} (h : ¬(x ≤ y)) : y < x

Full source

theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h

Strict Inequality from Negation of Non-Strict Inequality in Integers

Informal description

For any integers $x$ and $y$, if $x$ is not greater than or equal to $y$ (i.e., $\neg (x \geq y)$), then $y < x$.

Lean.Omega.Int.lt_of_not_le theorem

{x y : Int} (h : ¬(x ≤ y)) : y < x

Full source

theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h

Strict Inequality from Negation of Non-Strict Inequality in Integers

Informal description

For any integers $x$ and $y$, if $x$ is not less than or equal to $y$ (i.e., $\neg (x \leq y)$), then $y$ is strictly less than $x$ (i.e., $y < x$).

Lean.Omega.Int.not_le_of_lt theorem

{x y : Int} (h : y < x) : ¬(x ≤ y)

Full source

theorem not_le_of_lt {x y : Int} (h : y < x) : ¬ (x ≤ y) := Int.not_le.mpr h

Negation of Non-Strict Inequality from Strict Inequality in Integers

Informal description

For any integers $x$ and $y$, if $y < x$, then it is not true that $x \leq y$.

Lean.Omega.Int.lt_le_asymm theorem

{x y : Int} (h₁ : y < x) (h₂ : x ≤ y) : False

Full source

theorem lt_le_asymm {x y : Int} (h₁ : y < x) (h₂ : x ≤ y) : False := Int.not_le.mpr h₁ h₂

Asymmetry of Strict and Non-Strict Inequality on Integers

Informal description

For any integers $x$ and $y$, if $y < x$ and $x \leq y$, then we obtain a contradiction (False).

Lean.Omega.Int.le_lt_asymm theorem

{x y : Int} (h₁ : y ≤ x) (h₂ : x < y) : False

Full source

theorem le_lt_asymm {x y : Int} (h₁ : y ≤ x) (h₂ : x < y) : False := Int.not_lt.mpr h₁ h₂

Asymmetry of $\leq$ and $<$ on integers

Informal description

For any integers $x$ and $y$, if $y \leq x$ and $x < y$, then we obtain a contradiction (False).

Lean.Omega.Int.le_of_not_gt theorem

{x y : Int} (h : ¬(y > x)) : y ≤ x

Full source

theorem le_of_not_gt {x y : Int} (h : ¬ (y > x)) : y ≤ x := Int.not_lt.mp h

Non-strict inequality from negation of strict inequality in integers

Informal description

For any integers $x$ and $y$, if it is not the case that $y > x$, then $y \leq x$.

Lean.Omega.Int.not_lt_of_ge theorem

{x y : Int} (h : y ≥ x) : ¬(y < x)

Full source

theorem not_lt_of_ge {x y : Int} (h : y ≥ x) : ¬ (y < x) := Int.not_lt.mpr h

Negation of Strict Inequality from Non-Strict Inequality in Integers

Informal description

For any integers $x$ and $y$, if $y \geq x$, then it is not the case that $y < x$.

Lean.Omega.Int.le_of_not_lt theorem

{x y : Int} (h : ¬(x < y)) : y ≤ x

Full source

theorem le_of_not_lt {x y : Int} (h : ¬ (x < y)) : y ≤ x := Int.not_lt.mp h

Non-strict inequality from negation of strict inequality in integers

Informal description

For any integers $x$ and $y$, if it is not the case that $x < y$, then $y \leq x$.

Lean.Omega.Int.not_lt_of_le theorem

{x y : Int} (h : y ≤ x) : ¬(x < y)

Full source

theorem not_lt_of_le {x y : Int} (h : y ≤ x) : ¬ (x < y) := Int.not_lt.mpr h

Negation of Strict Inequality from Non-Strict Inequality in Integers

Informal description

For any integers $x$ and $y$, if $y \leq x$, then it is not the case that $x < y$.

Lean.Omega.Int.add_congr theorem

{a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d

Full source

theorem add_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d := by
  subst h₁; subst h₂; rfl

Addition Preserves Equality for Integers

Informal description

For any integers $a, b, c, d$, if $a = b$ and $c = d$, then $a + c = b + d$.

Lean.Omega.Int.mul_congr theorem

{a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d

Full source

theorem mul_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d := by
  subst h₁; subst h₂; rfl

Multiplication Preserves Equality for Integers

Informal description

For any integers $a, b, c, d$, if $a = b$ and $c = d$, then $a \cdot c = b \cdot d$.

Lean.Omega.Int.mul_congr_left theorem

{a b : Int} (h₁ : a = b) (c : Int) : a * c = b * c

Full source

theorem mul_congr_left {a b : Int} (h₁ : a = b)  (c : Int) : a * c = b * c := by
  subst h₁; rfl

Left Multiplication Preserves Equality for Integers

Informal description

For any integers $a$ and $b$ such that $a = b$, and for any integer $c$, it holds that $a \cdot c = b \cdot c$.

Lean.Omega.Int.sub_congr theorem

{a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d

Full source

theorem sub_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d := by
  subst h₁; subst h₂; rfl

Subtraction Preserves Equality for Integers

Informal description

For any integers $a, b, c, d$, if $a = b$ and $c = d$, then $a - c = b - d$.

Lean.Omega.Int.neg_congr theorem

{a b : Int} (h₁ : a = b) : -a = -b

Full source

theorem neg_congr {a b : Int} (h₁ : a = b) : -a = -b := by
  subst h₁; rfl

Negation Preserves Equality for Integers

Informal description

For any integers $a$ and $b$ such that $a = b$, it holds that $-a = -b$.

Lean.Omega.Int.lt_of_gt theorem

{x y : Int} (h : x > y) : y < x

Full source

theorem lt_of_gt {x y : Int} (h : x > y) : y < x := gt_iff_lt.mp h

Less Than from Greater Than for Integers ($x > y \implies y < x$)

Informal description

For any integers $x$ and $y$, if $x > y$ then $y < x$.

Lean.Omega.Int.le_of_ge theorem

{x y : Int} (h : x ≥ y) : y ≤ x

Full source

theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h

Greater Than or Equal Implies Less Than or Equal (Flipped) for Integers

Informal description

For any integers $x$ and $y$, if $x \geq y$, then $y \leq x$.

Lean.Omega.Int.ofNat_mul_nonneg theorem

{a b : Nat} : 0 ≤ (a : Int) * b

Full source

theorem ofNat_mul_nonneg {a b : Nat} : 0 ≤ (a : Int) * b := by
  rw [← Int.ofNat_mul]
  exact Int.ofNat_zero_le (a * b)

Nonnegativity of Natural Number Multiplication in Integers

Informal description

For any natural numbers $a$ and $b$, the product of $a$ (cast to an integer) and $b$ is nonnegative, i.e., $0 \leq (a : \mathbb{Z}) * b$.

Lean.Omega.Int.ofNat_sub_eq_zero theorem

{b a : Nat} (h : ¬b ≤ a) : ((a - b : Nat) : Int) = 0

Full source

theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 :=
  Int.ofNat_eq_zero.mpr (Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.not_le.mp h)))

Truncated Subtraction of Natural Numbers Cast to Integers Yields Zero When Subtrahend Exceeds Minuend

Informal description

For any natural numbers $a$ and $b$, if $b$ is not less than or equal to $a$ (i.e., $a < b$), then the integer obtained by casting the truncated subtraction $a - b$ from natural numbers to integers equals zero, i.e., $(a - b : \mathbb{N}) : \mathbb{Z} = 0$.

Lean.Omega.Int.ofNat_sub_dichotomy theorem

{a b : Nat} : b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0

Full source

theorem ofNat_sub_dichotomy {a b : Nat} :
    b ≤ a ∧ ((a - b : Nat) : Int) = a - bb ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0 := by
  by_cases h : b ≤ a
  · left
    have t := Int.ofNat_sub h
    simp at t
    exact ⟨h, t⟩
  · right
    have t := Nat.not_le.mp h
    simp [Int.ofNat_sub_eq_zero h]
    exact t

Dichotomy of Natural Number Subtraction Cast to Integers: $(a - b : \mathbb{N}) : \mathbb{Z} = a - b$ or $0$

Informal description

For any natural numbers $a$ and $b$, exactly one of the following holds: 1. $b \leq a$ and the integer obtained by casting the truncated subtraction $(a - b)$ equals the integer subtraction $(a - b)$, or 2. $a < b$ and the integer obtained by casting the truncated subtraction $(a - b)$ equals zero.

Lean.Omega.Int.ofNat_congr theorem

{a b : Nat} (h : a = b) : (a : Int) = (b : Int)

Full source

theorem ofNat_congr {a b : Nat} (h : a = b) : (a : Int) = (b : Int) := congrArg _ h

Embedding of Natural Numbers into Integers Preserves Equality

Informal description

For any natural numbers $a$ and $b$, if $a = b$, then their canonical embeddings into the integers are also equal, i.e., $(a : \mathbb{Z}) = (b : \mathbb{Z})$.

Lean.Omega.Int.ofNat_sub_sub theorem

{a b c : Nat} : ((a - b - c : Nat) : Int) = ((a - (b + c) : Nat) : Int)

Full source

theorem ofNat_sub_sub {a b c : Nat} : ((a - b - c : Nat) : Int) = ((a - (b + c) : Nat) : Int) :=
  congrArg _ (Nat.sub_sub _ _ _)

Embedding Preserves Nested Truncated Subtraction of Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the canonical embedding into the integers of the truncated subtraction $(a - b - c)$ is equal to the embedding of $(a - (b + c))$. That is, $(a - b - c : \mathbb{Z}) = (a - (b + c) : \mathbb{Z})$.

Lean.Omega.Int.ofNat_min theorem

(a b : Nat) : ((min a b : Nat) : Int) = min (a : Int) (b : Int)

Full source

theorem ofNat_min (a b : Nat) : ((min a b : Nat) : Int) = min (a : Int) (b : Int) := by
  simp only [Nat.min_def, Int.min_def, Int.ofNat_le]
  split <;> rfl

Embedding Preserves Minimum of Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the canonical embedding into the integers of their minimum $\min(a, b)$ is equal to the minimum of their embeddings, i.e., $(\min(a, b) : \mathbb{Z}) = \min(a : \mathbb{Z}, b : \mathbb{Z})$.

Lean.Omega.Int.ofNat_max theorem

(a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int)

Full source

theorem ofNat_max (a b : Nat) : ((max a b : Nat) : Int) = max (a : Int) (b : Int) := by
  simp only [Nat.max_def, Int.max_def, Int.ofNat_le]
  split <;> rfl

Embedding Preserves Maximum of Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the canonical embedding into the integers of their maximum $\max(a, b)$ is equal to the maximum of their embeddings, i.e., $(\max(a, b) : \mathbb{Z}) = \max(a : \mathbb{Z}, b : \mathbb{Z})$.

Lean.Omega.Int.ofNat_natAbs theorem

(a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a

Full source

theorem ofNat_natAbs (a : Int) : (a.natAbs : Int) = if 0 ≤ a then a else -a := by
  rw [Int.natAbs.eq_def]
  split <;> rename_i n
  · simp only [Int.ofNat_eq_coe]
    rw [if_pos (Int.ofNat_nonneg n)]
  · simp; rfl

Natural Absolute Value Embedding: $|a|_{\mathbb{N}} = \text{if } a \geq 0 \text{ then } a \text{ else } -a$

Informal description

For any integer $a$, the canonical embedding of the natural number absolute value of $a$ into the integers equals $a$ if $a$ is non-negative, and $-a$ otherwise. That is, $|a|_{\mathbb{N}} = \text{if } 0 \leq a \text{ then } a \text{ else } -a$.

Lean.Omega.Int.natAbs_dichotomy theorem

{a : Int} : 0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a

Full source

theorem natAbs_dichotomy {a : Int} : 0 ≤ a ∧ a.natAbs = a0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a := by
  by_cases h : 0 ≤ a
  · left
    simp_all [Int.natAbs_of_nonneg]
  · right
    rw [Int.not_le] at h
    rw [Int.ofNat_natAbs_of_nonpos (Int.le_of_lt h)]
    simp_all

Dichotomy of Natural Absolute Value for Integers

Informal description

For any integer $a$, either $a$ is non-negative and its natural absolute value equals $a$, or $a$ is negative and its natural absolute value equals $-a$. In other words, $a \geq 0 \land |a|_{\mathbb{N}} = a$ or $a < 0 \land |a|_{\mathbb{N}} = -a$.

Lean.Omega.Int.neg_le_natAbs theorem

{a : Int} : -a ≤ a.natAbs

Full source

theorem neg_le_natAbs {a : Int} : -a ≤ a.natAbs := by
  have t := Int.le_natAbs (a := -a)
  simp at t
  exact t

Negation Bounded by Natural Absolute Value in Integers

Informal description

For any integer $a$, the negation of $a$ is less than or equal to the natural number absolute value of $a$, i.e., $-a \leq |a|_{\mathbb{N}}$.

Lean.Omega.Int.add_le_iff_le_sub theorem

{a b c : Int} : a + b ≤ c ↔ a ≤ c - b

Full source

theorem add_le_iff_le_sub {a b c : Int} : a + b ≤ c ↔ a ≤ c - b := by
  conv =>
    lhs
    rw [← Int.add_zero c, ← Int.sub_self (-b), Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_neg,
      Int.add_le_add_iff_right]
  rfl

Integer Inequality: $a + b \leq c \leftrightarrow a \leq c - b$

Informal description

For any integers $a$, $b$, and $c$, the inequality $a + b \leq c$ holds if and only if $a \leq c - b$ holds.

Lean.Omega.Int.le_add_iff_sub_le theorem

{a b c : Int} : a ≤ b + c ↔ a - c ≤ b

Full source

theorem le_add_iff_sub_le {a b c : Int} : a ≤ b + c ↔ a - c ≤ b := by
  conv =>
    lhs
    rw [← Int.neg_neg c, Int.add_neg_eq_sub, ← add_le_iff_le_sub]
  rfl

Integer Inequality: $a \leq b + c \leftrightarrow a - c \leq b$

Informal description

For any integers $a$, $b$, and $c$, the inequality $a \leq b + c$ holds if and only if $a - c \leq b$ holds.

Lean.Omega.Int.add_le_zero_iff_le_neg theorem

{a b : Int} : a + b ≤ 0 ↔ a ≤ -b

Full source

theorem add_le_zero_iff_le_neg {a b : Int} : a + b ≤ 0 ↔ a ≤ - b := by
  rw [add_le_iff_le_sub, Int.zero_sub]

Integer Inequality: $a + b \leq 0 \leftrightarrow a \leq -b$

Informal description

For any integers $a$ and $b$, the inequality $a + b \leq 0$ holds if and only if $a \leq -b$.

Lean.Omega.Int.add_le_zero_iff_le_neg' theorem

{a b : Int} : a + b ≤ 0 ↔ b ≤ -a

Full source

theorem add_le_zero_iff_le_neg' {a b : Int} : a + b ≤ 0 ↔ b ≤ -a := by
  rw [Int.add_comm, add_le_zero_iff_le_neg]

Integer Inequality: $a + b \leq 0 \leftrightarrow b \leq -a$

Informal description

For any integers $a$ and $b$, the inequality $a + b \leq 0$ holds if and only if $b \leq -a$.

Lean.Omega.Int.add_nonnneg_iff_neg_le theorem

{a b : Int} : 0 ≤ a + b ↔ -b ≤ a

Full source

theorem add_nonnneg_iff_neg_le {a b : Int} : 0 ≤ a + b ↔ -b ≤ a := by
  rw [le_add_iff_sub_le, Int.zero_sub]

Non-negative Sum Condition: $0 \leq a + b \leftrightarrow -b \leq a$

Informal description

For any integers $a$ and $b$, the inequality $0 \leq a + b$ holds if and only if $-b \leq a$.

Lean.Omega.Int.add_nonnneg_iff_neg_le' theorem

{a b : Int} : 0 ≤ a + b ↔ -a ≤ b

Full source

theorem add_nonnneg_iff_neg_le' {a b : Int} : 0 ≤ a + b ↔ -a ≤ b := by
  rw [Int.add_comm, add_nonnneg_iff_neg_le]

Non-negative Sum Condition (Symmetric Form): $0 \leq a + b \leftrightarrow -a \leq b$

Informal description

For any integers $a$ and $b$, the inequality $0 \leq a + b$ holds if and only if $-a \leq b$.

Lean.Omega.Int.ofNat_fst_mk theorem

{β} {x : Nat} {y : β} : (Prod.mk x y).fst = (x : Int)

Full source

theorem ofNat_fst_mk {β} {x : Nat} {y : β} : (Prod.mk x y).fst = (x : Int) := rfl

First Projection of Pair with Natural Number Equals Integer Cast

Informal description

For any natural number $x$ and any element $y$ of type $\beta$, the first projection of the pair $(x, y)$ is equal to the integer cast of $x$, i.e., $(\mathrm{mk}\ x\ y).\mathrm{fst} = (x : \mathbb{Z})$.

Lean.Omega.Int.ofNat_snd_mk theorem

{α} {x : α} {y : Nat} : (Prod.mk x y).snd = (y : Int)

Full source

theorem ofNat_snd_mk {α} {x : α} {y : Nat} : (Prod.mk x y).snd = (y : Int) := rfl

Second Projection of Pair with Natural Number Equals Integer Cast

Informal description

For any element $x$ of type $\alpha$ and any natural number $y$, the second projection of the pair $(x, y)$ is equal to the integer cast of $y$, i.e., $(\mathrm{mk}\ x\ y).\mathrm{snd} = (y : \mathbb{Z})$.

Lean.Omega.Nat.lt_of_gt theorem

{x y : Nat} (h : x > y) : y < x

Full source

theorem lt_of_gt {x y : Nat} (h : x > y) : y < x := gt_iff_lt.mp h

$x > y$ implies $y < x$ for natural numbers

Informal description

For any natural numbers $x$ and $y$, if $x > y$ then $y < x$.

Lean.Omega.Nat.le_of_ge theorem

{x y : Nat} (h : x ≥ y) : y ≤ x

Full source

theorem le_of_ge {x y : Nat} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h

Inequality Reversal for Natural Numbers: $x \geq y \implies y \leq x$

Informal description

For any natural numbers $x$ and $y$, if $x \geq y$ then $y \leq x$.

Lean.Omega.Fin.ne_iff_lt_or_gt theorem

{i j : Fin n} : i ≠ j ↔ i < j ∨ i > j

Full source

theorem ne_iff_lt_or_gt {i j : Fin n} : i ≠ ji ≠ j ↔ i < j ∨ i > j := by
  cases i; cases j; simp only [ne_eq, Fin.mk.injEq, Nat.ne_iff_lt_or_gt, gt_iff_lt]; rfl

Inequality in Finite Types is Equivalent to Strict Ordering: $i \neq j \leftrightarrow i < j \lor i > j$

Informal description

For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, the inequality $i \neq j$ holds if and only if either $i < j$ or $i > j$.

Lean.Omega.Fin.lt_or_gt_of_ne theorem

{i j : Fin n} (h : i ≠ j) : i < j ∨ i > j

Full source

protected theorem lt_or_gt_of_ne {i j : Fin n} (h : i ≠ j) : i < j ∨ i > j := Fin.ne_iff_lt_or_gt.mp h

Strict Ordering of Distinct Elements in Finite Types: $i \neq j \implies i < j \lor i > j$

Informal description

For any two distinct elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$ (i.e., $i \neq j$), either $i$ is strictly less than $j$ or $i$ is strictly greater than $j$.

Lean.Omega.Fin.not_le theorem

{i j : Fin n} : ¬i ≤ j ↔ j < i

Full source

theorem not_le {i j : Fin n} : ¬ i ≤ j¬ i ≤ j ↔ j < i := by
  cases i; cases j; exact Nat.not_le

Negation of Order in Finite Types: $\neg (i \leq j) \leftrightarrow j < i$

Informal description

For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, the statement that $i$ is not less than or equal to $j$ is equivalent to the statement that $j$ is strictly less than $i$, i.e., $\neg (i \leq j) \leftrightarrow j < i$.

Lean.Omega.Fin.not_lt theorem

{i j : Fin n} : ¬i < j ↔ j ≤ i

Full source

theorem not_lt {i j : Fin n} : ¬ i < j¬ i < j ↔ j ≤ i := by
  cases i; cases j; exact Nat.not_lt

Negation of Strict Order in Finite Types: $\neg (i < j) \leftrightarrow j \leq i$

Informal description

For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, the statement $\neg (i < j)$ holds if and only if $j \leq i$.

Lean.Omega.Fin.lt_of_not_le theorem

{i j : Fin n} (h : ¬i ≤ j) : j < i

Full source

protected theorem lt_of_not_le {i j : Fin n} (h : ¬ i ≤ j) : j < i := Fin.not_le.mp h

Strict Order from Negated Non-Strict Order in Finite Types

Informal description

For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, if $i$ is not less than or equal to $j$, then $j$ is strictly less than $i$.

Lean.Omega.Fin.le_of_not_lt theorem

{i j : Fin n} (h : ¬i < j) : j ≤ i

Full source

protected theorem le_of_not_lt {i j : Fin n} (h : ¬ i < j) : j ≤ i := Fin.not_lt.mp h

Non-strict Order from Negation of Strict Order in Finite Types: $\neg (i < j) \to j \leq i$

Informal description

For any two elements $i$ and $j$ of the finite type $\mathrm{Fin}\,n$, if it is not the case that $i < j$, then $j \leq i$.

Lean.Omega.Fin.ofNat_val_add theorem

{x y : Fin n} : (((x + y : Fin n)) : Int) = ((x : Int) + (y : Int)) % n

Full source

theorem ofNat_val_add {x y : Fin n} :
    (((x + y : Fin n)) : Int) = ((x : Int) + (y : Int)) % n := rfl

Modular Congruence of Finite Type Addition

Informal description

For any two elements $x$ and $y$ of the finite type $\text{Fin}\,n$, the integer value of their sum in $\text{Fin}\,n$ is congruent modulo $n$ to the sum of their integer values, i.e., $$(x + y)_{\mathbb{Z}} \equiv (x_{\mathbb{Z}} + y_{\mathbb{Z}}) \mod n.$$

Lean.Omega.Fin.ofNat_val_sub theorem

{x y : Fin n} : (((x - y : Fin n)) : Int) = (((n - y : Nat) + (x : Int) : Int)) % n

Full source

theorem ofNat_val_sub {x y : Fin n} :
    (((x - y : Fin n)) : Int) = (((n - y : Nat) + (x : Int) : Int)) % n := rfl

Modular Congruence of Finite Type Subtraction

Informal description

For any two elements $x$ and $y$ of the finite type $\text{Fin}\,n$, the integer value of their difference in $\text{Fin}\,n$ is congruent modulo $n$ to the sum of the integer value of $x$ and the natural number difference $(n - y)$, i.e., $$(x - y)_{\mathbb{Z}} \equiv \big((n - y)_{\mathbb{N}} + x_{\mathbb{Z}}\big) \mod n.$$

Lean.Omega.Fin.ofNat_val_mul theorem

{x y : Fin n} : (((x * y : Fin n)) : Int) = ((x : Int) * (y : Int)) % n

Full source

theorem ofNat_val_mul {x y : Fin n} :
    (((x * y : Fin n)) : Int) = ((x : Int) * (y : Int)) % n := rfl

Modular Congruence of Finite Type Multiplication

Informal description

For any two elements $x$ and $y$ of the finite type $\text{Fin}\,n$, the integer value of their product in $\text{Fin}\,n$ is congruent modulo $n$ to the product of their integer values, i.e., $$(x \cdot y)_{\mathbb{Z}} \equiv (x_{\mathbb{Z}} \cdot y_{\mathbb{Z}}) \mod n.$$

Lean.Omega.Fin.ofNat_val_natCast theorem

{n x y : Nat} (h : y = x % (n + 1)) : @Nat.cast Int instNatCastInt (@Fin.val (n + 1) (OfNat.ofNat x)) = OfNat.ofNat y

Full source

theorem ofNat_val_natCast {n x y : Nat} (h : y = x % (n + 1)):
    @Nat.cast Int instNatCastInt (@Fin.val (n + 1) (OfNat.ofNat x)) = OfNat.ofNat y := by
  rw [h]
  rfl

Integer Cast of Finite Natural Number Modulo $n+1$ Equals Remainder

Informal description

For any natural numbers $n$, $x$, and $y$ such that $y = x \bmod (n + 1)$, the integer value of the finite natural number $\text{Fin.val}(x)$ (viewed as an element of $\text{Fin}(n+1)$) is equal to the integer value of $y$, i.e., $$\text{Nat.cast}(\text{Fin.val}(x)) = y.$$

Lean.Omega.Prod.of_lex theorem

(w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd

Full source

theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd :=
  Prod.lex_def.mp w

Lexicographic Order Implies Componentwise Relation or Equality and Second Relation

Informal description

For any relations $r$ on $\alpha$ and $s$ on $\beta$, and any pairs $p = (a_1, b_1)$ and $q = (a_2, b_2)$ in $\alpha \times \beta$, if the lexicographic order $\mathrm{Prod.Lex}\,r\,s\,p\,q$ holds, then either: 1. $r\,a_1\,a_2$ holds, or 2. $a_1 = a_2$ and $s\,b_1\,b_2$ holds.

Lean.Omega.Prod.of_not_lex theorem

 {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop} {p q : α × β} (w : ¬Prod.Lex r s p q) :
  ¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)

Full source

theorem of_not_lex {α} {r : α → α → Prop} [DecidableEq α] {β} {s : β → β → Prop}
    {p q : α × β} (w : ¬ Prod.Lex r s p q) :
    ¬ r p.fst q.fst¬ r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬ s p.snd q.snd) := by
  rw [Prod.lex_def, not_or, Decidable.not_and_iff_not_or_not] at w
  exact w

Negation of Lexicographic Order on Pairs: $\neg(\mathrm{Prod.Lex}\,r\,s\,p\,q) \to \neg r\,a_1\,a_2 \land (a_1 \neq a_2 \lor \neg s\,b_1\,b_2)$

Informal description

For any type $\alpha$ with a decidable equality, any relation $r$ on $\alpha$, any type $\beta$, any relation $s$ on $\beta$, and any pairs $p = (a_1, b_1)$ and $q = (a_2, b_2)$ in $\alpha \times \beta$, if the lexicographic order $\mathrm{Prod.Lex}\,r\,s\,p\,q$ does not hold, then: 1. $r\,a_1\,a_2$ does not hold, and 2. either $a_1 \neq a_2$ or $s\,b_1\,b_2$ does not hold.

Lean.Omega.Prod.fst_mk theorem

: (Prod.mk x y).fst = x

Full source

theorem fst_mk : (Prod.mk x y).fst = x := rfl

First Projection of Pair Equals First Component

Informal description

For any elements $x$ and $y$, the first projection of the pair $(x, y)$ equals $x$, i.e., $(x, y).\text{fst} = x$.

Lean.Omega.Prod.snd_mk theorem

: (Prod.mk x y).snd = y

Full source

theorem snd_mk : (Prod.mk x y).snd = y := rfl

Second Projection of Pair Equals Second Component

Informal description

For any elements $x$ and $y$, the second projection of the pair $(x, y)$ equals $y$, i.e., $(x, y).\text{snd} = y$.