chore: remove redundant comment, fix typo in FixedPoints

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/Order/FixedPoints.lean

@@ -106,10 +106,6 @@ theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p
   have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
   exact h.antisymm (f.lfp_le <| le_sSup hmem)
 
--- le_gfp, gfp_le, gfp_le_fixed, gfp_le_map, map_gfp, isFixedPt_gfp,
--- map_le_gfp, isGreatest_gfp_le, isGreatest_gfp, gfp_induction
--- auto-generated by @[to_dual]
-
 theorem lfp_le_gfp : f.lfp ≤ f.gfp :=
   f.lfp_le_fixed f.isFixedPt_gfp
 
@@ -243,7 +239,7 @@ instance completeLattice : CompleteLattice (fixedPoints f) where
 open OmegaCompletePartialOrder fixedPoints
 
 /-- **Kleene's fixed point Theorem**: The least fixed point in a complete lattice is
-the supremum of iterating a function on bottom arbitrary often. -/
+the supremum of iterating a function on bottom arbitrarily often. -/
 -- TODO: can't @[to_dual] because bot_le/le_top mismatch in ωSup_iterate proof
 theorem lfp_eq_sSup_iterate (h : ωScottContinuous f) :
     f.lfp = ⨆ n, f^[n] ⊥ := by