/-
Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov, Yaël Dillies

! This file was ported from Lean 3 source module algebra.ring.order_synonym
! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.Group.OrderSynonym

/-!
# Ring structure on the order type synonyms

Transfer algebraic instances from `α` to `αᵒᵈ` and `Lex α`.
-/


variable {α: Type ?u.5
α : Type _: Type (?u.1479+1)
Type _}

/-! ### Order dual -/


instance: {α : Type u_1} → [h : Distrib α] → Distrib αᵒᵈ
instance [h: Distrib α
h : Distrib: Type ?u.8 → Type ?u.8
Distrib α: Type ?u.5
α] : Distrib: Type ?u.11 → Type ?u.11
Distrib α: Type ?u.5
αᵒᵈ := h: Distrib α
h

instance: {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → [h : LeftDistribClass α] → LeftDistribClass αᵒᵈ
instance [Mul: Type ?u.49 → Type ?u.49
Mul α: Type ?u.46
α] [Add: Type ?u.52 → Type ?u.52
Add α: Type ?u.46
α] [h: LeftDistribClass α
h : LeftDistribClass: (R : Type ?u.55) → [inst : Mul R] → [inst : Add R] → Type
LeftDistribClass α: Type ?u.46
α] : LeftDistribClass: (R : Type ?u.75) → [inst : Mul R] → [inst : Add R] → Type
LeftDistribClass α: Type ?u.46
αᵒᵈ := h: LeftDistribClass α
h

instance: {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → [h : RightDistribClass α] → RightDistribClass αᵒᵈ
instance [Mul: Type ?u.180 → Type ?u.180
Mul α: Type ?u.177
α] [Add: Type ?u.183 → Type ?u.183
Add α: Type ?u.177
α] [h: RightDistribClass α
h : RightDistribClass: (R : Type ?u.186) → [inst : Mul R] → [inst : Add R] → Type
RightDistribClass α: Type ?u.177
α] : RightDistribClass: (R : Type ?u.206) → [inst : Mul R] → [inst : Add R] → Type
RightDistribClass α: Type ?u.177
αᵒᵈ := h: RightDistribClass α
h

instance: {α : Type u_1} → [h : NonUnitalNonAssocSemiring α] → NonUnitalNonAssocSemiring αᵒᵈ
instance [h: NonUnitalNonAssocSemiring α
h : NonUnitalNonAssocSemiring: Type ?u.311 → Type ?u.311
NonUnitalNonAssocSemiring α: Type ?u.308
α] : NonUnitalNonAssocSemiring: Type ?u.314 → Type ?u.314
NonUnitalNonAssocSemiring α: Type ?u.308
αᵒᵈ := h: NonUnitalNonAssocSemiring α
h

instance: {α : Type u_1} → [h : NonUnitalSemiring α] → NonUnitalSemiring αᵒᵈ
instance [h: NonUnitalSemiring α
h : NonUnitalSemiring: Type ?u.352 → Type ?u.352
NonUnitalSemiring α: Type ?u.349
α] : NonUnitalSemiring: Type ?u.355 → Type ?u.355
NonUnitalSemiring α: Type ?u.349
αᵒᵈ := h: NonUnitalSemiring α
h

instance: {α : Type u_1} → [h : NonAssocSemiring α] → NonAssocSemiring αᵒᵈ
instance [h: NonAssocSemiring α
h : NonAssocSemiring: Type ?u.393 → Type ?u.393
NonAssocSemiring α: Type ?u.390
α] : NonAssocSemiring: Type ?u.396 → Type ?u.396
NonAssocSemiring α: Type ?u.390
αᵒᵈ := h: NonAssocSemiring α
h

instance: {α : Type u_1} → [h : Semiring α] → Semiring αᵒᵈ
instance [h: Semiring α
h : Semiring: Type ?u.434 → Type ?u.434
Semiring α: Type ?u.431
α] : Semiring: Type ?u.437 → Type ?u.437
Semiring α: Type ?u.431
αᵒᵈ := h: Semiring α
h

instance: {α : Type u_1} → [h : NonUnitalCommSemiring α] → NonUnitalCommSemiring αᵒᵈ
instance [h: NonUnitalCommSemiring α
h : NonUnitalCommSemiring: Type ?u.475 → Type ?u.475
NonUnitalCommSemiring α: Type ?u.472
α] : NonUnitalCommSemiring: Type ?u.478 → Type ?u.478
NonUnitalCommSemiring α: Type ?u.472
αᵒᵈ := h: NonUnitalCommSemiring α
h

instance: {α : Type u_1} → [h : CommSemiring α] → CommSemiring αᵒᵈ
instance [h: CommSemiring α
h : CommSemiring: Type ?u.516 → Type ?u.516
CommSemiring α: Type ?u.513
α] : CommSemiring: Type ?u.519 → Type ?u.519
CommSemiring α: Type ?u.513
αᵒᵈ := h: CommSemiring α
h

instance: {α : Type u_1} → [inst : Mul α] → [h : HasDistribNeg α] → HasDistribNeg αᵒᵈ
instance [Mul: Type ?u.557 → Type ?u.557
Mul α: Type ?u.554
α] [h: HasDistribNeg α
h : HasDistribNeg: (α : Type ?u.560) → [inst : Mul α] → Type ?u.560
HasDistribNeg α: Type ?u.554
α] : HasDistribNeg: (α : Type ?u.573) → [inst : Mul α] → Type ?u.573
HasDistribNeg α: Type ?u.554
αᵒᵈ := h: HasDistribNeg α
h

instance: {α : Type u_1} → [h : NonUnitalNonAssocRing α] → NonUnitalNonAssocRing αᵒᵈ
instance [h: NonUnitalNonAssocRing α
h : NonUnitalNonAssocRing: Type ?u.648 → Type ?u.648
NonUnitalNonAssocRing α: Type ?u.645
α] : NonUnitalNonAssocRing: Type ?u.651 → Type ?u.651
NonUnitalNonAssocRing α: Type ?u.645
αᵒᵈ := h: NonUnitalNonAssocRing α
h

instance: {α : Type u_1} → [h : NonUnitalRing α] → NonUnitalRing αᵒᵈ
instance [h: NonUnitalRing α
h : NonUnitalRing: Type ?u.689 → Type ?u.689
NonUnitalRing α: Type ?u.686
α] : NonUnitalRing: Type ?u.692 → Type ?u.692
NonUnitalRing α: Type ?u.686
αᵒᵈ := h: NonUnitalRing α
h

instance: {α : Type u_1} → [h : NonAssocRing α] → NonAssocRing αᵒᵈ
instance [h: NonAssocRing α
h : NonAssocRing: Type ?u.730 → Type ?u.730
NonAssocRing α: Type ?u.727
α] : NonAssocRing: Type ?u.733 → Type ?u.733
NonAssocRing α: Type ?u.727
αᵒᵈ := h: NonAssocRing α
h

instance: {α : Type u_1} → [h : Ring α] → Ring αᵒᵈ
instance [h: Ring α
h : Ring: Type ?u.771 → Type ?u.771
Ring α: Type ?u.768
α] : Ring: Type ?u.774 → Type ?u.774
Ring α: Type ?u.768
αᵒᵈ := h: Ring α
h

instance: {α : Type u_1} → [h : NonUnitalCommRing α] → NonUnitalCommRing αᵒᵈ
instance [h: NonUnitalCommRing α
h : NonUnitalCommRing: Type ?u.812 → Type ?u.812
NonUnitalCommRing α: Type ?u.809
α] : NonUnitalCommRing: Type ?u.815 → Type ?u.815
NonUnitalCommRing α: Type ?u.809
αᵒᵈ := h: NonUnitalCommRing α
h

instance: {α : Type u_1} → [h : CommRing α] → CommRing αᵒᵈ
instance [h: CommRing α
h : CommRing: Type ?u.853 → Type ?u.853
CommRing α: Type ?u.850
α] : CommRing: Type ?u.856 → Type ?u.856
CommRing α: Type ?u.850
αᵒᵈ := h: CommRing α
h

instance: ∀ {α : Type u_1} [inst : Ring α] [h : IsDomain α], IsDomain αᵒᵈ
instance [Ring: Type ?u.894 → Type ?u.894
Ring α: Type ?u.891
α] [h: IsDomain α
h : IsDomain: (α : Type ?u.897) → [inst : Semiring α] → Prop
IsDomain α: Type ?u.891
α] : IsDomain: (α : Type ?u.920) → [inst : Semiring α] → Prop
IsDomain α: Type ?u.891
αᵒᵈ := h: IsDomain α
h

/-! ### Lexicographical order -/


instance: {α : Type u_1} → [h : Distrib α] → Distrib (Lex α)
instance [h: Distrib α
h : Distrib: Type ?u.974 → Type ?u.974
Distrib α: Type ?u.971
α] : Distrib: Type ?u.977 → Type ?u.977
Distrib (Lex: Type ?u.978 → Type ?u.978
Lex α: Type ?u.971
α) := h: Distrib α
h

instance: {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → [h : LeftDistribClass α] → LeftDistribClass (Lex α)
instance [Mul: Type ?u.1015 → Type ?u.1015
Mul α: Type ?u.1012
α] [Add: Type ?u.1018 → Type ?u.1018
Add α: Type ?u.1012
α] [h: LeftDistribClass α
h : LeftDistribClass: (R : Type ?u.1021) → [inst : Mul R] → [inst : Add R] → Type
LeftDistribClass α: Type ?u.1012
α] : LeftDistribClass: (R : Type ?u.1041) → [inst : Mul R] → [inst : Add R] → Type
LeftDistribClass (Lex: Type ?u.1042 → Type ?u.1042
Lex α: Type ?u.1012
α) := h: LeftDistribClass α
h

instance: {α : Type u_1} → [inst : Mul α] → [inst_1 : Add α] → [h : RightDistribClass α] → RightDistribClass (Lex α)
instance [Mul: Type ?u.1146 → Type ?u.1146
Mul α: Type ?u.1143
α] [Add: Type ?u.1149 → Type ?u.1149
Add α: Type ?u.1143
α] [h: RightDistribClass α
h : RightDistribClass: (R : Type ?u.1152) → [inst : Mul R] → [inst : Add R] → Type
RightDistribClass α: Type ?u.1143
α] : RightDistribClass: (R : Type ?u.1172) → [inst : Mul R] → [inst : Add R] → Type
RightDistribClass (Lex: Type ?u.1173 → Type ?u.1173
Lex α: Type ?u.1143
α) := h: RightDistribClass α
h

instance: {α : Type u_1} → [h : NonUnitalNonAssocSemiring α] → NonUnitalNonAssocSemiring (Lex α)
instance [h: NonUnitalNonAssocSemiring α
h : NonUnitalNonAssocSemiring: Type ?u.1277 → Type ?u.1277
NonUnitalNonAssocSemiring α: Type ?u.1274
α] : NonUnitalNonAssocSemiring: Type ?u.1280 → Type ?u.1280
NonUnitalNonAssocSemiring (Lex: Type ?u.1281 → Type ?u.1281
Lex α: Type ?u.1274
α) := h: NonUnitalNonAssocSemiring α
h

instance: {α : Type u_1} → [h : NonUnitalSemiring α] → NonUnitalSemiring (Lex α)
instance [h: NonUnitalSemiring α
h : NonUnitalSemiring: Type ?u.1318 → Type ?u.1318
NonUnitalSemiring α: Type ?u.1315
α] : NonUnitalSemiring: Type ?u.1321 → Type ?u.1321
NonUnitalSemiring (Lex: Type ?u.1322 → Type ?u.1322
Lex α: Type ?u.1315
α) := h: NonUnitalSemiring α
h

instance: {α : Type u_1} → [h : NonAssocSemiring α] → NonAssocSemiring (Lex α)
instance [h: NonAssocSemiring α
h : NonAssocSemiring: Type ?u.1359 → Type ?u.1359
NonAssocSemiring α: Type ?u.1356
α] : NonAssocSemiring: Type ?u.1362 → Type ?u.1362
NonAssocSemiring (Lex: Type ?u.1363 → Type ?u.1363
Lex α: Type ?u.1356
α) := h: NonAssocSemiring α
h

instance: {α : Type u_1} → [h : Semiring α] → Semiring (Lex α)
instance [h: Semiring α
h : Semiring: Type ?u.1400 → Type ?u.1400
Semiring α: Type ?u.1397
α] : Semiring: Type ?u.1403 → Type ?u.1403
Semiring (Lex: Type ?u.1404 → Type ?u.1404
Lex α: Type ?u.1397
α) := h: Semiring α
h

instance: {α : Type u_1} → [h : NonUnitalCommSemiring α] → NonUnitalCommSemiring (Lex α)
instance [h: NonUnitalCommSemiring α
h : NonUnitalCommSemiring: Type ?u.1441 → Type ?u.1441
NonUnitalCommSemiring α: Type ?u.1438
α] : NonUnitalCommSemiring: Type ?u.1444 → Type ?u.1444
NonUnitalCommSemiring (Lex: Type ?u.1445 → Type ?u.1445
Lex α: Type ?u.1438
α) := h: NonUnitalCommSemiring α
h

instance: {α : Type u_1} → [h : CommSemiring α] → CommSemiring (Lex α)
instance [h: CommSemiring α
h : CommSemiring: Type ?u.1482 → Type ?u.1482
CommSemiring α: Type ?u.1479
α] : CommSemiring: Type ?u.1485 → Type ?u.1485
CommSemiring (Lex: Type ?u.1486 → Type ?u.1486
Lex α: Type ?u.1479
α) := h: CommSemiring α
h

instance: {α : Type u_1} → [inst : Mul α] → [h : HasDistribNeg α] → HasDistribNeg (Lex α)
instance [Mul: Type ?u.1523 → Type ?u.1523
Mul α: Type ?u.1520
α] [h: HasDistribNeg α
h : HasDistribNeg: (α : Type ?u.1526) → [inst : Mul α] → Type ?u.1526
HasDistribNeg α: Type ?u.1520
α] : HasDistribNeg: (α : Type ?u.1539) → [inst : Mul α] → Type ?u.1539
HasDistribNeg (Lex: Type ?u.1540 → Type ?u.1540
Lex α: Type ?u.1520
α) := h: HasDistribNeg α
h

instance: {α : Type u_1} → [h : NonUnitalNonAssocRing α] → NonUnitalNonAssocRing (Lex α)
instance [h: NonUnitalNonAssocRing α
h : NonUnitalNonAssocRing: Type ?u.1614 → Type ?u.1614
NonUnitalNonAssocRing α: Type ?u.1611
α] : NonUnitalNonAssocRing: Type ?u.1617 → Type ?u.1617
NonUnitalNonAssocRing (Lex: Type ?u.1618 → Type ?u.1618
Lex α: Type ?u.1611
α) := h: NonUnitalNonAssocRing α
h

instance: {α : Type u_1} → [h : NonUnitalRing α] → NonUnitalRing (Lex α)
instance [h: NonUnitalRing α
h : NonUnitalRing: Type ?u.1655 → Type ?u.1655
NonUnitalRing α: Type ?u.1652
α] : NonUnitalRing: Type ?u.1658 → Type ?u.1658
NonUnitalRing (Lex: Type ?u.1659 → Type ?u.1659
Lex α: Type ?u.1652
α) := h: NonUnitalRing α
h

instance: {α : Type u_1} → [h : NonAssocRing α] → NonAssocRing (Lex α)
instance [h: NonAssocRing α
h : NonAssocRing: Type ?u.1696 → Type ?u.1696
NonAssocRing α: Type ?u.1693
α] : NonAssocRing: Type ?u.1699 → Type ?u.1699
NonAssocRing (Lex: Type ?u.1700 → Type ?u.1700
Lex α: Type ?u.1693
α) := h: NonAssocRing α
h

instance: {α : Type u_1} → [h : Ring α] → Ring (Lex α)
instance [h: Ring α
h : Ring: Type ?u.1737 → Type ?u.1737
Ring α: Type ?u.1734
α] : Ring: Type ?u.1740 → Type ?u.1740
Ring (Lex: Type ?u.1741 → Type ?u.1741
Lex α: Type ?u.1734
α) := h: Ring α
h

instance: {α : Type u_1} → [h : NonUnitalCommRing α] → NonUnitalCommRing (Lex α)
instance [h: NonUnitalCommRing α
h : NonUnitalCommRing: Type ?u.1778 → Type ?u.1778
NonUnitalCommRing α: Type ?u.1775
α] : NonUnitalCommRing: Type ?u.1781 → Type ?u.1781
NonUnitalCommRing (Lex: Type ?u.1782 → Type ?u.1782
Lex α: Type ?u.1775
α) := h: NonUnitalCommRing α
h

instance: {α : Type u_1} → [h : CommRing α] → CommRing (Lex α)
instance [h: CommRing α
h : CommRing: Type ?u.1819 → Type ?u.1819
CommRing α: Type ?u.1816
α] : CommRing: Type ?u.1822 → Type ?u.1822
CommRing (Lex: Type ?u.1823 → Type ?u.1823
Lex α: Type ?u.1816
α) := h: CommRing α
h

instance: ∀ {α : Type u_1} [inst : Ring α] [h : IsDomain α], IsDomain (Lex α)
instance [Ring: Type ?u.1860 → Type ?u.1860
Ring α: Type ?u.1857
α] [h: IsDomain α
h : IsDomain: (α : Type ?u.1863) → [inst : Semiring α] → Prop
IsDomain α: Type ?u.1857
α] : IsDomain: (α : Type ?u.1886) → [inst : Semiring α] → Prop
IsDomain (Lex: Type ?u.1887 → Type ?u.1887
Lex α: Type ?u.1857
α) := h: IsDomain α
h