From 5a0fdbfb21c2f5567dba58a41f278e65ca370e4a Mon Sep 17 00:00:00 2001
From: Blackfeather007 <2100017455@stu.pku.edu.cn>
Date: Sun, 6 Oct 2024 14:54:17 +0800
Subject: [PATCH] Update Basic.lean

---
 FilteredRing/Basic.lean | 37 +++++++++++++++++++++----------------
 1 file changed, 21 insertions(+), 16 deletions(-)

diff --git a/FilteredRing/Basic.lean b/FilteredRing/Basic.lean
index 7926676..0d67119 100644
--- a/FilteredRing/Basic.lean
+++ b/FilteredRing/Basic.lean
@@ -9,30 +9,21 @@ class FilteredRing (F : ι → AddSubgroup R) where
   one : 1 ∈ F 0
   mul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F j → x * y ∈ F (i + j)
 
-variable (F : ι → AddSubgroup R) [fil : FilteredRing F]
-variable (M : Type w) [AddCommGroup M] [Module R M]
+section FilteredRing
 
-class FilteredModule (F' : ι → Submodule R M) where
-  mono : ∀ i ≤ j, F' i ≤ F' j
-  smul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F' j → x • y ∈ F' (i + j)
+variable (F : ι → AddSubgroup R) [FilteredRing F]
 
 variable {F} in
-def F0 : Subring R where
+private def F0 : Subring R where
   __ := F 0
-  mul_mem' := by
-    intro a b ha hb
-    have := fil.mul_mem ha hb
-    rw [zero_add] at this
-    exact this
-  one_mem' := fil.one
+  mul_mem' hx hy := by simpa [zero_add] using FilteredRing.mul_mem hx hy
+  one_mem' := FilteredRing.one
 
 instance : Semiring (F 0) := inferInstanceAs (Semiring F0)
 
 instance Module_of_zero_fil (i : ι) : Module (F 0) (F i) where
   smul := fun x y ↦ ⟨x * y, by
-    have := fil.mul_mem (SetLike.coe_mem x) (SetLike.coe_mem y)
-    rw [zero_add] at this
-    exact this⟩
+    simpa [zero_add] using FilteredRing.mul_mem (SetLike.coe_mem x) (SetLike.coe_mem y)⟩
   one_smul := fun x ↦ SetLike.coe_eq_coe.mp (one_mul (x : R))
   mul_smul := fun x y a ↦ SetLike.coe_eq_coe.mp (mul_assoc (x : R) y a)
   smul_zero := fun x ↦ SetLike.coe_eq_coe.mp (mul_zero (x : R))
@@ -40,4 +31,18 @@ instance Module_of_zero_fil (i : ι) : Module (F 0) (F i) where
   add_smul := fun x y a ↦ SetLike.coe_eq_coe.mp (RightDistribClass.right_distrib (x : R) y a)
   zero_smul := fun x ↦ SetLike.coe_eq_coe.mp (zero_mul (x : R))
 
-instance fil_one_mem (i : ι) (hi : 0 ≤ i) : 1 ∈ F i := (fil.mono 0 hi) fil.one
+
+end FilteredRing
+
+
+section FilteredModule
+
+variable (F : ι → AddSubgroup R) [FilteredRing F]
+
+variable (M : Type w) [AddCommGroup M] [Module R M]
+
+class FilteredModule (F' : ι → AddSubgroup M) where
+  mono : ∀ i ≤ j, F' i ≤ F' j
+  smul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F' j → x • y ∈ F' (i + j)
+
+end FilteredModule