From ee8ce8507d3fb309d54814f43799c9d35c616065 Mon Sep 17 00:00:00 2001 From: adomani Date: Tue, 16 Apr 2024 11:37:44 +0200 Subject: [PATCH] remove non-existing set_options --- .../Limits/FilteredColimitCommutesFiniteLimit.lean | 2 -- Mathlib/CategoryTheory/Limits/Final.lean | 1 - Mathlib/Tactic/NormNum/Inv.lean | 2 -- 3 files changed, 5 deletions(-) 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,