Products of ordered monoids

theorem Prod.instOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 + x).1 ≤ (x_2 + x_1).1 ∧ (x_2 + x).2 ≤ (x_2 + x_1).2

instance Prod.instOrderedAddCommMonoidSum {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] : OrderedAddCommMonoid (α × β)

Equations

• Prod.instOrderedAddCommMonoidSum = OrderedAddCommMonoid.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 + x).1 ≤ (x_2 + x_1).1 ∧ (x_2 + x).2 ≤ (x_2 + x_1).2)

instance Prod.instOrderedCommMonoidProd {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [OrderedCommMonoid β] : OrderedCommMonoid (α × β)

Equations

• Prod.instOrderedCommMonoidProd = OrderedCommMonoid.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 * x).1 ≤ (x_2 * x_1).1 ∧ (x_2 * x).2 ≤ (x_2 * x_1).2)

theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : ∀ (x x_1 x_2 : α × β), x + x_1 ≤ x + x_2 → x_1.1 ≤ x_2.1 ∧ x_1.2 ≤ x_2.2

instance Prod.instOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : OrderedCancelAddCommMonoid (α × β)

Equations

• Prod.instOrderedAddCancelCommMonoid = let src := inferInstance; OrderedCancelAddCommMonoid.mk (_ : ∀ (x x_1 x_2 : α × β), x + x_1 ≤ x + x_2 → x_1.1 ≤ x_2.1 ∧ x_1.2 ≤ x_2.2)

instance Prod.instOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] : OrderedCancelCommMonoid (α × β)

Equations

• Prod.instOrderedCancelCommMonoid = let src := inferInstance; OrderedCancelCommMonoid.mk (_ : ∀ (x x_1 x_2 : α × β), x * x_1 ≤ x * x_2 → x_1.1 ≤ x_2.1 ∧ x_1.2 ≤ x_2.2)

abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_1 {α : Type u_2} {β : Type u_1} [Add β] : ∀ {a b : α × β} (motive : (∃ (c : β), b.2 = a.2 + c) → Prop) (x : ∃ (c : β), b.2 = a.2 + c), (∀ (d : β) (hd : b.2 = a.2 + d), motive (_ : ∃ (c : β), b.2 = a.2 + c)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

abbrev Prod.instExistsAddOfLESumInstAddInstLESum.match_2 {α : Type u_1} {β : Type u_2} [Add α] : ∀ {a b : α × β} (motive : (∃ (c : α), b.1 = a.1 + c) → Prop) (x : ∃ (c : α), b.1 = a.1 + c), (∀ (c : α) (hc : b.1 = a.1 + c), motive (_ : ∃ (c : α), b.1 = a.1 + c)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

instance Prod.instExistsAddOfLESumInstAddInstLESum {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] : ExistsAddOfLE (α × β)

Equations

• (_ : ExistsAddOfLE (α × β)) = (_ : ExistsAddOfLE (α × β))

instance Prod.instExistsMulOfLEProdInstMulInstLEProd {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] : ExistsMulOfLE (α × β)

Equations

• (_ : ExistsMulOfLE (α × β)) = (_ : ExistsMulOfLE (α × β))

theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] : ExistsAddOfLE (α × β)

instance Prod.instCanonicallyOrderedAddCommMonoidSum {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] : CanonicallyOrderedAddCommMonoid (α × β)

Equations

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

theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_3 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] : ∀ (x x_1 : α × β), x.1 ≤ (x + x_1).1 ∧ x.2 ≤ (x + x_1).2

theorem Prod.instCanonicallyOrderedAddCommMonoidSum.proof_2 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] : ∀ {a b : α × β}, a ≤ b → ∃ (c : α × β), b = a + c

instance Prod.instCanonicallyOrderedCommMonoidProd {α : Type u_1} {β : Type u_2} [CanonicallyOrderedCommMonoid α] [CanonicallyOrderedCommMonoid β] : CanonicallyOrderedCommMonoid (α × β)

Equations

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

theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [OrderedAddCommMonoid β] : ∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (z : Lex (α × β)), z + x ≤ z + x_1

instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [OrderedAddCommMonoid β] : OrderedAddCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedAddCommMonoid = OrderedAddCommMonoid.mk (_ : ∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (z : Lex (α × β)), z + x ≤ z + x_1)

instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [OrderedCommMonoid β] : OrderedCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedCommMonoid = OrderedCommMonoid.mk (_ : ∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (z : Lex (α × β)), z * x ≤ z * x_1)

theorem Prod.Lex.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : ∀ (x x_1 : Lex (α × β)), x ≤ x_1 → ∀ (a : Lex (α × β)), a + x ≤ a + x_1

instance Prod.Lex.orderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : OrderedCancelAddCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk (_ : ∀ (x x_1 x_2 : Lex (α × β)), x + x_1 ≤ x + x_2 → x_1 ≤ x_2)

theorem Prod.Lex.orderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] : ∀ (x x_1 x_2 : Lex (α × β)), x + x_1 ≤ x + x_2 → x_1 ≤ x_2

instance Prod.Lex.orderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCancelCommMonoid α] [OrderedCancelCommMonoid β] : OrderedCancelCommMonoid (Lex (α × β))

Equations

• Prod.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk (_ : ∀ (x x_1 x_2 : Lex (α × β)), x * x_1 ≤ x * x_2 → x_1 ≤ x_2)

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) : a + b ≤ a + c → b ≤ c

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) : min a b = if a ≤ b then a else b

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) : max a b = if a ≤ b then b else a

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_6 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) : compare a b = compareOfLessAndEq a b

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) : a ≤ b → ∀ (c : Lex (α × β)), c + a ≤ c + b

instance Prod.Lex.linearOrderedAddCancelCommMonoid {α : Type u_1} {β : Type u_2} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] : LinearOrderedCancelAddCommMonoid (Lex (α × β))

Equations

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

theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) : a ≤ b ∨ b ≤ a

instance Prod.Lex.linearOrderedCancelCommMonoid {α : Type u_1} {β : Type u_2} [LinearOrderedCancelCommMonoid α] [LinearOrderedCancelCommMonoid β] : LinearOrderedCancelCommMonoid (Lex (α × β))

Equations

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