fix errors

Author: dagurtomas

Mathlib/CategoryTheory/Galois/Topology.lean

@@ -92,7 +92,7 @@ lemma autEmbedding_range :
     Set.range (autEmbedding F) = ⋂ (f : Arrow C), { a | F.map f.hom ≫ (a f.right).hom =
       (a f.left).hom ≫ F.map f.hom } := by
   ext a
-  simp +instances only [Set.mem_range, DFunLike.coe_fn_eq, Set.mem_iInter, Set.mem_setOf_eq]
+  simp +instances only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq]
   refine ⟨fun ⟨σ, h⟩ i ↦ by cat_disch, fun h ↦ ?_⟩
   exact ⟨NatIso.ofComponents a (fun {X Y} f ↦ by
     ext; simpa using ConcreteCategory.congr_hom (h ⟨X, Y, f⟩) _), rfl⟩

Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

@@ -328,6 +328,7 @@ def smoothSheafCommRing.forgetStalk (x : TopCat.of M) :
       (smoothSheafCommRing IM I M R).presheaf) U).hom  := by
   dsimp
   rw [Iso.comp_inv_eq, ← smoothSheafCommRing.ι_forgetStalk_hom]
+  rfl
 
 /-- Given a smooth commutative ring `R` and a manifold `M`, and an open neighbourhood `U` of a point
 `x : M`, the evaluation-at-`x` map to `R` from smooth functions from  `U` to `R`. -/