chore: cleanup skipAssignedInstances flags (#18320)

leanprover-community · Oct 28, 2024 · 2d2bbe0 · 2d2bbe0
1 parent d886d6d
commit 2d2bbe0
Show file tree

Hide file tree

Showing 12 changed files with 13 additions and 40 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -808,21 +808,15 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR
       rw [ModuleCat.coe_comp, Function.comp_apply, restrictScalars.map_apply]
       rfl
     homEquiv_counit := fun {X Y g} ↦ LinearMap.ext fun x => by
-        -- Porting note: once again reminding Lean of the instances
-        letI m1 : Module R S := Module.compHom S f
-        letI m2 : Module R Y := Module.compHom Y f
         induction x using TensorProduct.induction_on with
         | zero => rw [map_zero, map_zero]
         | tmul =>
           rw [ExtendRestrictScalarsAdj.homEquiv_symm_apply]
-          -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-          erw [ModuleCat.coe_comp]
-          rw [Function.comp_apply, ExtendRestrictScalarsAdj.counit_app]
+          dsimp
+          rw [ModuleCat.coe_comp, Function.comp_apply]
           -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
           erw [ExtendRestrictScalarsAdj.Counit.map_apply]
-          set_option tactic.skipAssignedInstances false in dsimp
-          rw [TensorProduct.lift.tmul]
-          rfl
+          dsimp
         | add => rw [map_add, map_add]; congr 1 }
 
 instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :

diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -982,8 +982,6 @@ theorem mem_prod_list_ofFn {a : α} {s : Fin n → Finset α} :
 @[to_additive]
 theorem mem_pow {a : α} {n : ℕ} :
     a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i => ↑(f i)).prod = a := by
-  -- Also compiles without the option, but much slower.
-  set_option tactic.skipAssignedInstances false in
   simp [← mem_coe, coe_pow, Set.mem_pow]
 
 @[to_additive (attr := simp) nsmul_empty]

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@@ -70,7 +70,6 @@ noncomputable abbrev trianglehOfDegreewiseSplit :
 
 variable [HasBinaryBiproducts C]
 
-set_option tactic.skipAssignedInstances false in
 /-- The canonical isomorphism `(mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q`
 when `p + 1 = q`. -/
 noncomputable def mappingConeHomOfDegreewiseSplitXIso (p q : ℤ) (hpq : p + 1 = q) :
@@ -116,7 +115,6 @@ noncomputable def mappingConeHomOfDegreewiseSplitIso :
     have r_f := (σ (p + 1 + 1)).r_f
     have s_g := (σ (p + 1)).s_g
     dsimp at r_f s_g
-    set_option tactic.skipAssignedInstances false in
     simp [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
       mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by linarith),
       cocycleOfDegreewiseSplit, r_f]

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean b/Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@@ -323,13 +323,11 @@ noncomputable def shiftTriangleIso (n : ℤ) :
       Triangle.mk_obj₂, Triangle.mk_mor₁, Preadditive.smul_iso_hom, Iso.refl_hom,
       Linear.comp_smul, comp_id, smul_smul, Int.units_coe_mul_self, one_smul, id_comp]
   · ext p
-    set_option tactic.skipAssignedInstances false in
     dsimp
     simp only [Units.smul_def, shiftIso, Int.reduceNeg, Linear.smul_comp, id_comp,
       ext_to_iff _ _ (p + 1) rfl, shiftFunctor_obj_X', assoc, lift_f_fst_v, Cocycle.coe_smul,
       Cocycle.shift_coe, Cochain.smul_v, Cochain.shift_v', Linear.comp_smul, inr_f_fst_v,
       smul_zero, lift_f_snd_v, inr_f_snd_v, and_true]
-    rw [smul_zero]
   · ext p
     dsimp
     simp only [triangle, Triangle.mk_mor₃, Cocycle.homOf_f, Cocycle.rightShift_coe,

diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -275,11 +275,8 @@ open Function RingHom
 
 theorem comap_inducing_of_surjective (hf : Surjective f) : Inducing (comap f) where
   induced := by
-    set_option tactic.skipAssignedInstances false in
-    simp_rw [TopologicalSpace.ext_iff, ← isClosed_compl_iff,
-      ← @isClosed_compl_iff (PrimeSpectrum S)
-        ((TopologicalSpace.induced (comap f) zariskiTopology)), isClosed_induced_iff,
-      isClosed_iff_zeroLocus]
+    simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus,
+      isClosed_induced_iff]
     refine fun s =>
       ⟨fun ⟨F, hF⟩ =>
         ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by

diff --git a/Mathlib/FieldTheory/KummerExtension.lean b/Mathlib/FieldTheory/KummerExtension.lean
@@ -369,7 +369,6 @@ lemma autAdjoinRootXPowSubCEquiv_root (η) :
     autAdjoinRootXPowSubCEquiv hζ hn H η (root _) = ((η : Kˣ) : K) • root _ :=
   autAdjoinRootXPowSubC_root hn a η
 
-set_option tactic.skipAssignedInstances false in
 lemma autAdjoinRootXPowSubCEquiv_symm_smul (σ) :
     ((autAdjoinRootXPowSubCEquiv hζ hn H).symm σ : Kˣ) • (root _ : K[n√a]) = σ (root _) := by
   have := Fact.mk H
