Unused hypothesis

leanprover-community · Dec 6, 2023 · b71c141 · b71c141
1 parent 0f90b48
commit b71c141
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Group/Units/Hom.lean b/Mathlib/Algebra/Group/Units/Hom.lean
@@ -223,7 +223,7 @@ theorem map [MonoidHomClass F M N] (f : F) {x : M} (h : IsUnit x) : IsUnit (f x)
 #align is_add_unit.map IsAddUnit.map
 
 @[to_additive]
-theorem of_leftInverse [MonoidHomClass F M N] [MonoidHomClass G N M] {f : F} {x : M} (g : G)
+theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G)
     (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) : IsUnit x := by
   simpa only [hfg x] using h.map g
 #align is_unit.of_left_inverse IsUnit.of_leftInverse

diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean
@@ -772,8 +772,8 @@ theorem ext_adjoin {s : Set A} [NDFunLike F (adjoin R s) B]
   · simp only [map_star, hx]
 #align star_alg_hom.ext_adjoin StarAlgHom.ext_adjoin
 
-theorem ext_adjoin_singleton {a : A} [NDFunLike F (adjoin R ({a} : Set A)) B] [StarHomClass F _ B]
-    [RingHomClass F _ B] [StarAlgHomClass F R (adjoin R ({a} : Set A)) B] {f g : F}
+theorem ext_adjoin_singleton {a : A} [NDFunLike F (adjoin R ({a} : Set A)) B]
+    [StarAlgHomClass F R (adjoin R ({a} : Set A)) B] {f g : F}
     (h : f ⟨a, self_mem_adjoin_singleton R a⟩ = g ⟨a, self_mem_adjoin_singleton R a⟩) : f = g :=
   ext_adjoin fun x hx =>
     (show x = ⟨a, self_mem_adjoin_singleton R a⟩ from

diff --git a/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
@@ -183,7 +183,7 @@ noncomputable instance (priority := 100) Complex.instStarHomClass : StarHomClass
 
 /-- This is not an instance to avoid type class inference loops. See
 `WeakDual.Complex.instStarHomClass`. -/
-noncomputable def _root_.AlgHomClass.instStarAlgHomClass : StarAlgHomClass F ℂ A ℂ :=
+noncomputable lemma _root_.AlgHomClass.instStarAlgHomClass : StarAlgHomClass F ℂ A ℂ :=
   { WeakDual.Complex.instStarHomClass, hF with }
 #align alg_hom_class.star_alg_hom_class AlgHomClass.instStarAlgHomClass