fixes

Author: j-loreaux

Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

@@ -91,7 +91,7 @@ instance (priority := 900) [IsOpenImmersion (pullback.diagonal f)] : FormallyUnr
   obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
   obtain ⟨x, rfl⟩ := Ideal.mem_span_singleton.mp (he'.le hx)
   refine (Ideal.toCotangent_eq_zero _ _).mpr ?_
-  rw [pow_two, Subtype.coe_mk, ← he, mul_assoc]
+  rw [pow_two, Subtype.coe_mk, ← he.eq, mul_assoc]
   exact Ideal.mul_mem_mul (he'.ge (Ideal.mem_span_singleton_self e)) hx
 
 theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -606,7 +606,7 @@ theorem starProjection_eq_self_iff {v : E} : K.starProjection v = v ↔ v ∈ K
 variable (K) in
 @[simp]
 lemma isIdempotentElem_starProjection : IsIdempotentElem K.starProjection :=
-  ContinuousLinearMap.ext fun x ↦ starProjection_eq_self_iff.mpr <| by simp
+  ⟨ContinuousLinearMap.ext fun x ↦ starProjection_eq_self_iff.mpr <| by simp⟩
 
 @[simp]
 lemma range_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :

Mathlib/RingTheory/Unramified/Field.lean

@@ -89,7 +89,7 @@ theorem bijective_of_isAlgClosed_of_isLocalRing
      algebraMap_eq_smul_one, hf₁, sub_self]
   have hf₃ : IsIdempotentElem (1 - f 1) := by
     apply IsIdempotentElem.one_sub
-    rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, hf₁]
+    rw [isIdempotentElem_iff, ← smul_eq_mul, ← map_smul, hf₁]
   have hf₄ : f 1 = 1 := by
     obtain ⟨n, hn⟩ := hA
     have : (1 - f 1) ^ n = 0 := by