Products of ordered monoids

ink

def Prod.instOrderedAddCommMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [inst : OrderedAddCommMonoid α] [inst : OrderedAddCommMonoid β] : ∀ (x x_1 : α × β), x ≤ x_1 → ∀ (x_2 : α × β), (x_2 + x).fst ≤ (x_2 + x_1).fst ∧ (x_2 + x).snd ≤ (x_2 + x_1).snd

Equations

• (_ : (x + x).fst ≤ (x + x).fst ∧ (x + x).snd ≤ (x + x).snd) = (_ : (x + x).fst ≤ (x + x).fst ∧ (x + x).snd ≤ (x + x).snd)

ink

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

Equations

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

ink

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

Equations

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

ink

def Prod.instOrderedAddCancelCommMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : OrderedCancelAddCommMonoid M] [inst : OrderedCancelAddCommMonoid N] (a : M × N) (b : M × N) : a ≤ b → ∀ (c : M × N), c + a ≤ c + b

Equations

• (_ : ∀ (a b : M × N), a ≤ b → ∀ (c : M × N), c + a ≤ c + b) = (_ : ∀ (a b : M × N), a ≤ b → ∀ (c : M × N), c + a ≤ c + b)

ink

instance Prod.instOrderedAddCancelCommMonoidSum {M : Type u_1} {N : Type u_2} [inst : OrderedCancelAddCommMonoid M] [inst : OrderedCancelAddCommMonoid N] : OrderedCancelAddCommMonoid (M × N)

Equations

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

ink

def Prod.instOrderedAddCancelCommMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : OrderedCancelAddCommMonoid M] [inst : OrderedCancelAddCommMonoid N] : ∀ (x x_1 x_2 : M × N), x + x_1 ≤ x + x_2 → x_1.fst ≤ x_2.fst ∧ x_1.snd ≤ x_2.snd

Equations

• (_ : x.fst ≤ x.fst ∧ x.snd ≤ x.snd) = (_ : x.fst ≤ x.fst ∧ x.snd ≤ x.snd)

ink

instance Prod.instOrderedCancelCommMonoidProd {M : Type u_1} {N : Type u_2} [inst : OrderedCancelCommMonoid M] [inst : OrderedCancelCommMonoid N] : OrderedCancelCommMonoid (M × N)

Equations

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

ink

def Prod.instExistsAddOfLESumInstAddSumInstLESum.proof_1 {α : Type u_1} {β : Type u_2} [inst : LE α] [inst : LE β] [inst : Add α] [inst : Add β] [inst : ExistsAddOfLE α] [inst : ExistsAddOfLE β] : ExistsAddOfLE (α × β)

Equations

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

ink

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

Equations

• Prod.instExistsAddOfLESumInstAddSumInstLESum.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

Equations

• Prod.instExistsAddOfLESumInstAddSumInstLESum.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

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

Equations

• @Prod.instExistsAddOfLESumInstAddSumInstLESum = @Prod.instExistsAddOfLESumInstAddSumInstLESum.proof_1

ink

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

Equations

• @Prod.instExistsMulOfLEProdInstMulProdInstLEProd = @Prod.instExistsMulOfLEProdInstMulProdInstLEProd.proof_1

ink

def Prod.instCanonicallyOrderedAddMonoidSum.proof_2 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] : ExistsAddOfLE (α × β)

Equations

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

ink

def Prod.instCanonicallyOrderedAddMonoidSum.proof_4 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] : ∀ {a b : α × β}, a ≤ b → ∃ c, b = a + c

Equations

• (_ : a ≤ b → ∃ c, b = a + c) = (_ : a ≤ b → ∃ c, b = a + c)

ink

def Prod.instCanonicallyOrderedAddMonoidSum.proof_3 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] (a : α × β) : ⊥ ≤ a

Equations

• (_ : ∀ (a : α × β), ⊥ ≤ a) = (_ : ∀ (a : α × β), ⊥ ≤ a)

ink

def Prod.instCanonicallyOrderedAddMonoidSum.proof_1 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] (a : α × β) (b : α × β) : a ≤ b → ∀ (c : α × β), c + a ≤ c + b

Equations

• (_ : ∀ (a b : α × β), a ≤ b → ∀ (c : α × β), c + a ≤ c + b) = (_ : ∀ (a b : α × β), a ≤ b → ∀ (c : α × β), c + a ≤ c + b)

ink

instance Prod.instCanonicallyOrderedAddMonoidSum {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] : CanonicallyOrderedAddMonoid (α × β)

Equations

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

ink

def Prod.instCanonicallyOrderedAddMonoidSum.proof_5 {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedAddMonoid α] [inst : CanonicallyOrderedAddMonoid β] : ∀ (x x_1 : α × β), x.fst ≤ (x + x_1).fst ∧ x.snd ≤ (x + x_1).snd

Equations

• (_ : x.fst ≤ (x + x).fst ∧ x.snd ≤ (x + x).snd) = (_ : x.fst ≤ (x + x).fst ∧ x.snd ≤ (x + x).snd)

ink

instance Prod.instCanonicallyOrderedMonoidProd {α : Type u_1} {β : Type u_2} [inst : CanonicallyOrderedMonoid α] [inst : CanonicallyOrderedMonoid β] : CanonicallyOrderedMonoid (α × β)

Equations

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