adaptations for 9638

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -50,7 +50,7 @@ variable {K : Type u} {L : Type v} {M : Type w}
 variable [DivisionRing K] [DivisionRing L] [DivisionRing M]
 
 /-- `SubfieldClass S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
-class SubfieldClass (S K : Type*) [DivisionRing K] [SetLike S K] : Prop
+class SubfieldClass (S : Type*) (K : outParam Type*) [DivisionRing K] [SetLike S K] : Prop
     extends SubringClass S K, InvMemClass S K
 
 namespace SubfieldClass

Mathlib/Algebra/Ring/Equiv.lean

@@ -76,8 +76,8 @@ add_decl_doc RingEquiv.toMulEquiv
 
 /-- `RingEquivClass F R S` states that `F` is a type of ring structure preserving equivalences.
 You should extend this class when you extend `RingEquiv`. -/
-class RingEquivClass (F R S : Type*) [Mul R] [Add R] [Mul S] [Add S] [EquivLike F R S] : Prop
-  extends MulEquivClass F R S where
+class RingEquivClass (F : Type*) (R S : outParam Type*) [Mul R] [Add R] [Mul S] [Add S]
+    [EquivLike F R S] : Prop extends MulEquivClass F R S where
   /-- By definition, a ring isomorphism preserves the additive structure. -/
   map_add : ∀ (f : F) (a b), f (a + b) = f a + f b
 

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

@@ -80,7 +80,9 @@ lemma app_localPreimage {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : Cᵒᵖ} (s : T
 
 /-- A morphism of presheaves `f : F ⟶ G` is locally surjective with respect to a grothendieck
 topology if every section of `G` is locally in the image of `f`. -/
-class IsLocallySurjective {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) : Prop where
+class IsLocallySurjective {FA : outParam (A → A → Type*)} {CA : outParam (A → Type w')}
+    [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory.{w'} A FA]
+    {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) : Prop where
   imageSieve_mem {U : C} (s : ToType (G.obj (op U))) : imageSieve f s ∈ J U
 
 lemma imageSieve_mem {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) [IsLocallySurjective J f] {U : Cᵒᵖ}
@@ -330,7 +332,9 @@ variable {F₁ F₂ F₃ : Sheaf J A} (φ : F₁ ⟶ F₂) (ψ : F₂ ⟶ F₃)
 
 /-- If `φ : F₁ ⟶ F₂` is a morphism of sheaves, this is an abbreviation for
 `Presheaf.IsLocallySurjective J φ.val`. -/
-abbrev IsLocallySurjective := Presheaf.IsLocallySurjective J φ.val
+abbrev IsLocallySurjective {FA : outParam (A → A → Type*)} {CA : outParam (A → Type w')}
+    [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory.{w'} A FA]
+    {F₁ F₂ : Sheaf J A} (φ : F₁ ⟶ F₂) := Presheaf.IsLocallySurjective J φ.val
 
 lemma isLocallySurjective_sheafToPresheaf_map_iff :
     Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map φ) ↔ IsLocallySurjective φ := by rfl

Mathlib/Order/Heyting/Hom.lean

@@ -62,8 +62,8 @@ structure BiheytingHom (α β : Type*) [BiheytingAlgebra α] [BiheytingAlgebra 
 /-- `HeytingHomClass F α β` states that `F` is a type of Heyting homomorphisms.
 
 You should extend this class when you extend `HeytingHom`. -/
-class HeytingHomClass (F α β : Type*) [HeytingAlgebra α] [HeytingAlgebra β] [FunLike F α β] : Prop
-    extends LatticeHomClass F α β where
+class HeytingHomClass (F : Type*) (α β : outParam Type*) [HeytingAlgebra α] [HeytingAlgebra β]
+    [FunLike F α β] : Prop extends LatticeHomClass F α β where
   /-- The proposition that a Heyting homomorphism preserves the bottom element. -/
   map_bot (f : F) : f ⊥ = ⊥
   /-- The proposition that a Heyting homomorphism preserves the Heyting implication. -/
@@ -72,9 +72,8 @@ class HeytingHomClass (F α β : Type*) [HeytingAlgebra α] [HeytingAlgebra β]
 /-- `CoheytingHomClass F α β` states that `F` is a type of co-Heyting homomorphisms.
 
 You should extend this class when you extend `CoheytingHom`. -/
-class CoheytingHomClass (F α β : Type*) [CoheytingAlgebra α] [CoheytingAlgebra β] [FunLike F α β] :
-    Prop
-  extends LatticeHomClass F α β where
+class CoheytingHomClass (F : Type*) (α β : outParam Type*) [CoheytingAlgebra α] [CoheytingAlgebra β]
+    [FunLike F α β] : Prop extends LatticeHomClass F α β where
   /-- The proposition that a co-Heyting homomorphism preserves the top element. -/
   map_top (f : F) : f ⊤ = ⊤
   /-- The proposition that a co-Heyting homomorphism preserves the difference operation. -/
@@ -83,9 +82,8 @@ class CoheytingHomClass (F α β : Type*) [CoheytingAlgebra α] [CoheytingAlgebr
 /-- `BiheytingHomClass F α β` states that `F` is a type of bi-Heyting homomorphisms.
 
 You should extend this class when you extend `BiheytingHom`. -/
-class BiheytingHomClass (F α β : Type*) [BiheytingAlgebra α] [BiheytingAlgebra β] [FunLike F α β] :
-    Prop
-  extends LatticeHomClass F α β where
+class BiheytingHomClass (F : Type*) (α β : outParam Type*) [BiheytingAlgebra α] [BiheytingAlgebra β]
+    [FunLike F α β] : Prop extends LatticeHomClass F α β where
   /-- The proposition that a bi-Heyting homomorphism preserves the Heyting implication. -/
   map_himp (f : F) : ∀ a b, f (a ⇨ b) = f a ⇨ f b
   /-- The proposition that a bi-Heyting homomorphism preserves the difference operation. -/

Mathlib/Order/Hom/Bounded.lean

@@ -74,7 +74,7 @@ class BotHomClass (F : Type*) (α β : outParam Type*) [Bot α] [Bot β] [FunLik
 /-- `BoundedOrderHomClass F α β` states that `F` is a type of bounded order morphisms.
 
 You should extend this class when you extend `BoundedOrderHom`. -/
-class BoundedOrderHomClass (F α β : Type*) [LE α] [LE β]
+class BoundedOrderHomClass (F : Type*) (α β : outParam Type*) [LE α] [LE β]
     [BoundedOrder α] [BoundedOrder β] [FunLike F α β] : Prop
   extends RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
   /-- Morphisms preserve the top element. The preferred spelling is `_root_.map_top`. -/

Mathlib/Order/Hom/BoundedLattice.lean

@@ -73,25 +73,24 @@ section
 /-- `SupBotHomClass F α β` states that `F` is a type of finitary supremum-preserving morphisms.
 
 You should extend this class when you extend `SupBotHom`. -/
-class SupBotHomClass (F α β : Type*) [Max α] [Max β] [Bot α] [Bot β] [FunLike F α β] : Prop
-  extends SupHomClass F α β where
+class SupBotHomClass (F : Type*) (α β : outParam Type*) [Max α] [Max β] [Bot α] [Bot β]
+    [FunLike F α β] : Prop extends SupHomClass F α β where
   /-- A `SupBotHomClass` morphism preserves the bottom element. -/
   map_bot (f : F) : f ⊥ = ⊥
 
 /-- `InfTopHomClass F α β` states that `F` is a type of finitary infimum-preserving morphisms.
 
 You should extend this class when you extend `SupBotHom`. -/
-class InfTopHomClass (F α β : Type*) [Min α] [Min β] [Top α] [Top β] [FunLike F α β] : Prop
-  extends InfHomClass F α β where
+class InfTopHomClass (F : Type*) (α β : outParam Type*) [Min α] [Min β] [Top α] [Top β]
+    [FunLike F α β] : Prop extends InfHomClass F α β where
   /-- An `InfTopHomClass` morphism preserves the top element. -/
   map_top (f : F) : f ⊤ = ⊤
 
 /-- `BoundedLatticeHomClass F α β` states that `F` is a type of bounded lattice morphisms.
 
 You should extend this class when you extend `BoundedLatticeHom`. -/
-class BoundedLatticeHomClass (F α β : Type*) [Lattice α] [Lattice β] [BoundedOrder α]
-    [BoundedOrder β] [FunLike F α β] : Prop
-  extends LatticeHomClass F α β where
+class BoundedLatticeHomClass (F : Type*) (α β : outParam Type*) [Lattice α] [Lattice β]
+    [BoundedOrder α] [BoundedOrder β] [FunLike F α β] : Prop extends LatticeHomClass F α β where
   /-- A `BoundedLatticeHomClass` morphism preserves the top element. -/
   map_top (f : F) : f ⊤ = ⊤
   /-- A `BoundedLatticeHomClass` morphism preserves the bottom element. -/

Mathlib/Order/Hom/CompleteLattice.lean

@@ -75,31 +75,32 @@ section
 /-- `sSupHomClass F α β` states that `F` is a type of `⨆`-preserving morphisms.
 
 You should extend this class when you extend `sSupHom`. -/
-class sSupHomClass (F α β : Type*) [SupSet α] [SupSet β] [FunLike F α β] : Prop where
+class sSupHomClass (F : Type*) (α β : outParam Type*) [SupSet α] [SupSet β] [FunLike F α β] :
+    Prop where
   /-- The proposition that members of `sSupHomClass`s commute with arbitrary suprema/joins. -/
   map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)
 
 /-- `sInfHomClass F α β` states that `F` is a type of `⨅`-preserving morphisms.
 
 You should extend this class when you extend `sInfHom`. -/
-class sInfHomClass (F α β : Type*) [InfSet α] [InfSet β] [FunLike F α β] : Prop where
+class sInfHomClass (F : Type*) (α β : outParam Type*) [InfSet α] [InfSet β] [FunLike F α β] :
+    Prop where
   /-- The proposition that members of `sInfHomClass`s commute with arbitrary infima/meets. -/
   map_sInf (f : F) (s : Set α) : f (sInf s) = sInf (f '' s)
 
 /-- `FrameHomClass F α β` states that `F` is a type of frame morphisms. They preserve `⊓` and `⨆`.
 
 You should extend this class when you extend `FrameHom`. -/
-class FrameHomClass (F α β : Type*) [CompleteLattice α] [CompleteLattice β] [FunLike F α β] : Prop
-  extends InfTopHomClass F α β where
+class FrameHomClass (F : Type*) (α β : outParam Type*) [CompleteLattice α] [CompleteLattice β]
+    [FunLike F α β] : Prop extends InfTopHomClass F α β where
   /-- The proposition that members of `FrameHomClass` commute with arbitrary suprema/joins. -/
   map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)
 
 /-- `CompleteLatticeHomClass F α β` states that `F` is a type of complete lattice morphisms.
 
 You should extend this class when you extend `CompleteLatticeHom`. -/
-class CompleteLatticeHomClass (F α β : Type*) [CompleteLattice α] [CompleteLattice β]
-    [FunLike F α β] : Prop
-  extends sInfHomClass F α β where
+class CompleteLatticeHomClass (F : Type*) (α β : outParam Type*) [CompleteLattice α]
+    [CompleteLattice β] [FunLike F α β] : Prop extends sInfHomClass F α β where
   /-- The proposition that members of `CompleteLatticeHomClass` commute with arbitrary
   suprema/joins. -/
   map_sSup (f : F) (s : Set α) : f (sSup s) = sSup (f '' s)

Mathlib/Order/Hom/Lattice.lean

@@ -71,22 +71,22 @@ section
 /-- `SupHomClass F α β` states that `F` is a type of `⊔`-preserving morphisms.
 
 You should extend this class when you extend `SupHom`. -/
-class SupHomClass (F α β : Type*) [Max α] [Max β] [FunLike F α β] : Prop where
+class SupHomClass (F : Type*) (α β : outParam Type*) [Max α] [Max β] [FunLike F α β] : Prop where
   /-- A `SupHomClass` morphism preserves suprema. -/
   map_sup (f : F) (a b : α) : f (a ⊔ b) = f a ⊔ f b
 
 /-- `InfHomClass F α β` states that `F` is a type of `⊓`-preserving morphisms.
 
 You should extend this class when you extend `InfHom`. -/
-class InfHomClass (F α β : Type*) [Min α] [Min β] [FunLike F α β] : Prop where
+class InfHomClass (F : Type*) (α β : outParam Type*) [Min α] [Min β] [FunLike F α β] : Prop where
   /-- An `InfHomClass` morphism preserves infima. -/
   map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
 
 /-- `LatticeHomClass F α β` states that `F` is a type of lattice morphisms.
 
 You should extend this class when you extend `LatticeHom`. -/
-class LatticeHomClass (F α β : Type*) [Lattice α] [Lattice β] [FunLike F α β] : Prop
-  extends SupHomClass F α β where
+class LatticeHomClass (F : Type*) (α β : outParam Type*) [Lattice α] [Lattice β]
+    [FunLike F α β] : Prop extends SupHomClass F α β where
   /-- A `LatticeHomClass` morphism preserves infima. -/
   map_inf (f : F) (a b : α) : f (a ⊓ b) = f a ⊓ f b
 

Mathlib/RingTheory/FilteredAlgebra/Basic.lean

@@ -88,8 +88,8 @@ and the pointwise scalar multiplication of `F i` and `FM j` is in `F (i +ᵥ j)`
 
 The index set `ιM` for the module can be more general, however usually we take `ιM = ι`. -/
 class IsModuleFiltration (F : ι → σ) (F_lt : outParam <| ι → σ) [IsRingFiltration F F_lt]
-    (F' : ιM → σM) (F'_lt : outParam <| ιM → σM) : Prop
-    extends IsFiltration F' F'_lt, SetLike.GradedSMul F F'
+    (F' : ιM → σM) (F'_lt : outParam <| ιM → σM) [IsFiltration F' F'_lt] : Prop
+    extends SetLike.GradedSMul F F'
 
 /-- A convenience constructor for `IsModuleFiltration` when the index is the integers. -/
 lemma IsModuleFiltration.mk_int (F : ℤ → σ) (mono : Monotone F) [SetLike.GradedMonoid F]

Mathlib/RingTheory/NonUnitalSubring/Defs.lean

@@ -47,8 +47,8 @@ section NonUnitalSubringClass
 
 /-- `NonUnitalSubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative submonoid and an additive subgroup. -/
