fixes for leanprover/lean4#5376

Mathlib/Algebra/GradedMonoid.lean

@@ -486,7 +486,8 @@ section Subobjects
 variable {R : Type*}
 
 /-- A version of `GradedMonoid.GOne` for internally graded objects. -/
-class SetLike.GradedOne {S : Type*} [SetLike S R] [One R] [Zero ι] (A : ι → S) : Prop where
+class SetLike.GradedOne {S : Type*}
+    [One R] [Zero ι] [SetLike S R] (A : ι → S) : Prop where
   /-- One has grade zero -/
   one_mem : (1 : R) ∈ A 0
 

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -294,7 +294,12 @@ theorem mem_carrier_iff_of_mem (hm : 0 < m) (q : Spec.T A⁰_ f) (a : A) {n} (hn
   trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
     ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
   · refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
-    convert zero_mem q.asIdeal
+    #adaptation_note
+    /--
+    After https://github.com/leanprover/lean4/pull/5376
+    we need to specify the implicit arguments by `inferInstance`.
+    -/
+    convert @zero_mem _ _ inferInstance inferInstance _ q.asIdeal
     apply HomogeneousLocalization.val_injective
     simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
       HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -583,7 +583,8 @@ the morphism `Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to t
 -/
 @[reassoc (attr := simp)]
 lemma pullbackSpecIso_inv_snd :
-    (pullbackSpecIso R S T).inv ≫ pullback.snd _ _ = Spec.map (ofHom (toRingHom includeRight)) :=
+    (pullbackSpecIso R S T).inv ≫ pullback.snd _ _ =
+      Spec.map (ofHom (R := T) (S := S ⊗[R] T) (toRingHom includeRight)) :=
   limit.isoLimitCone_inv_π _ _
 /--
 The composition of the isomorphism `pullbackSepcIso R S T` (from the pullback of

Mathlib/FieldTheory/KummerExtension.lean

@@ -272,9 +272,13 @@ theorem Polynomial.separable_X_pow_sub_C_of_irreducible : (X ^ n - C a).Separabl
     AdjoinRoot.algebraMap_eq,
     X_pow_sub_C_eq_prod (hζ.map_of_injective (algebraMap K _).injective) hn
     (root_X_pow_sub_C_pow n a), separable_prod_X_sub_C_iff']
-  sorry
-  -- exact (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
-  --   (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)
+  #adaptation_note
+  /--
+  After https://github.com/leanprover/lean4/pull/5376 we need to provide this helper instance.
+  -/
+  have : MonoidHomClass (K →+* K[n√a]) K K[n√a] := inferInstance
+  exact (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
+    (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)
 
 /-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
 `η ↦ (ⁿ√a ↦ η • ⁿ√a)`. Also see `autAdjoinRootXPowSubC` for the `AlgEquiv` version. -/

Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

@@ -219,11 +219,10 @@ theorem tmul_coe_mul_one_tmul {j₁ : ι} (a₁ : A) (b₁ : ℬ j₁) (b₂ : B
 
 theorem tmul_one_mul_one_tmul (a₁ : A) (b₂ : B) :
     (a₁ ᵍ⊗ₜ[R] (1 : B) * (1 : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ : A) ᵍ⊗ₜ (b₂ : B) := by
-  sorry
-  -- convert tmul_coe_mul_zero_coe_tmul 𝒜 ℬ
-  --   a₁ (@GradedMonoid.GOne.one _ (ℬ ·) _ _) (@GradedMonoid.GOne.one _ (𝒜 ·) _ _) b₂
-  -- · rw [SetLike.coe_gOne, mul_one]
-  -- · rw [SetLike.coe_gOne, one_mul]
+  convert tmul_coe_mul_zero_coe_tmul 𝒜 ℬ
+    a₁ (GradedMonoid.GOne.one (A := (ℬ ·))) (GradedMonoid.GOne.one (A := (𝒜 ·))) b₂
+  · rw [SetLike.coe_gOne, mul_one]
+  · rw [SetLike.coe_gOne, one_mul]
 
 /-- The ring morphism `A →+* A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/
 @[simps]