fix bad comments

Mathlib/Data/Rat/Floor.lean

@@ -142,7 +142,7 @@ def evalIntFloor : NormNumExt where eval {u αZ} e := do
       let _i ← synthInstanceQ q(LinearOrderedField $α)
       assertInstancesCommute
       have z : Q(ℤ) := mkRawIntLit ⌊q⌋
-      letI : $z =Q ⌊$n / $d⌋ := ⟨⟩
+      letI : $z =Q $n / $d := ⟨⟩
       return .isInt q(inferInstance) z ⌊q⌋ q(isInt_intFloor_ofIsRat _ $n $d $h)
   | _, _, _ => failure
 
@@ -172,7 +172,7 @@ def evalIntCeil : NormNumExt where eval {u αZ} e := do
       return .isNat q(inferInstance) _ q(isNat_intCeil $x _ $pb)
     | .isNegNat _ _ pb => do
       assertInstancesCommute
-      -- floor always keeps naturals negative, so we can shortcut `.isInt`
+      -- ceil always keeps naturals negative, so we can shortcut `.isInt`
       return .isNegNat q(inferInstance) _ q(isInt_intCeil _ _ $pb)
     | .isRat _ q n d h => do
       let _i ← synthInstanceQ q(LinearOrderedField $α)