norm_num extensions for inequalities.

def Mathlib.Meta.NormNum.inferOrderedSemiring {u : Lean.Level} (α : Q(Type u)) : Lean.MetaM Q(OrderedSemiring «$α»)

Helper function to synthesize a typed OrderedSemiring α expression.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.inferOrderedRing {u : Lean.Level} (α : Q(Type u)) : Lean.MetaM Q(OrderedRing «$α»)

Helper function to synthesize a typed OrderedRing α expression.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.inferLinearOrderedField {u : Lean.Level} (α : Q(Type u)) : Lean.MetaM Q(LinearOrderedField «$α»)

Helper function to synthesize a typed LinearOrderedField α expression.

Equations

• One or more equations did not get rendered due to their size.

theorem Mathlib.Meta.NormNum.isNat_le_true {α : Type u_1} [OrderedSemiring α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.ble a' b' = true → a ≤ b

theorem Mathlib.Meta.NormNum.isNat_lt_false {α : Type u_1} [OrderedSemiring α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : Nat.ble b' a' = true) : ¬a < b

theorem Mathlib.Meta.NormNum.isRat_le_true {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {da : ℕ} {db : ℕ} : Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (Int.mul na (Int.ofNat db) ≤ Int.mul nb (Int.ofNat da)) = true → a ≤ b

theorem Mathlib.Meta.NormNum.isRat_lt_true {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {da : ℕ} {db : ℕ} : Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (na * ↑db < nb * ↑da) = true → a < b

theorem Mathlib.Meta.NormNum.isRat_le_false {α : Type u_1} [LinearOrderedRing α] [Nontrivial α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {da : ℕ} {db : ℕ} (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * ↑da < na * ↑db) = true) : ¬a ≤ b

theorem Mathlib.Meta.NormNum.isRat_lt_false {α : Type u_1} [LinearOrderedRing α] {a : α} {b : α} {na : ℤ} {nb : ℤ} {da : ℕ} {db : ℕ} (ha : Mathlib.Meta.NormNum.IsRat a na da) (hb : Mathlib.Meta.NormNum.IsRat b nb db) (h : decide (nb * ↑da ≤ na * ↑db) = true) : ¬a < b

(In)equalities

theorem Mathlib.Meta.NormNum.isNat_lt_true {α : Type u_1} [OrderedSemiring α] [CharZero α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} : Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → Nat.ble b' a' = false → a < b

theorem Mathlib.Meta.NormNum.isNat_le_false {α : Type u_1} [OrderedSemiring α] [CharZero α] {a : α} {b : α} {a' : ℕ} {b' : ℕ} (ha : Mathlib.Meta.NormNum.IsNat a a') (hb : Mathlib.Meta.NormNum.IsNat b b') (h : Nat.ble a' b' = false) : ¬a ≤ b

theorem Mathlib.Meta.NormNum.isInt_le_true {α : Type u_1} [OrderedRing α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} : Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' ≤ b') = true → a ≤ b

theorem Mathlib.Meta.NormNum.isInt_lt_true {α : Type u_1} [OrderedRing α] [Nontrivial α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} : Mathlib.Meta.NormNum.IsInt a a' → Mathlib.Meta.NormNum.IsInt b b' → decide (a' < b') = true → a < b

theorem Mathlib.Meta.NormNum.isInt_le_false {α : Type u_1} [OrderedRing α] [Nontrivial α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' < a') = true) : ¬a ≤ b

theorem Mathlib.Meta.NormNum.isInt_lt_false {α : Type u_1} [OrderedRing α] {a : α} {b : α} {a' : ℤ} {b' : ℤ} (ha : Mathlib.Meta.NormNum.IsInt a a') (hb : Mathlib.Meta.NormNum.IsInt b b') (h : decide (b' ≤ a') = true) : ¬a < b

def Mathlib.Meta.NormNum.evalLE : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form a ≤ b, such that norm_num successfully recognises both a and b.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalLE.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalLE.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalLT : Mathlib.Meta.NormNum.NormNumExt

The norm_num extension which identifies expressions of the form a < b, such that norm_num successfully recognises both a and b.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalLT.intArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Meta.NormNum.evalLT.ratArm {v : Lean.Level} {β : Q(Type v)} (e : Q(«$β»)) (f : Lean.Expr) (u : Lean.Level) (α : let u := u; Q(Type u)) (a : Q(«$α»)) (b : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (rb : Mathlib.Meta.NormNum.Result b) : Lean.MetaM (Mathlib.Meta.NormNum.Result e)

Equations

• One or more equations did not get rendered due to their size.