FunLike の仕様変更に伴うエラーを解消する

Solution/Advanced/Algebra/Lecture2.lean

@@ -31,7 +31,7 @@ variable [Group G₁] [Group G₂] {f : G₁ →* G₂}
 -- `f`と`a : G₁`に対して、いちいち`f.toFun a`と書く代わりに、`f a`と書くためのおまじない
 -- （`f`そのものは、写像`f.toFun`と、それが積を保つという事実`f.map_mul'`を束ねたもので、本来は写像でない）
 -- 右側のInfoviewには、`f a`の代わりに`↑f a`と表示されることもあるが、同じなので気にしないでください。
-instance : FunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where
+instance : DFunLike (G₁ →* G₂) G₁ (fun _ ↦ G₂) where
   coe := fun f ↦ f.toFun
   coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr
 

Solution/Advanced/Algebra/Lecture3.lean

@@ -148,7 +148,7 @@ notation:25 X " →[" G:25 "] " Y:0 => GroupActionHom G X Y
 variable [Group G] [GroupAction G X] [GroupAction G Y] [GroupAction G Z]
 
 -- `f : X →[G] Y`に対して`f x`のように書くためのおまじない。
-instance : FunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where
+instance : DFunLike (GroupActionHom G X Y) X (fun _ ↦ Y) where
   coe f := f.toFun
   coe_injective' f₁ f₂ _ := by cases f₁; cases f₂; congr
 
@@ -161,7 +161,7 @@ theorem GroupActionHom.coe_coe (f : X → Y) (h) : ((⟨f, h⟩ : X →[G] Y) :
 -- 定義からすぐ分かること
 @[ext]
 theorem GroupActionHom.ext {f₁ f₂ : X →[G] Y} : (∀ x, f₁ x = f₂ x) → f₁ = f₂ :=
-  FunLike.ext f₁ f₂
+  DFunLike.ext f₁ f₂
 
 theorem map_smul (f : X →[G] Y) : ∀ (a : G) (x : X), f (a • x) = a • f x := f.map_smul'
 

Solution/Advanced/Category/Lecture1.lean

@@ -174,6 +174,14 @@ instance {R : CommRingCat} : Category (CommAlgCat R) where
 
 /- 定義の上の`@[simps]`はおまじないで、ここでは特に意味がない。`Lecture 2`で役に立つ。 -/
 
+-- おまじない
+instance {A B : CommAlgCat R} : FunLike (Hom A B) A B where
+  coe f := f.toFun
+  coe_injective' f g h := by
+    rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
+    rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
+    congr
+
 -- おまじない。`Lecture 2`で役に立つ。
 instance {A B : CommAlgCat R} : AlgHomClass (Hom A B) R A B :=
   inferInstanceAs <| AlgHomClass (A →ₐ[R] B) R A B