diff --git a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
index f997c05417cc4..e983c517cfbc1 100644
--- a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
@@ -159,7 +159,6 @@ open CategoryTheory.Prod
 
 variable [IsFiltered K]
 
-set_option linter.haveLet false in  -- `clear_value` complains
 /-- This follows this proof from
 * Borceux, Handbook of categorical algebra 1, Theorem 2.13.4
 although with different names.
@@ -188,7 +187,6 @@ theorem colimitLimitToLimitColimit_surjective :
     -- As a first step, we use that `K` is filtered to pick some point `k' : K` above all the `k j`
     let k' : K := IsFiltered.sup (Finset.univ.image k) ∅
     -- and name the morphisms as `g j : k j ⟶ k'`.
-    -- changing `have` to `let` causes `clear_value k'` to complain
     have g : ∀ j, k j ⟶ k' := fun j => IsFiltered.toSup (Finset.univ.image k) ∅ (by simp)
     clear_value k'
     -- Recalling that the components of `x`, which are indexed by `j : J`, are "coherent",
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 8be4aba1dcb8c..dfdad42583d7a 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -408,7 +408,6 @@ theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶
 
 end Final
 
-set_option linter.haveLet false in  -- have := (I d).inv PUnit.unit
 /-- If `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit` for all `d : D`, then `F` is cofinal.
 -/
 theorem cofinal_of_colimit_comp_coyoneda_iso_pUnit
diff --git a/Mathlib/Tactic/NormNum/Inv.lean b/Mathlib/Tactic/NormNum/Inv.lean
index 8166a5a876ff4..c1de8cc594748 100644
--- a/Mathlib/Tactic/NormNum/Inv.lean
+++ b/Mathlib/Tactic/NormNum/Inv.lean
@@ -121,12 +121,10 @@ theorem isRat_inv_neg_one {α} [DivisionRing α] : {a : α} →
     IsInt a (.negOfNat (nat_lit 1)) → IsInt a⁻¹ (.negOfNat (nat_lit 1))
   | _, ⟨rfl⟩ => ⟨by simp [inv_neg_one]⟩
 
-set_option linter.haveLet false in
 theorem isRat_inv_neg {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} :
     IsRat a (.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (.negOfNat d) (Nat.succ n) := by
   rintro ⟨_, rfl⟩
   simp only [Int.negOfNat_eq]
-  -- changing `have` to `let`, makes the following `generalize` fail
   have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
   generalize Nat.succ n = n at *
   use this; simp only [Int.ofNat_eq_coe, Int.cast_neg,