fix

Author: Kha

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -562,11 +562,11 @@ public lemma algebraMap_germ
 
 @[deprecated (since := "2026-02-10")] public alias toOpen_germ := algebraMap_germ
 
-@[expose] public
+public
 instance (x : PrimeSpectrum.Top R) : Algebra R ((structurePresheafInCommRingCat R).stalk x) :=
   (toStalk R x).hom.toAlgebra
 
-@[expose] public
+public
 instance (x : PrimeSpectrum.Top R) :
     Module R ↑(TopCat.Presheaf.stalk (moduleStructurePresheaf R M).presheaf x) :=
   .compHom _ (toStalk R x).hom

Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

@@ -446,7 +446,7 @@ def cosPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ where
   continuousOn_invFun := continuous_arccos.continuousOn
 
 /-- `Real.cos` and `Real.arccos` as a (partial) equivalence from `[0, π]` to `[-1, 1]` -/
-@[simps, expose]
+@[simps]
 noncomputable def cosPartialEquiv : PartialEquiv ℝ ℝ where
   toFun θ := cos θ
   invFun x := arccos x

Mathlib/Tactic/NormNum/Result.lean

@@ -311,7 +311,7 @@ section
 set_option linter.unusedVariables false
 
 /-- The result of `norm_num` running on an expression `x` of type `α`. -/
-@[nolint unusedArguments, expose] def Result {α : Q(Type u)} (x : Q($α)) := Result'
+@[nolint unusedArguments] def Result {α : Q(Type u)} (x : Q($α)) := Result'
 
 -- The new behaviour of `inferInstanceAs` from leanprover/lean4#12897 needs to be updated,
 -- to ensure that if we are in a `meta` section then the auxiliary definitions are also `meta`.
@@ -320,36 +320,36 @@ set_option backward.inferInstanceAs.wrap false in
 instance {α : Q(Type u)} {x : Q($α)} : Inhabited (Result x) := inferInstanceAs (Inhabited Result')
 
 /-- The result is `proof : x`, where `x` is a (true) proposition. -/
-@[match_pattern, inline, expose] def Result.isTrue {x : Q(Prop)} :
+@[match_pattern, inline] def Result.isTrue {x : Q(Prop)} :
     ∀ (proof : Q($x)), Result q($x) := Result'.isBool true
 
 /-- The result is `proof : ¬x`, where `x` is a (false) proposition. -/
-@[match_pattern, inline, expose] def Result.isFalse {x : Q(Prop)} :
+@[match_pattern, inline] def Result.isFalse {x : Q(Prop)} :
     ∀ (proof : Q(¬$x)), Result q($x) := Result'.isBool false
 
 /-- The result is `lit : ℕ` (a raw nat literal) and `proof : isNat x lit`. -/
-@[match_pattern, inline, expose] def Result.isNat {α : Q(Type u)} {x : Q($α)} :
+@[match_pattern, inline] def Result.isNat {α : Q(Type u)} {x : Q($α)} :
     ∀ (inst : Q(AddMonoidWithOne $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsNat $x $lit)),
       Result x := Result'.isNat
 
 /-- The result is `-lit` where `lit` is a raw nat literal
 and `proof : isInt x (.negOfNat lit)`. -/
-@[match_pattern, inline, expose] def Result.isNegNat {α : Q(Type u)} {x : Q($α)} :
+@[match_pattern, inline] def Result.isNegNat {α : Q(Type u)} {x : Q($α)} :
     ∀ (inst : Q(Ring $α) := by assumption) (lit : Q(ℕ)) (proof : Q(IsInt $x (.negOfNat $lit))),
       Result x := Result'.isNegNat
 
 /-- The result is `proof : IsNNRat x n d`,
 where `n` a raw nat literal, `d` is a raw nat literal (not 0 or 1),
 `n` and `d` are coprime, and `q` is the value of `n / d`. -/
-@[match_pattern, inline, expose] def Result.isNNRat {α : Q(Type u)} {x : Q($α)} :
+@[match_pattern, inline] def Result.isNNRat {α : Q(Type u)} {x : Q($α)} :
     ∀ (inst : Q(DivisionSemiring $α) := by assumption) (q : Rat) (n : Q(ℕ)) (d : Q(ℕ))
       (proof : Q(IsNNRat $x $n $d)), Result x := Result'.isNNRat
 
 /-- The result is `proof : IsRat x n d`,
 where `n` is `.negOfNat lit` with `lit` a raw nat literal,
 `d` is a raw nat literal (not 0 or 1),
 `n` and `d` are coprime, and `q` is the value of `n / d`. -/
-@[match_pattern, inline, expose] def Result.isNegNNRat {α : Q(Type u)} {x : Q($α)} :
+@[match_pattern, inline] def Result.isNegNNRat {α : Q(Type u)} {x : Q($α)} :
     ∀ (inst : Q(DivisionRing $α) := by assumption) (q : Rat) (n : Q(ℕ)) (d : Q(ℕ))
       (proof : Q(IsRat $x (.negOfNat $n) $d)), Result x := Result'.isNegNNRat