From 4128908e3e226661f51d3b1074d3250bbab3362e Mon Sep 17 00:00:00 2001 From: Artie Khovanov Date: Wed, 22 Jan 2025 00:02:19 +0000 Subject: [PATCH] . --- Mathlib/Algebra/Ring/Subring/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Ring/Subring/Defs.lean b/Mathlib/Algebra/Ring/Subring/Defs.lean index 608eca3327899..f22e50e3e09ac 100644 --- a/Mathlib/Algebra/Ring/Subring/Defs.lean +++ b/Mathlib/Algebra/Ring/Subring/Defs.lean @@ -85,7 +85,7 @@ instance (priority := 100) SubringClass.nonUnitalSubringClass (S : Type*) (R : T variable [SetLike S R] [hSR : SubringClass S R] (s : S) -@[simp] +@[simp, aesop safe apply (rule_sets := [SetLike])] theorem intCast_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem] @[deprecated _root_.intCast_mem (since := "2024-04-05")] alias coe_int_mem := intCast_mem