Deprecated instances about order structures.

@[deprecated "This was a leftover from Lean 3, and has not been needed." (since := "2024-11-26")]

instance isStrictTotalOrder_of_linearOrder {α : Type u_1} [LinearOrder α] : IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2

Lemmas of the form b ≤ c → a ≤ 1 → b * a ≤ c.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_le_of_le_of_le_one_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : b ≤ c) (ha : a ≤ 1) (hb : 0 ≤ b) : b * a ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] (bc : b ≤ c) (ha : a < 1) (b0 : 0 < b) : b * a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : b < c) (ha : a ≤ 1) (hb : 0 ≤ b) : b * a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.mul_le_one_of_le_of_le {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulMono α] (ha : a ≤ 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b ≤ 1

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.mul_lt_of_le_of_lt_one_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulStrictMono α] (ha : a ≤ 1) (hb : b < 1) (a0 : 0 < a) : a * b < 1

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.mul_lt_of_lt_of_le_one_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulMono α] (ha : a < 1) (hb : b ≤ 1) (a0 : 0 ≤ a) : a * b < 1

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_le_of_le_of_le_one' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosMono α] (bc : b ≤ c) (ha : a ≤ 1) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : b * a ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_of_le_one' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : a ≤ 1) (a0 : 0 < a) (c0 : 0 ≤ c) : b * a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_le_of_lt_one' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [MulPosMono α] (bc : b ≤ c) (ha : a < 1) (a0 : 0 ≤ a) (c0 : 0 < c) : b * a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_of_lt_one_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : a ≤ 1) (a0 : 0 < a) (c0 : 0 ≤ c) : b * a < c

Lemmas of the form b ≤ c → 1 ≤ a → b ≤ c * a.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_mul_of_le_of_one_le_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : b ≤ c) (ha : 1 ≤ a) (hc : 0 ≤ c) : b ≤ c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_le_of_one_lt_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] (bc : b ≤ c) (ha : 1 < a) (c0 : 0 < c) : b < c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : b < c) (ha : 1 ≤ a) (hc : 0 ≤ c) : b < c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.one_le_mul_of_le_of_le {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : 1 ≤ a * b

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.one_lt_mul_of_le_of_lt_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulStrictMono α] (ha : 1 ≤ a) (hb : 1 < b) (a0 : 0 < a) : 1 < a * b

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Left.lt_mul_of_lt_of_one_le_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [PosMulMono α] (ha : 1 < a) (hb : 1 ≤ b) (a0 : 0 ≤ a) : 1 < a * b

Assumes left covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_mul_of_le_of_one_le' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosMono α] (bc : b ≤ c) (ha : 1 ≤ a) (a0 : 0 ≤ a) (b0 : 0 ≤ b) : b ≤ c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_le_of_one_lt' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [MulPosMono α] (bc : b ≤ c) (ha : 1 < a) (a0 : 0 ≤ a) (b0 : 0 < b) : b < c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_lt_of_one_le' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosStrictMono α] (bc : b < c) (ha : 1 ≤ a) (a0 : 0 < a) (b0 : 0 ≤ b) : b < c * a

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_lt_of_one_lt_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [MulPosStrictMono α] (bc : b < c) (ha : 1 < a) (a0 : 0 < a) (b0 : 0 < b) : b < c * a