-class NonUnitalSubringClass (S : Type*) (R : Type u) [NonUnitalNonAssocRing R] [SetLike S R] : Prop
-  extends NonUnitalSubsemiringClass S R, NegMemClass S R where
+class NonUnitalSubringClass (S : Type*) (R : outParam (Type u)) [NonUnitalNonAssocRing R]
+    [SetLike S R] : Prop extends NonUnitalSubsemiringClass S R, NegMemClass S R where
 
 -- See note [lower instance priority]
 instance (priority := 100) NonUnitalSubringClass.addSubgroupClass (S : Type*) (R : Type u)

Mathlib/RingTheory/RingInvo.lean

@@ -37,7 +37,7 @@ add_decl_doc RingInvo.toRingEquiv
 
 /-- `RingInvoClass F R` states that `F` is a type of ring involutions.
 You should extend this class when you extend `RingInvo`. -/
-class RingInvoClass (F R : Type*) [Semiring R] [EquivLike F R Rᵐᵒᵖ] : Prop
+class RingInvoClass (F : Type*) (R : outParam Type*) [Semiring R] [EquivLike F R Rᵐᵒᵖ] : Prop
   extends RingEquivClass F R Rᵐᵒᵖ where
   /-- Every ring involution must be its own inverse -/
   involution : ∀ (f : F) (x), (f (f x).unop).unop = x

Mathlib/Topology/Spectral/Hom.lean

@@ -74,7 +74,7 @@ section
 /-- `SpectralMapClass F α β` states that `F` is a type of spectral maps.
 
 You should extend this class when you extend `SpectralMap`. -/
-class SpectralMapClass (F α β : Type*) [TopologicalSpace α] [TopologicalSpace β]
+class SpectralMapClass (F : Type*) (α β : outParam Type*) [TopologicalSpace α] [TopologicalSpace β]
     [FunLike F α β] : Prop where
   /-- statement that `F` is a type of spectral maps -/
   map_spectral (f : F) : IsSpectralMap f

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99d3bd0522280b5b4d21f3817b3f94c726f33278",
+   "rev": "3e5895e54e7a5534738e3497ca9782f2e21bb35a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "lean-pr-testing-9638",