Revert "fix proof"

Thmoas-Guan · Thmoas-Guan · commit aa42b3a429fe · 2025-02-17T22:12:20.000+08:00
This reverts commit c355b1a.
diff --git a/Mathlib/RingTheory/AdicCompletion/Algebra.lean b/Mathlib/RingTheory/AdicCompletion/Algebra.lean
@@ -60,19 +60,18 @@ def transitionMapₐ {m n : ℕ} (hmn : m ≤ n) :
 
 /-- `AdicCompletion I R` is an `R`-subalgebra of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`. -/
 def subalgebra : Subalgebra R (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
-  Submodule.toSubalgebra (submodule I R) (fun _ ↦ by simp [transitionMap_map_one I])
-    (fun x y hx hy m n hmn ↦ by simp [hx hmn, hy hmn, transitionMap_map_mul I hmn])
+  Submodule.toSubalgebra (submodule I R) (fun _ ↦ by simp)
+    (fun x y hx hy m n hmn ↦ by simp [hx hmn, hy hmn])
 
 /-- `AdicCompletion I R` is a subring of `∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)`. -/
 def subring : Subring (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) :=
   Subalgebra.toSubring (subalgebra I)
 
 instance : Mul (AdicCompletion I R) where
-  mul x y := ⟨x.val * y.val, fun hmn ↦ by
-    simp [x.property, y.property, transitionMap_map_mul I hmn]⟩
+  mul x y := ⟨x.val * y.val, by simp [x.property, y.property]⟩
 
 instance : One (AdicCompletion I R) where
-  one := ⟨1, by simp [transitionMap_map_one I]⟩
+  one := ⟨1, by simp⟩
 
 instance : NatCast (AdicCompletion I R) where
   natCast n := ⟨n, fun _ ↦ rfl⟩
@@ -81,7 +80,7 @@ instance : IntCast (AdicCompletion I R) where
   intCast n := ⟨n, fun _ ↦ rfl⟩
 
 instance : Pow (AdicCompletion I R) ℕ where
-  pow x n := ⟨x.val ^ n, fun hmn ↦ by simp [x.property, transitionMap_map_pow I hmn]⟩
+  pow x n := ⟨x.val ^ n, fun _ ↦ by simp [x.property]⟩
 
 instance : CommRing (AdicCompletion I R) :=
   let f : AdicCompletion I R → ∀ n, R ⧸ (I ^ n • ⊤ : Ideal R) := Subtype.val
@@ -91,11 +90,9 @@ instance : CommRing (AdicCompletion I R) :=
 
 instance [Algebra S R] : Algebra S (AdicCompletion I R) where
   algebraMap :=
-  { toFun r := ⟨algebraMap S (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) r, fun hmn ↦ by
-      simp only [Pi.algebraMap_apply,
-        IsScalarTower.algebraMap_apply S R (R ⧸ (I ^ _ • ⊤ : Ideal R)),
-        Ideal.Quotient.algebraMap_eq, mapQ_eq_factor]
-      rfl⟩
+  { toFun r := ⟨algebraMap S (∀ n, R ⧸ (I ^ n • ⊤ : Ideal R)) r, by
+      simp [-Ideal.Quotient.mk_algebraMap,
+        IsScalarTower.algebraMap_apply S R (R ⧸ (I ^ _ • ⊤ : Ideal R))]⟩
     map_one' := Subtype.ext <| map_one _
     map_mul' x y := Subtype.ext <| map_mul _ x y
     map_zero' := Subtype.ext <| map_zero _
@@ -242,8 +239,8 @@ instance smul : SMul (AdicCompletion I R) (AdicCompletion I M) where
     property := fun {m n} hmn ↦ by
       apply induction_on I R r (fun r ↦ ?_)
       apply induction_on I M x (fun x ↦ ?_)
-      simp only [coe_eval, mapQ_eq_factor, mk_apply_coe, mkQ_apply, Ideal.Quotient.mk_eq_mk,
-        mk_smul_mk, map_smul, mapQ_apply, LinearMap.id_coe, id_eq]
+      simp only [coe_eval, mk_apply_coe, mkQ_apply, Ideal.Quotient.mk_eq_mk,
+        mk_smul_mk, LinearMapClass.map_smul, mapQPow_mk]
       rw [smul_mk I hmn]
   }
 
