no goals
F : Type ?u.65495
α : Type u_1
β : Type ?u.65501
γ : Type ?u.65504
δ : Type ?u.65507
inst✝¹¹ : Mul α
inst✝¹⁰ : Add α
inst✝⁹ : LE α
inst✝⁸ : Mul β
inst✝⁷ : Add β
inst✝⁶ : LE β
inst✝⁵ : Mul γ
inst✝⁴ : Add γ
inst✝³ : LE γ
inst✝² : Mul δ
inst✝¹ : Add δ
inst✝ : LE δ
x : α
⊢ ↑(OrderRingIso.refl α) x = x
rfl