chore(Order.Grade): remove porting notes (#10496)

Simple changes to remove porting notes.

Mathlib/Order/Grade.lean

@@ -89,14 +89,14 @@ class GradeBoundedOrder (𝕆 α : Type*) [Preorder 𝕆] [Preorder α] extends
 #align grade_bounded_order GradeBoundedOrder
 
 section Preorder -- grading
--- PORTING NOTE: this `variable [Preorder 𝕆]` for the whole section seems to not work in Lean4
--- variable [Preorder 𝕆]
+variable [Preorder 𝕆]
 
 section Preorder -- graded order
 variable [Preorder α]
 
 section GradeOrder
-variable (𝕆) [Preorder 𝕆] [GradeOrder 𝕆 α] {a b : α}
+variable (𝕆)
+variable [GradeOrder 𝕆 α] {a b : α}
 
 /-- The grade of an element in a graded order. Morally, this is the number of elements you need to
 go down by to get to `⊥`. -/
@@ -265,9 +265,8 @@ theorem grade_ofDual [GradeOrder 𝕆 α] (a : αᵒᵈ) : grade 𝕆 (ofDual a)
 /-- Lifts a graded order along a strictly monotone function. -/
 @[reducible]
 def GradeOrder.liftLeft [GradeOrder 𝕆 α] (f : 𝕆 → ℙ) (hf : StrictMono f)
-    (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α
-    where
-  grade := f ∘ (@grade 𝕆 _ _ _ _) -- porting note - what the hell?! used to be `grade 𝕆`
+    (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder ℙ α where
+  grade := f ∘ _root_.grade 𝕆
   grade_strictMono := hf.comp grade_strictMono
   covBy_grade _ _ h := hcovBy _ _ <| h.grade _
 #align grade_order.lift_left GradeOrder.liftLeft
@@ -301,9 +300,8 @@ def GradeBoundedOrder.liftLeft [GradeBoundedOrder 𝕆 α] (f : 𝕆 → ℙ) (h
 /-- Lifts a graded order along a strictly monotone function. -/
 @[reducible]
 def GradeOrder.liftRight [GradeOrder 𝕆 β] (f : α → β) (hf : StrictMono f)
-    (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α
-    where
-  grade := (@grade 𝕆 _ _ _ _) ∘ f -- porting note: again, weird
+    (hcovBy : ∀ a b, a ⋖ b → f a ⋖ f b) : GradeOrder 𝕆 α where
+  grade := _root_.grade 𝕆 ∘ f
   grade_strictMono := grade_strictMono.comp hf
   covBy_grade _ _ h := (hcovBy _ _ h).grade _
 #align grade_order.lift_right GradeOrder.liftRight