@@ -380,7 +379,7 @@ lemma autAdjoinRootXPowSubCEquiv_symm_smul (σ) :
     Units.val_ofPowEqOne, ite_mul, one_mul, ne_eq]
   simp_rw [← root_X_pow_sub_C_eq_zero_iff H]
   split_ifs with h
-  · rw [h, mul_zero, map_zero]
+  · rw [h, map_zero]
   · rw [div_mul_cancel₀ _ h]
 
 end AdjoinRoot

diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean
@@ -197,21 +197,15 @@ theorem piecewise_apply {s : Set α} (hs : MeasurableSet s) (f g : α →ₛ β)
 @[simp]
 theorem piecewise_compl {s : Set α} (hs : MeasurableSet sᶜ) (f g : α →ₛ β) :
     piecewise sᶜ hs f g = piecewise s hs.of_compl g f :=
-  coe_injective <| by
-    set_option tactic.skipAssignedInstances false in
-    simp [hs]; convert Set.piecewise_compl s f g
+  coe_injective <| by simp [hs]
 
 @[simp]
 theorem piecewise_univ (f g : α →ₛ β) : piecewise univ MeasurableSet.univ f g = f :=
-  coe_injective <| by
-    set_option tactic.skipAssignedInstances false in
-    simp; convert Set.piecewise_univ f g
+  coe_injective <| by simp
 
 @[simp]
 theorem piecewise_empty (f g : α →ₛ β) : piecewise ∅ MeasurableSet.empty f g = g :=
-  coe_injective <| by
-    set_option tactic.skipAssignedInstances false in
-    simp; convert Set.piecewise_empty f g
+  coe_injective <| by simp
 
 @[simp]
 theorem piecewise_same (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) :

diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
@@ -213,8 +213,6 @@ theorem Basis.parallelepiped_map (b : Basis ι ℝ E) (e : E ≃ₗ[ℝ] F) :
     LinearMap.isOpenMap_of_finiteDimensional _ e.surjective) :=
   PositiveCompacts.ext (image_parallelepiped e.toLinearMap _).symm
 
--- removing this option makes elaboration approximately 1 second slower
-set_option tactic.skipAssignedInstances false in
 theorem Basis.prod_parallelepiped (v : Basis ι ℝ E) (w : Basis ι' ℝ F) :
     (v.prod w).parallelepiped = v.parallelepiped.prod w.parallelepiped := by
   ext x

diff --git a/Mathlib/Order/Closure.lean b/Mathlib/Order/Closure.lean
@@ -254,7 +254,7 @@ variable [CompleteLattice α] (c : ClosureOperator α)
 @[simps!]
 def ofCompletePred (p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : ClosureOperator α :=
   ofPred (fun a ↦ ⨅ b : {b // a ≤ b ∧ p b}, b) p
-    (fun a ↦ by set_option tactic.skipAssignedInstances false in simp [forall_swap])
+    (fun a ↦ by simp [forall_swap])
     (fun _ ↦ hsinf _ <| forall_mem_range.2 fun b ↦ b.2.2)
     (fun _ b hab hb ↦ iInf_le_of_le ⟨b, hab, hb⟩ le_rfl)
 

diff --git a/Mathlib/Order/Filter/Basic.lean b/Mathlib/Order/Filter/Basic.lean
@@ -991,7 +991,7 @@ theorem frequently_imp_distrib_left {f : Filter α} [NeBot f] {p : Prop} {q : α
 
 theorem frequently_imp_distrib_right {f : Filter α} [NeBot f] {p : α → Prop} {q : Prop} :
     (∃ᶠ x in f, p x → q) ↔ (∀ᶠ x in f, p x) → q := by
-  set_option tactic.skipAssignedInstances false in simp [frequently_imp_distrib]
+  simp only [frequently_imp_distrib, frequently_const]
 
 theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
     (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q := by

diff --git a/Mathlib/Probability/Process/Stopping.lean b/Mathlib/Probability/Process/Stopping.lean
@@ -387,8 +387,7 @@ theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i :
     by_cases hij : i ≤ j
     · simp only [hij, Set.setOf_true, Set.inter_univ]
       exact f.mono hij _ h
-    · set_option tactic.skipAssignedInstances false in simp [hij]
-      convert @MeasurableSet.empty _ (Filtration.seq f j)
+    · simp [hij]
 
 theorem measurableSpace_le_of_le_const (hτ : IsStoppingTime f τ) {i : ι} (hτ_le : ∀ ω, τ ω ≤ i) :
     hτ.measurableSpace ≤ f i :=

diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean
@@ -47,9 +47,7 @@ def piFanIsLimit {ι : Type v} (α : ι → TopCat.{max v u}) : IsLimit (piFan
     intro S m h
     apply ContinuousMap.ext; intro x
     funext i
-    set_option tactic.skipAssignedInstances false in
-    dsimp
-    rw [ContinuousMap.coe_mk, ← h ⟨i⟩]
+    simp [ContinuousMap.coe_mk, ← h ⟨i⟩]
     rfl
   fac _ _ := rfl