Tweak to use the ofNat thing from #20169.

leanprover-community · Jan 6, 2025 · b4bbbad · b4bbbad
1 parent d7af08c
commit b4bbbad
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Order/Kleene.lean b/Mathlib/Algebra/Order/Kleene.lean
@@ -138,7 +138,7 @@ lemma natCast_eq_one {n : ℕ} (nezero : n ≠ 0) : (n : α) = 1 := by
   | base => exact Nat.cast_one
   | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]
 
-lemma ofNat_eq_one {n : ℕ} [n.AtLeastTwo] : (no_index (OfNat.ofNat n : α)) = 1 :=
+lemma ofNat_eq_one {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : α) = 1 :=
   natCast_eq_one <| Nat.not_eq_zero_of_lt Nat.AtLeastTwo.prop
 
 theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -856,7 +856,7 @@ theorem natCast_eq_top {n : ℕ} (hn : n ≠ 0) : (n : Ideal R) = ⊤ :=
 
 /-- `3 : Ideal R` is *not* the ideal generated by 3 (which would be spelt
     `Ideal.span {3}`), it is simply `1 + 1 + 1 = ⊤`. -/
-theorem ofNat_eq_top {n : ℕ} [n.AtLeastTwo] : (no_index (OfNat.ofNat n : Ideal R)) = ⊤ :=
+theorem ofNat_eq_top {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Ideal R) = ⊤ :=
   ofNat_eq_one.trans one_eq_top
 
 variable (I)