Lemmas of the form a ≤ 1 → b ≤ c → a * b ≤ c.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_le_of_le_one_of_le_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (ha : a ≤ 1) (h : b ≤ c) (hb : 0 ≤ b) : a * b ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_one_of_le_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] (ha : a < 1) (h : b ≤ c) (hb : 0 < b) : a * b < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_le_one_of_lt_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (ha : a ≤ 1) (h : b < c) (hb : 0 ≤ b) : a * b < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.mul_lt_one_of_lt_of_le_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosStrictMono α] (ha : a < 1) (hb : b ≤ 1) (b0 : 0 < b) : a * b < 1

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.mul_lt_one_of_le_of_lt_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosMono α] (ha : a ≤ 1) (hb : b < 1) (b0 : 0 ≤ b) : a * b < 1

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_one_of_lt_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [MulPosStrictMono α] (ha : a < 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 < c) : a * b < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.mul_le_one_of_le_of_le {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosMono α] (ha : a ≤ 1) (hb : b ≤ 1) (b0 : 0 ≤ b) : a * b ≤ 1

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_le_of_le_one_of_le' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosMono α] (ha : a ≤ 1) (bc : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 ≤ c) : a * b ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_lt_one_of_le' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] [MulPosStrictMono α] (ha : a < 1) (bc : b ≤ c) (a0 : 0 ≤ a) (c0 : 0 < c) : a * b < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem mul_lt_of_le_one_of_lt' {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulStrictMono α] [MulPosMono α] (ha : a ≤ 1) (bc : b < c) (a0 : 0 < a) (c0 : 0 ≤ c) : a * b < c

Lemmas of the form 1 ≤ a → b ≤ c → b ≤ a * c.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_one_lt_of_le_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] (ha : 1 < a) (h : b ≤ c) (hc : 0 < c) : b < a * c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_one_le_of_lt_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) : b < a * c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_one_lt_of_lt_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosStrictMono α] (ha : 1 < a) (h : b < c) (hc : 0 < c) : b < a * c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.one_lt_mul_of_lt_of_le_of_pos {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosStrictMono α] (ha : 1 < a) (hb : 1 ≤ b) (b0 : 0 < b) : 1 < a * b

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.one_lt_mul_of_le_of_lt_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosMono α] (ha : 1 ≤ a) (hb : 1 < b) (b0 : 0 ≤ b) : 1 < a * b

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.one_lt_mul_of_lt_of_lt {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosStrictMono α] (ha : 1 < a) (hb : 1 < b) (b0 : 0 < b) : 1 < a * b

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_mul_of_one_lt_of_lt_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (ha : 1 ≤ a) (h : b < c) (hc : 0 ≤ c) : b < a * c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_of_mul_lt_of_one_le_of_nonneg_left {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : a * b < c) (hle : 1 ≤ b) (ha : 0 ≤ a) : a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_of_lt_mul_of_le_one_of_nonneg_left {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : a < b * c) (hc : c ≤ 1) (hb : 0 ≤ b) : a < b

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem lt_of_lt_mul_of_le_one_of_nonneg_right {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (h : a < b * c) (hb : b ≤ 1) (hc : 0 ≤ c) : a < c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_mul_of_one_le_of_le_of_nonneg {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (ha : 1 ≤ a) (bc : b ≤ c) (c0 : 0 ≤ c) : b ≤ a * c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem Right.one_le_mul_of_le_of_le {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b : α} [MulPosMono α] (ha : 1 ≤ a) (hb : 1 ≤ b) (b0 : 0 ≤ b) : 1 ≤ a * b

Assumes right covariance.

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_of_mul_le_of_one_le_of_nonneg_left {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : a * b ≤ c) (hb : 1 ≤ b) (ha : 0 ≤ a) : a ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_of_le_mul_of_le_one_of_nonneg_left {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [PosMulMono α] (h : a ≤ b * c) (hc : c ≤ 1) (hb : 0 ≤ b) : a ≤ b

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_of_mul_le_of_one_le_nonneg_right {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (h : a * b ≤ c) (ha : 1 ≤ a) (hb : 0 ≤ b) : b ≤ c

@[deprecated "No replacement, use constituent lemmas from proof." (since := "2025-02-27")]

theorem le_of_le_mul_of_le_one_of_nonneg_right {α : Type u_1} [MulOneClass α] [Zero α] [Preorder α] {a b c : α} [MulPosMono α] (h : a ≤ b * c) (hb : b ≤ 1) (hc : 0 ≤ c) : a ≤ c

@[deprecated "No replacement." (since := "2025-02-27")]

theorem exists_square_le' {α : Type u_1} [MulOneClass α] [Zero α] [LinearOrder α] {a : α} [PosMulStrictMono α] (a0 : 0 < a) : ∃ (b : α), b * b ≤ a